Oscillatory matrices: simple spectrum and strict leading-principal charpoly interlacing

[PerAlexandersson]

Missing reusable theory

The library now proves the positive-spectrum part of Gantmacher–Krein for matrices whose compounds are primitive (exists_charpoly_eq_prod_of_forall_compound_primitive and exists_charpoly_eq_prod_of_pow_compound_pos), and issue #394 tracks the full singular/reducible TN theorem. A separate strict oscillatory interface is still missing.

We need a theorem package for a finite totally nonnegative matrix A satisfying the classical oscillation criterion:

• A is nonsingular;
• the first subdiagonal and first superdiagonal entries are strictly positive.

The desired conclusions are:

1. A.charpoly has positive, pairwise distinct roots;
2. the characteristic polynomial of the consecutive leading principal section strictly interlaces A.charpoly;
3. ideally, a bridge from the criterion above to the existing primitive-compound/power-positive-compound API.

This is not supplied by Cauchy interlacing: the matrices of interest are nonsymmetric upper Hessenberg matrices. It is also narrower than #394, which concerns arbitrary possibly singular and reducible TN matrices and does not provide strictness or leading-section interlacing.

Immediate consumer: A318107

A complete classical proof for A318107 factors its Hessenberg matrix as a product of three nonnegative bidiagonal matrices, proving total nonnegativity, positive determinant, and positive adjacent off-diagonals. The missing theorem above then gives simple positive eigenvalues and strict interlacing of consecutive leading sections, closing the polynomial argument.

Research checkpoint: real-rooted-oeis commit 699999f1 and note workbench/proof-explorers/A318107-hessenberg-oscillation-continuation-2026-08-24.md.

Suggested first milestones

• define an upstream-shaped oscillatory predicate or work directly from the criterion;
• expose distinctness from primitive compounds (the existing proof already uses strict Perron dominance);
• formalize the leading-principal section and the strict charpoly interlacing theorem;
• only then instantiate the A318107 Hessenberg family in its own repository.

No sorry, axioms, or theorem-shaped scaffolds should count as completion.

Reference

Branquinho–Foulquié-Moreno–Mañas, Oscillatory banded Hessenberg matrices, multiple orthogonal polynomials and random walks, arXiv:2203.13578, Theorems 1–2 and the leading-principal interlacing discussion on p. 21.

[PerAlexandersson]

Audit/checkpoint update (2026-08-24):

I first tested the proposed TN+nonsingular+positive-adjacent-off-diagonal route against the existing primitive-compound theorem. The bridge is not currently available in the repository. IsTotallyNonneg supplies minor nonnegativity and closure/submatrix APIs, while isPrimitive_compound_of_pow starts only after one already has a common power whose compound entries are positive. The classical Gantmacher--Krein criterion needed between those endpoints (equivalently, oscillatory iff TN, nonsingular, and the first sub-/super-diagonals are positive) requires solid-minor/positive-bidiagonal-factorization or sign-variation machinery that is not yet formalized. The cited paper https://arxiv.org/abs/2203.13578 states this criterion and the truncation/interlacing facts as classical inputs rather than proving the general matrix theorem.

There is an independent gap inside the current primitive-compound endpoint: spectral_dominance_of_primitive distinguishes other eigenvalue values from the Perron value, but does not establish algebraic simplicity of the Perron root. Consequently exists_charpoly_eq_prod_of_forall_compound_primitive proves a positive factorization but cannot rule out repeated factors. Strict leading-principal-section interlacing is a further separate gap: simple positive spectra for the matrix and its section do not alone imply interlacing; a sign-variation/eigenvector theorem (or a Hessenberg-specific determinant/sign recurrence) is still required.

PR #423 is the smallest checked reusable checkpoint I found. It exposes the positive eigenvalue enumeration already constructed by the compound proof as Antitone, preserves the old API, and proves a StrictAnti version under the natural explicit hypothesis that the characteristic polynomial is separable. This makes algebraic simplicity the exact remaining PF boundary without adding an axiom, sorry, or theorem-shaped scaffold. Focused and full lake-workspace builds passed (3,419 and 9,025 jobs), and both new theorems use only the standard axioms propext, Classical.choice, and Quot.sound.

Suggested continuation order:

1. Prove algebraic simplicity of the Perron root for a primitive matrix using positive right and left Perron vectors to exclude extra and generalized eigenvectors.
2. Apply that result to every compound. Equality of consecutive ordered eigenvalues gives two different subset products equal to the relevant compound Perron root, contradicting simplicity.
3. Formalize the classical adjacent-off-diagonal oscillatory criterion via solid minors or positive bidiagonal factorization, yielding primitive compounds through the existing power bridge.
4. Add the oscillatory sign-variation theorem needed to prove strict interlacing of consecutive leading-principal characteristic polynomials (and prove leading sections remain oscillatory).

This is intentionally partial; #421 should remain open.

[PerAlexandersson]

Additive continuation is now pushed to PR #423 (head 13f9f40c). This closes the Perron/compound-simplicity gap identified in the previous audit and adds the smallest clean strict-interlacing closure I found:

• Matrix.perronRoot_rootMultiplicity_eq_one_of_irreducible proves algebraic multiplicity one for the Perron root of an irreducible nonnegative real matrix; ..._of_primitive is the requested primitive corollary (68203a29).
• Matrix.exists_charpoly_eq_prod_strictAnti_of_forall_compound_primitive removes the separability hypothesis from the strict-spectrum endpoint. If two ordered eigenvalues coincide, two distinct q-subsets give the same top compound product; the compound Perron root would then occur at least twice, contradicting the new multiplicity theorem (687b1f84).
• Matrix.strictInterlace_charpoly_of_interlace_of_noCommonRoot upgrades an explicitly weakly interlacing pair of linear characteristic-polynomial factorizations to strict interlacing when the polynomials have no common real root (caf53979, with the parser-only identifier repair 13f9f40c).

The deletion/principal-submatrix audit found only the Hermitian Cauchy API (RealRooted.cauchy_interlacing and its polynomial wrapper), which does not apply to the generally nonsymmetric TN Hessenberg matrices here. Real-rootedness plus disjoint spectra also does not by itself imply weak interlacing. Thus, for B := A.submatrix Fin.castSucc Fin.castSucc, the two exact remaining classical inputs under TN, nonsingularity, and positive adjacent sub-/super-diagonals are:

1. ∀ r, A.charpoly.IsRoot r → ¬ B.charpoly.IsRoot r;
2. ordered factorizations lam, μ satisfying ∀ k, lam k.succ ≤ μ k ∧ μ k ≤ lam k.castSucc.

The new closure turns those two inputs into strict leading-section interlacing. Establishing them still needs the absent oscillatory sign-variation/eigenvector theorem, or an appropriate general Hessenberg determinant-sign recurrence; I did not add assumptions, axioms, sorry, or a statement scaffold.

Local serialized verification after the Lake slot was released:

• focused lake-workspace build RealRooted.Mathlib.LinearAlgebra.Matrix.GantmacherKrein: passed, 3,423 jobs;
• full lake-workspace build RealRooted: passed, 9,025 jobs;
• git diff --check and the forbidden-token audit: passed;
• #print axioms for the four new public endpoints reports only propext, Classical.choice, and Quot.sound.

The full issue remains open for the two inputs above.

[PerAlexandersson]

Mathematics-only continuation: the exact classical closure is Li--Mathias, “Interlacing inequalities for totally nonnegative matrices,” LAA 341 (2002), Lemma 1.2 and Theorem 2.1 (https://cklixx.people.wm.edu/tpinter.pdf), equivalently Fallat--Woerdeman, “Refinements on the interlacing of eigenvalues of certain totally nonnegative matrices,” Operators and Matrices 1 (2007), Theorems 2 and 1 (https://files.ele-math.com/articles/oam-01-18.pdf). For B = A.submatrix Fin.castSucc Fin.castSucc, TN + det A ≠ 0 + positive first sub/superdiagonals makes A oscillatory, makes B oscillatory, and gives ordered positive roots λᵢ > μᵢ > λᵢ₊₁. Thus both weak interlacing and no-common-root required downstream of PR #423 follow immediately.

The honest formalization boundary is the Li--Mathias Whitney TN-preserving similarity reduction compatible with the endpoint principal section, followed by diagonal symmetrization to an irreducible Jacobi matrix (or the comparably substantial Gantmacher--Krein nodal theorem); this is not an AXLE-sized missing lemma and no theorem-shaped scaffold is warranted. Full note PR: https://github.com/sqrt-of-2/real-rooted-oeis/pull/234. Existing formal API: #423.

[PerAlexandersson]

Bounded post-PR-#428 feasibility update:

PR #428 now supplies the local criterion-to-irreducibility step. The exact next bridge into PR #423 is the (c) → (a) direction of Li--Mathias Lemma 1.2 (equivalently the hard direction of Fallat--Woerdeman Theorem 2), stated in the API PR #423 already consumes:

theorem exists_pow_compound_pos_of_tn_det_ne_zero_irreducible
    {A : Matrix (Fin n) (Fin n) ℝ}
    (hTN : A.IsTotallyNonneg) (hdet : A.det ≠ 0)
    (hirr : A.IsIrreducible) :
    ∃ k, 0 < k ∧
      ∀ q, 1 ≤ q → q ≤ n → ∀ s t, 0 < Matrix.compound q (A ^ k) s t

The current library starts only after this conclusion (isPrimitive_compound_of_pow). Proving it requires, for every nontrivial q, irreducibility and positive diagonal entries of compound q A (then IsPrimitive.of_irreducible_pos_diagonal), plus a common exponent. Neither the required solid/principal-minor positivity nor compound irreducibility is present.

For the principal-section half, the smallest useful Whitney package is an all-rank existence theorem producing a real Hermitian irreducible tridiagonal J such that

J.charpoly = A.charpoly
(J.submatrix Fin.castSucc Fin.castSucc).charpoly =
  (A.submatrix Fin.castSucc Fin.castSucc).charpoly

with nonzero adjacent entries. Hermitian Cauchy interlacing would then give the weak inequalities; the Jacobi determinant recurrence gives no common root; PR #423 supplies the strict upgrade. This is exactly the reduction inside Li--Mathias Theorem 2.1, not a missing one-line matrix identity.

A compact algebraic leaf was feasible and is checked locally: block-diagonal conjugation preserves the ambient and both diagonal-block characteristic polynomials (charpoly_fromBlocks_diagonal_conj and the two charpoly_toBlocks... variants). AXLE 4.31 checked the exact declarations with no failed declarations or linter warnings. No Lake command was run.

The remaining existence theorem is genuinely broad: it needs TN-preserving Neville/Whitney elimination with pivot positivity and minor control, a finite elimination invariant yielding the block form [1] ⊕ S₁, the transpose elimination phase, and diagonal symmetrization. The alternative Gantmacher--Krein route needs the absent compound irreducibility/positive-principal-minor and eigenvector nodal package. I am stopping at the checked algebraic leaf rather than adding a theorem-shaped scaffold or broad unrelated matrix theory.