Prove the compound eigenvalue theorem - #411
Closed
PerAlexandersson wants to merge 8 commits into
Closed
Conversation
Formalizes the engine of the positive-recurrence route for sequences whose generating function rearranges into a strictly positive recurrence with partial sums, of the shape A n = A (n-2) + A (n-3) + c * X * S (n-4), S n = S (n-1) + A n, c > 0. partialSum_step: if the partial sum S interlaces both plain terms A1 and A2, then A1 + A2 + c * X * S is real-rooted and precedes X * S. The proof composes three results that were already present: the degree shift prec_to_prec_mul_X_of_nonneg turns S < A_i into A_i < X * S, the two-term right cone prec0_add_left_of_common_right_of_nonneg gives A1 + A2 < X * S, and prec_nonneg_combo_right together with isRealRooted_nonneg_combo_of_prec finishes. partialSum_step_left gives the other half of the sandwich, A1 + A2 < A1 + A2 + c * X * S. Recorded separately and with an explicit hypothesis because prec_nonneg_combo_left requires the two summands to be coprime; that is a genuine extra condition which applications must supply, not something the cone argument provides for free. Motivated by A275442, whose generated definition has the negative factor (2X - 1); ProofsOeis/A275442.lean is owned by another worker, so nothing there is touched and this contributes only the reusable general step. No sorry and no axiom; the full RealRooted target builds with zero warnings. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Adds RealRooted/Mathlib/LinearAlgebra/Matrix/Triangularize.lean: - `Matrix.exists_mulVec_eq_smul`: a matrix over an algebraically closed field has an eigenvector (charpoly root -> singular pencil -> kernel vector); - `Matrix.exists_unitsConj_blockTriangular`: every square matrix over an algebraically closed field is conjugate to an upper triangular matrix, the triangular shape witnessed by an injective height function `b : m -> N`, so no linear order on the index type is required. The induction conjugates by `1.updateCol i0 v` (invertible since its determinant is `v i0`, via `cramer_one`) to clear the eigencolumn, then splits the index type with `Equiv.sumCompl` and recurses on the complement block; all block bookkeeping is `Matrix.fromBlocks` algebra plus `submatrix_mul_equiv`. This is the missing keystone for the compound eigenvalue theorem (#405 item 3) and, downstream, Gantmacher-Krein (#394). Mathlib currently has no matrix-level triangularization; the file mirrors the Mathlib tree for upstreaming. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Formalize the coupled partial-sum induction step
Add compound matrices: multiplicativity and entrywise nonnegativity
Triangularize matrices over an algebraically closed field
Closes the mathematical content of issue #405: over an algebraically closed field there is an enumeration mu of the eigenvalues of A (with multiplicity) such that for every q the characteristic polynomial of `compound q A` is `prod_s (X - C (prod_{i in s} mu i))` over the increasing q-selections. Pure assembly of the two merged halves plus one new ingredient: - triangularize A (`exists_unitsConj_blockTriangular`, #410); - sort the height function of the triangular form into the index order by a permutation-matrix conjugation (`Tuple.sort` + `permMatrixHom.toHomUnits` + `PEquiv.toMatrix_toPEquiv_mul` / `PEquiv.mul_toMatrix_toPEquiv`); - read off the compound charpoly of the sorted triangular form (`charpoly_compound_of_blockTriangular`), transporting along both conjugations with `charpoly_compound_conj` and `charpoly_units_conj`. This is the spectral input Gantmacher-Krein (#394) consumes: TN matrices have entrywise nonnegative compounds, so Perron-Frobenius (#404) on each compound controls the eigenvalue products. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
This was referenced Aug 21, 2026
Owner
Author
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Stacked on #409 (and merges main for #410). Closes the mathematical content of #405.
Matrix.exists_charpoly_compound_eq_prod: over an algebraically closed field,∃ μ : Fin n → K, A.charpoly = ∏ i, (X - C (μ i)) ∧ ∀ q, (compound q A).charpoly = ∏ s : Set.powersetCard (Fin n) q, (X - C (∏ k, μ (powersetEnum s k)))— the eigenvalues of the
q-th compound are exactly theq-fold products ofthe eigenvalues of
A, with multiplicity.Assembly: triangularize (#410) → sort the height function into the index order
by a permutation-matrix conjugation (
Tuple.sort,permMatrixHom.toHomUnits,PEquiv.toMatrix_toPEquiv_mul/mul_toMatrix_toPEquiv) → read off the compoundcharpoly of the triangular form (#409), transporting along both conjugations
via
charpoly_compound_conjand Mathlib'scharpoly_units_conj.With this, #394 (Gantmacher–Krein) needs only Perron–Frobenius (#404) plus glue.
Sorry-free.
🤖 Generated with Claude Code