Prove oscillatory leading-principal interlacing - #430

Open

PerAlexandersson wants to merge 30 commits into

mainfrom

proof/issue-421-leading-principal-interlacing-20260826

Commits on Aug 24, 2026

feat: expose ordered primitive-compound spectrum
PerAlexandersson
committed
2062c93
feat: prove Perron root algebraic simplicity
PerAlexandersson
committed
68203a2
feat: derive simple spectrum from primitive compounds
PerAlexandersson
committed
687b1f8
feat: upgrade disjoint charpoly interlacing to strict
PerAlexandersson
committed
caf5397
fix: use an identifier for interlacing roots
PerAlexandersson
committed
13f9f40
Add variable-band Hessenberg determinant recurrence
PerAlexandersson
committed
3bc7fae
Expose banded Hessenberg definition
PerAlexandersson
committed
5c69576
Import banded Hessenberg determinant module
PerAlexandersson
committed
4f45667
feat(matrix): derive irreducibility from adjacent positivity
PerAlexandersson
committed
83ab624
feat(matrix): preserve principal spectra under block conjugation
PerAlexandersson
committed
d7cddc2

Commits on Aug 26, 2026

Merge remote-tracking branch 'origin/proof/issue-421-oscillatory' into proof/issue-421-oscillatory-missing-theory
PerAlexandersson
committed
b527ee4
Merge remote-tracking branch 'origin/proof/issue-425-variable-hessenberg-det' into proof/issue-421-oscillatory-missing-theory
PerAlexandersson
committed
1702548
Add primitive order-one oscillatory criteria
PerAlexandersson
committed
85805e9
Formalize Whitney elimination determinant core
PerAlexandersson
committed
46264e6
Add Whitney hard-branch cofactor step
PerAlexandersson
committed
b8745a6
Track adjacent Whitney insertion sign
PerAlexandersson
committed
ce5f64a
Prove Whitney elimination preserves total nonnegativity
PerAlexandersson
committed
1a57e9d
Add reversible Whitney factor step
PerAlexandersson
committed
c6ab684
Iterate Whitney first-column elimination
PerAlexandersson
committed
456aa75
Track Whitney clearing factors
PerAlexandersson
committed
a9b377b
Add trailing block transvection lemmas
PerAlexandersson
committed
daeca56
Expose recursive Whitney factorization
PerAlexandersson
committed
1b24969
Cycle Whitney sweep below subdiagonal
PerAlexandersson
committed
d7876ec
Generalize Whitney elimination to later columns
PerAlexandersson
committed
cda1dd3
Lift Whitney cycles through Hessenberg prefixes
PerAlexandersson
committed
41e91ad
Reduce TN matrices to tridiagonal form
PerAlexandersson
committed
2e95fdf
Preserve oscillatory adjacency through Whitney reduction
PerAlexandersson
committed
14413e2
Prove oscillatory strict principal interlacing
PerAlexandersson
committed
e8c5a18
Expose leading oscillatory interlacing
PerAlexandersson
committed
f705e37
Import oscillatory matrix modules
PerAlexandersson
committed
cee88c9

Navigation Menu

Prove oscillatory leading-principal interlacing - #430

Prove oscillatory leading-principal interlacing#430
PerAlexandersson wants to merge 30 commits into
mainfrom
proof/issue-421-leading-principal-interlacing-20260826

Commits on Aug 24, 2026

feat: expose ordered primitive-compound spectrum

feat: prove Perron root algebraic simplicity

feat: derive simple spectrum from primitive compounds

feat: upgrade disjoint charpoly interlacing to strict

fix: use an identifier for interlacing roots

Add variable-band Hessenberg determinant recurrence

Expose banded Hessenberg definition

Import banded Hessenberg determinant module

feat(matrix): derive irreducibility from adjacent positivity

feat(matrix): preserve principal spectra under block conjugation

Commits on Aug 26, 2026

Merge remote-tracking branch 'origin/proof/issue-421-oscillatory' into proof/issue-421-oscillatory-missing-theory

Merge remote-tracking branch 'origin/proof/issue-425-variable-hessenberg-det' into proof/issue-421-oscillatory-missing-theory

Add primitive order-one oscillatory criteria

Formalize Whitney elimination determinant core

Add Whitney hard-branch cofactor step

Track adjacent Whitney insertion sign

Prove Whitney elimination preserves total nonnegativity

Add reversible Whitney factor step

Iterate Whitney first-column elimination

Track Whitney clearing factors

Add trailing block transvection lemmas

Expose recursive Whitney factorization

Cycle Whitney sweep below subdiagonal

Generalize Whitney elimination to later columns

Lift Whitney cycles through Hessenberg prefixes

Reduce TN matrices to tridiagonal form

Preserve oscillatory adjacency through Whitney reduction

Prove oscillatory strict principal interlacing

Expose leading oscillatory interlacing

Import oscillatory matrix modules