Skip to content
BranchesTags

Repository files navigation

RealRooted

Proof assumptions and refuted legacy interfaces are summarized in PROOF_STATUS.md.

RealRooted is an experimental Lean 4 library for real-rooted univariate polynomials, interlacing, compatibility, Polya-frequency sequences, and related combinatorial applications.

Browse the theorem and definition catalog. It presents a curated overview of completed results, with readable statements, Lean declarations, references, and links to the corresponding source.

The repository is a research formalization workspace rather than a polished mathlib contribution. The useful part is that the named theorem declarations below are checked by Lean, and the surrounding files give searchable proof infrastructure for real-rootedness and interlacing arguments. The long-term goal is to extract stable, reusable components for eventual upstreaming.

Table of Contents

Build

The project uses Lean 4.34.0 and Mathlib v4.34.0 through Lake.

lake exe cache get
lake build

The default build checks the historical broad umbrella together with the production-only and tactic-regression entry points. They can also be checked individually:

lake build RealRooted.Production
lake build RealRooted.Tactic.Examples

In the Lean 4.34 port, the local list operation is named List.interleaveRight: it starts with the right list and truncates when that list is empty. Batteries now provides a different List.interleave, which starts with the left list and retains leftovers. The List.Interleaves relation keeps its existing meaning; operation-specific helper lemmas use the interleaveRight spelling. List sign variations now use Mathlib's identical definition instead of a duplicate local declaration. The core Matrix.IsTotallyNonneg API likewise comes from Mathlib now; the local shim retains rectangular minors and the additional matrix lemmas. Its scalar-multiplication theorem infers the scalar from the positivity certificate, so callers use hM.smul hc rather than hM.smul c hc.

Useful focused checks for recent theorem areas are:

lake build RealRooted.CommonInterleaverTwo
lake build RealRooted.ChudnovskySeymour
lake build RealRooted.Hadamard
lake build RealRooted.VeroneseMatrix
lake build RealRooted.VeroneseSection
lake build RealRooted.Bezoutian

For an independent kernel re-check and axiom audit of the small comparator surface, use ./verify.sh on x86_64 Linux. The script downloads and caches the pinned comparator, exporter, sandbox, and independent Rust kernel listed in comparator/versions.env. On another host platform, or for a clean Ubuntu environment, use ./verify_docker.sh; non-x86_64 hosts require Docker's amd64 emulation. These scripts complement lake build; they do not replace it.

Repository Layout

  • ARCHITECTURE.md records the intended dependency layers, import budgets, module-splitting rules, and consumer-to-library extraction workflow.
  • RealRooted.lean is the broad compatibility umbrella for the full public development.
  • RealRooted/Production.lean imports every non-regression module and excludes RealRooted.Tactic.Examples and its leaves.
  • RealRooted/Tactic/Examples.lean is the mandatory regression umbrella and retains every historical example import path.
  • RealRooted/Basic.lean, Derivative.lean, Wagner*.lean, and InterlacingSequence*.lean contain the core interlacing API.
  • RealRooted/Wronskian/ separates polynomial Wronskian algebra, forward and converse Bezoutian bridges, and successor-degree sign/interlacing results; Wronskian.lean is its focused public entry point.
  • RealRooted/CommonInterleaver*.lean and ChudnovskySeymour.lean contain the compatibility and common-interleaver work.
  • RealRooted/AissenSchoenbergWhitney.lean, PFPolynomial.lean, VeroneseSection.lean, and VeroneseMatrix.lean contain the PF, Toeplitz, and Veronese-section material.
  • RealRooted/LGV/ connects finite ranked-path networks to strict Toeplitz minors and Pólya-frequency sequences without duplicating LeanLGV's checked path-cancellation engine. Its repeated-chip endpoint certifies finite G * (K * G) ^ q kernel rows directly from nonnegative lower-bidiagonal factorizations. RealRooted/BrandenLeite/ packages the corresponding finite kernel rows, two-kernel composition rows, and stationary or position-dependent tiling specializations.
  • VeroneseSectionPair.lean gives strict proper position for two nonzero ordered residues; its HermiteBiehler child gives the induced upper-half-plane and Hurwitz stability certificates.
  • RealRooted/Hadamard/Product.lean contains the elementary coefficientwise product API; GarloffWagner/Algebra.lean owns the factorial-normalized Schur-product and differential-operator algebra, and GarloffWagner/Iterated.lean owns the J^k ∘ L Theorem 11 transport. GarloffWagner/KreinData.lean owns the root-multiplicity and divisibility data for the later Krein expansion. GarloffWagner/KreinExpansion.lean owns the positive root-deleted expansions and their Theorem 11 proper-position consequences. GarloffWagner/Theorem12.lean owns the factorial Schur-product induction and its fixed-factor Hadamard consequences, while GarloffWagner/Hadamard.lean owns the double-deleted reduction and final two-pair endpoint. GarloffWagner.lean remains their theorem-route compatibility import. Hadamard/Basic.lean owns the coefficient-support and Schur--Szego composition algebra, including the Jensen and degree-three identities; Hadamard/Finite.lean, Newton.lean, and Cubic.lean respectively own the finite-composition interfaces, normalized Newton inequalities, and degree-three reductions. Hadamard/Grace.lean owns the apolar/Grace proof, followed by GarloffWagner.lean, Hurwitz.lean, and Consequences.lean for the endpoint interfaces. Hadamard.lean is their compatibility import.
  • MultiplierSequence/PolyaSchur/Factorial.lean identifies factorial-weighted coefficient Jensen polynomials with Garloff--Wagner Schur products, while Limit.lean proves pointwise closure of PF multiplier sequences. MultiplierSequence/Sign.lean proves the zero-safe parity sign constraint and the four classical PF sign normalizations for arbitrary multiplier sequences. LaguerrePolya/TypeIReverse.lean combines these facts with locally uniform derivative convergence to prove the reverse Type-I Pólya--Schur bridge from Taylor data, and the exponential-generating-function classification under its necessary positive-radius hypothesis.
  • BorceaBranden/Applications/BidiagonalSymbol.lean computes genuine affine finite symbols for coefficient-bidiagonal operators; its RealConsequences child supplies their real preservation consequences, and EulerFiniteSymbol.lean packages the stable Euler-family specialization with diagonal constant c ≥ 1.
  • RealRooted/GammaPencil/ develops the A16634x gamma operator from its coefficient recurrence and exact finite symbol through degree-box preservation and the all-rank oriented gamma-pencil theorem.
  • RealRooted/SymmetricDecomposition/ separates the Brändén--Solus definitions, f-polynomial transport, symmetric-decomposition, and Theorem 2.6 layers; SymmetricDecomposition.lean remains their compatibility import. Bezoutian.lean contains the classical Bezoutian interface.
  • RealRooted/RowThreshold.lean contains the row-threshold preserver. ThresholdMatrix/Basic.lean owns the generic threshold-matrix API, while its HaglundZhang and GustafssonSolus children own the two independent application backends. ThresholdMatrix.lean remains their compatibility import. Shared constant and positive-slope affine proper-position lemmas live in AffineProperPosition.lean rather than in a Veronese-specific module.
  • RealRooted/NarayanaTransformation/ layers the Mao--Wang Narayana transformation by root geometry, basis transforms, factorial preservation, coefficient identities, rectangular convolution, recurrences, and endpoints; NarayanaTransformation.lean remains its compatibility import. LowerTriangularMatrix.lean and MaoWangMatrixProduct.lean provide the lower-triangular row-generating-function API and matrix-product endpoint wrappers.
  • RealRooted/ParkingFunctions/ToricContribution/ layers the public A390883 backend from shifted-Jacobi and interval-insertion infrastructure through the finite and exceptional offsets, coefficient reversal, fixed-row pairwise interlacing, and the common-interlacer weighted-sum endpoint.
  • RealRooted/EulerOperator/Darboux/ provides the coefficient-ring algebra of the unit-interval Darboux operator and a separate ordered interlacing layer; the toric insertion operator is a compatibility alias for this API.
  • RealRooted/Mathlib/RingTheory/Polynomial/Jacobi/DifferentialOperator.lean owns the generic shifted-Jacobi differential operator, while RealRooted/Jacobi/DifferentialOperator.lean supplies its shifted-Euler and Jacobi ODE identities. The family-neutral simple-root and derivative- elimination lemmas live in RealRooted/Mathlib/Algebra/Polynomial/DifferentialEquation/SecondOrder.lean.
  • RealRooted/Jacobi/Orthogonality.lean proves full two-parameter shifted- Jacobi orthogonality from Gamma moments and a coefficient-ring moment- recurrence API. Its Orthogonality/Integral.lean child identifies that pairing with the beta-weighted integral, keeping analytic imports out of the finite Jacobi family and root theory. Jacobi/Favard.lean owns the monic three-term recurrence certificate, and the orthogonality layer identifies its concrete moment pairing with the normalized Favard pairing. The beta-zero and beta-one modules retain their historical rational APIs as compatibility specializations.
  • RealRooted/JacobiDeformation/ proves the root theory of the Jacobi deformation J_{m,δ}^{c,d}(X, U, V) by a finite algebraic argument: a diagonal Jacobi kernel expansion, entrywise positivity of a quasi-Jacobi collocation matrix, the Micchelli--Willoughby spectral-product theorem in RealRooted/SpectralProduct.lean, and critical-point signs. JacobiDeformation.lean is its facade. RealRooted/Applications/OEIS/A132885.lean specializes it to the central-trinomial rows of OEIS A132885, using Nat.centralTrinomial from RealRooted/Mathlib/Combinatorics/Enumerative/CentralTrinomial.lean.
  • RealRooted/RootVieta/Newton.lean exposes Newton recurrences for multisets, ordinary polynomial roots, and reversed polynomial roots. Its Mathlib-shaped shims evaluate multivariate power sums and orient Vieta formulas for direct reuse; no degree-specific power identities are stored in the library.
  • RealRooted/LiuOppositeSigns/RootCount.lean contains Liu's threshold-count foundation, RootDeletion.lean contains the general cofactor and largest-root deletion API, and PositiveSplitRootCount.lean packages the normalized positive-leading pair. LiuOppositeSigns.lean retains the cross-owned-gap and left/right branch interface, with LiuOppositeSignsTheorem.lean providing the theorem endpoint. Its XSub/ProperPosition.lean child exposes the ordinary StrictInterl bridge and the nonnegative X * p - μ * q splitness corollary. Its XSub/IntervalRootCount/ package separates root filters, adjacent gaps, exterior tails, count-to-splitting endpoints, and the three degree cases; XSub/IntervalRootCount.lean remains the compatible import. Its XSub/CubicCubic/ package similarly separates cubic-minus-quadratic infrastructure, normalized setup, root-order case families, repeated-root boundaries, and the degree-three endpoints; XSub/CubicCubic.lean remains the compatible import.
  • RealRooted/Favard/Affine/ separates direct positive-slope recurrences, scalar-denominator normalizations, and row-sign normalizations; its parent Favard/Affine.lean is the focused theorem import, while Tactic/Favard.lean is the compatible frontend façade over its focused syntax and macro-rule modules. Favard/Recurrence.lean owns the ring-generic monic recurrence and polynomial-basis API. Favard/Orthogonality.lean constructs its normalized functional and product pairing, proving basis orthogonality, the norm recurrence, nondegeneracy, positive definiteness, and uniqueness up to scaling.
  • RealRooted/Mathlib/RingTheory/Polynomial/Laguerre/ defines the canonical monic sign-reversed generalized Laguerre family and its algebraic identities. RealRooted/Mathlib/Algebra/Polynomial/Moment.lean provides the reusable moment-functional and pairing algebra for its orthogonality theory and other classical polynomial families. RealRooted/Laguerre/Favard.lean owns the three-term recurrence certificate; the family separately packages roots/interlacing and algebraic or integral orthogonality, including the bridge from the concrete moment pairing to the normalized Favard pairing. RealRooted/Laguerre.lean is the family facade.
  • RealRooted/Mathlib/RingTheory/Polynomial/Hermite.lean extends Mathlib's canonical probabilists' Hermite family with the lowering identity and monic three-term recurrence. RealRooted/Hermite/Favard.lean maps that family to arbitrary coefficient rings and supplies the real Favard certificate; Hermite/Roots.lean packages real-rootedness, consecutive interlacing, simple roots, and Sturm sequences. Hermite/Orthogonality.lean owns the normalized algebraic pairing with squared norms n!, while its Integral child alone imports analysis and identifies that pairing with the Gaussian weight exp (-(x² / 2)). RealRooted/Hermite.lean is the family facade.
  • RealRooted/Mathlib/RingTheory/Polynomial/ShiftedLegendre.lean identifies Mathlib's integer shifted Legendre family with the zero-parameter shifted Jacobi family after mapping to the reals. Legendre/Basic.lean exposes that canonical map and its reflection through the origin, while Legendre/Roots.lean packages degree, root-location, simple-root, and consecutive-interlacing theory in both orientations. The reflected family is the reusable positive-leading normalization behind the A080721 auxiliary Legendre polynomials; the actual OEIS family remains a distinct local quasi-Legendre combination. RealRooted/Legendre.lean is the family facade.
  • RealRooted/GeneralizedSnakePosets.lean contains theorem-shaped interfaces for the Braun-Jal generalized snake poset target.
  • RealRooted/Challenges/ contains compact entry points for famous theorem statements. Opted-in module comments are the maintained source for the public challenge catalog, including its human-readable descriptions and primary references.
  • RealRooted/CombinatorialExamples/ contains examples such as Eulerian, type B Eulerian, simsun, Touchard, Narayana, Motzkin, and related families.
  • RealRooted/Tactic/OEIS_COVERAGE.md is the generated coverage ledger for OEIS-labeled tactic shells, certificate fragments, and concrete theorems.
  • RealRooted/Tactic/OEIS/ contains focused OEIS certificate-family frontends. DerivativeLag.lean, PositiveLag.lean, and NegativeLag.lean own the lag families, while ProductExit.lean, ProductFactor.lean, ProductLift.lean, and ProductParity.lean own product certificates. Tactic/OEIS.lean remains the compatible umbrella import.
  • RealRooted/Mathlib/ contains local compatibility lemmas intended to look like future Mathlib additions.

Main Concepts

  • Interlaces f g, StrictInterl f g, and Interl f g: the main strict, oriented, and zero-aware interlacing relations.
  • p = 0 ∨ p.Splits: the zero-aware real-rootedness convention used in closure statements where the zero polynomial is a natural exceptional case.
  • IsGeneralizedSturmSeq ps, IsInterlacingSeq fs, and IsInterlacingSeq0 fs: list-level Sturm and interlacing predicates.
  • Compatible f g, PairwiseCompatible fs, and FamilyCompatible fs: Chudnovsky-Seymour style compatibility predicates.
  • HasCommonInterleaver fs and HasCommonLeftInterleaver fs: common interleaver data for finite families.
  • AllComboRealRooted f g: every real linear combination of f and g is zero or real-rooted.
  • IsPolyaFreqSeq a: total nonnegativity of the Toeplitz matrix of a sequence.
  • veroneseSectionPolynomial r k p: the fixed-residue Veronese section of a polynomial.
  • FullyInterlacingPair a b: the two-row Lace total-nonnegativity interface used by the Veronese development. Its proposed identification with Hurwitz stability is false for the current row orientation.

Checked Highlights

Every declaration named in this section is a checked Lean declaration. Any open proposition scaffold is explicitly labeled and tracked in PROOF_STATUS.md; the project does not use sorry stubs.

Theorem-Level Highlights

The formalization now contains theorem interfaces for several standard real-rootedness and interlacing results. In ordinary mathematical language, the checked or challenge-facing highlights are:

  • Cauchy interlacing: the eigenvalues of a principal codimension-one submatrix of a real symmetric or Hermitian matrix interlace the eigenvalues of the original matrix, with a reusable characteristic-polynomial bridge in RealRooted.CauchyInterlacing.Polynomial. See cauchy_interlacing and RealRooted.Challenges.CauchyInterlacing; references include Fisk (2005) and Godsil (2017).
  • Oscillatory interlacing: Whitney reduction and tridiagonal matrix theory live in RealRooted.Mathlib.LinearAlgebra.Matrix.OscillatoryInterlacing.Core, while RealRooted.OscillatoryInterlacing combines that core with Cauchy interlacing to prove strict interlacing of consecutive principal-section characteristic polynomials.
  • Totally nonnegative principal interlacing: every finite real totally nonnegative matrix has weak leading- and trailing-principal characteristic- polynomial interlacing, including singular matrices. See Matrix.IsTotallyNonneg.leading_charpoly_interlaces and Matrix.IsTotallyNonneg.trailing_charpoly_interlaces in RealRooted.TotallyNonnegInterlacing.
  • Wagner's lemma: for real-rooted polynomials with nonpositive roots and positive leading coefficients, common interlacers are closed under addition, and multiplication by X shifts the interlacing relation in the expected way. The reusable forms live in RealRooted.Wagner.NonpositiveRoots, with challenge-facing aliases in RealRooted.Challenges.Wagner; reference: Wagner (1992).
  • Obreschkoff's theorem: two polynomials have a real-rooted real pencil alpha * f + beta * g if and only if they interlace, up to orientation and degree conventions. See allComboRealRooted_of_strictInterl, strictInterl_of_allComboRealRooted, and RealRooted.Challenges.Obreschkoff; references include Obreschkoff (1963), Dedieu (1992), and Branden (2004).
  • Interlacing preservers: a linear operator that preserves real-rootedness sends interlacing pairs to interlacing pairs, up to the zero and orientation conventions used by Interl. See operatorPreservesInterlacingPairsUpToOrder and RealRooted.Challenges.OperatorPreservers; reference: Branden (2004).
  • Matrix preservers: a polynomial matrix with nonnegative coefficients preserves interlacing sequences when its two-by-two affine tests interlace. See matrix_preserves_interlacing_seq and RealRooted.Challenges.MatrixInterlacing; Fisk (2006) develops matrices preserving interlacing, and Branden (2015) gives the exact criterion used here.
  • Favard interlacing: a three-term Favard recurrence with positive recurrence coefficients gives a Sturm sequence, hence every polynomial in the sequence is real-rooted. See favardInterlacing and RealRooted.Challenges.Favard; reference: Favard (1935).
  • Polya-frequency and Veronese results: the ASW reverse direction and the Toeplitz/PF infrastructure imply that Veronese sections of a real-rooted polynomial with nonnegative coefficients are real-rooted or zero. See aissenSchoenbergWhitney_reverse, isRealRootedOrZero_veroneseSectionPolynomial_of_realRooted_nonneg_matrix, and RealRooted.Challenges.VeroneseSections; references include Aissen--Schoenberg--Whitney (1952) and Athanasiadis--Wagner (2024).
  • Eulerian examples: ordinary Eulerian and type B Eulerian polynomials are real-rooted, and the formalization proves stronger consecutive interlacing or Sturm-sequence statements. See RealRooted.Challenges.Eulerian; references include Frobenius (1910).
  • Toric contributions for A390883: each fixed row is an oriented all-pairs interlacing sequence, the normalized reverse-offset family has a common left interleaver, and every strictly positive weighted normalized sum is real-rooted. See toricContributionRow_isInterlacingSeq, normalizedRPolynomialFamily_hasCommonLeftInterleaver, and normalizedRPolynomialFamily_weighted_sum_splits; reference: Xiao (2026).
  • Graph polynomials: finite claw-free graphs have real-rooted independence polynomials, and matching-polynomial corollaries are packaged through the line-graph reduction. See Graph.clawFree_indepPoly_splits and RealRooted.Challenges.ChudnovskySeymour; references include Chudnovsky--Seymour (2007) and Heilmann--Lieb (1972).
  • Mao--Wang Narayana transformation: the formalization proves the Narayana transform preserves PF polynomials and packages the lower-triangular matrix-product criterion for admissible affine, Touchard/Stirling, rising-factorial, and Narayana matrix factors. See narayanaTransformPreservesPF, LowerTriangularMatrix.maoWang_matrixProduct_rowGeneratingFunctions_pf, and LowerTriangularMatrix.maoWang_matrixProduct_rowGeneratingFunctions_nonposRoots; reference: Mao--Wang (2026).
  • Jacobi deformation and A132885: for 0 < δ < 1 and positive parameters, the Jacobi deformation J_{m,δ}^{c,d}(X, U, V) has m simple strictly negative roots and is strictly interlaced by the derivative of J_{m,0}; for every δ ≥ 0 it splits with strictly negative roots. Consequently every nonconstant row ∑_k C(n - k, k) T(n - 2k) X ^ k of OEIS A132885, with central trinomial coefficients T, has exactly n / 2 simple negative roots. See JacobiDeformation.polynomial_strict_package, JacobiDeformation.polynomial_all_rank_nonneg_parameter, and Applications.OEIS.A132885.splits_simple_roots_neg; the spectral step uses Micchelli--Willoughby (1979).

The challenge surface also records theorem-shaped targets as they mature. Kurtz's coefficient inequality criterion is implemented in RealRooted.Kurtz and re-exported by its challenge entry point. The finite Hermite--Poulain differential-operator preserver is implemented in RealRooted.Hermite.Poulain over the shared RealRooted.Derivative.LinearCombination theorem layer. The full finite complex Borcea--Branden classification, including its stable rank-at-most-one branch, is implemented in RealRooted.BorceaBranden.FiniteSymbolClassification; its low-dependency real-univariate interface lives in RealRooted.BorceaBranden.UnivariateFiniteSymbol. The challenge entry point re-exports both APIs.

Interlacing And Preservers

  • derivative_interlaces: Rolle-style derivative interlacing for real-rooted polynomials.
  • StrictInterl.add_of_right_of_posLeadingCoeff, StrictInterl.add_of_left, and interl_mul_X_of_interl: checked Wagner-lemma forms for common interlacers and multiplication by X.
  • strictInterl_ma_wang and generalizedLiuWangCriterion: Ma-Wang and Liu-Wang style criteria for interlacing recurrences and weighted sums.
  • favardInterlacing and isRealRooted_of_favard: a Favard recurrence interface for orthogonal-polynomial style Sturm sequences.
  • SatisfiesFavardRecurrence.pairing_iIsOrtho, SatisfiesFavardRecurrence.pairing_nondegenerate, and SatisfiesFavardRecurrence.pairing_posDef: the normalized algebraic Favard functional and pairing, with orthogonality, nondegeneracy, and positivity.
  • generalizedLaguerre_splits, generalizedLaguerre_hasSimpleRoots, and generalizedLaguerre_integral_orthogonal: the root, Sturm, and classical orthogonality package for the canonical generalized Laguerre family.
  • matrix_preserves_interlacing_seq and matrix_preserves_interlacing_seq0_of_2x2: matrix preservers from finite two-by-two interlacing checks.
  • operatorPreservesInterlacingPairsUpToOrder: a general operator-preserver interface for interlacing pairs.
  • cauchy_interlacing: Cauchy's eigenvalue interlacing theorem for Hermitian matrices and one-index principal submatrices.
  • gwHadamardProductNonnegInterl: the Garloff--Wagner interlacing theorem for coefficientwise Hadamard products of nonnegative real-rooted pairs.

Compatibility And Common Interleavers

  • hasCommonInterleaver_of_pairwiseHasCommonInterleaver: pairwise common interleavers imply a global common interleaver.
  • isRealRooted_sum_of_commonInterleaver and isRealRooted_sum_of_commonLeftInterleaver: nonnegative sums are real-rooted when a family has common interleaver data.
  • familyCompatible_of_commonInterleaver and pairwiseCompatible_of_familyCompatible: the easy directions relating common interleavers and compatibility.
  • Declarations with prefix chudnovskySeymour_fourWay_of_: several checked Chudnovsky-Seymour four-way packages under formalized bridge hypotheses.
  • pairwiseCompatible_iff_familyCompatible_of_natDegree_le_one: the complete low-degree compatibility equivalence.

Symmetric Decomposition And Bezoutians

  • idDecompositionExistsUnique and rdDecompositionExistsUnique: existence and uniqueness of the Branden-Solus symmetric decompositions.
  • brandenSolusTheorem26: the formalized Branden-Solus Theorem 2.6 package in the canonical interlacing language.
  • isRealRooted_fPolynomial_of_isRealRooted_of_hasNonnegCoeffs: real-rootedness preservation for the h -> f transform in the nonnegative setting.
  • strictInterlSameDegree_iff_bezoutMatrix_posDef: strict same-degree Bezoutian characterization.

Polya Frequency, ASW, And Veronese Sections

  • aissenSchoenbergWhitney_reverse: the reverse Aissen-Schoenberg-Whitney direction, from real-rooted nonpositive roots and nonnegative coefficients to a Polya-frequency coefficient sequence.
  • isPFMultiplierSequence_iff_isLaguerrePolyaTypeI_complexExpGeneratingFunction: the Type-I Pólya--Schur classification for exponential generating series with positive radius of convergence.
  • IsMultiplierSequence.exists_pf_sign_normalization: every multiplier sequence is PF after identity, global negation, alternation, or negated alternation, including arbitrary internal zero gaps.
  • isMultiplierSequence_iff_isLaguerrePolyaTypeISigned_complexExpGeneratingFunction: the full signed Type-I classification under the necessary positive-radius hypothesis; isLaguerrePolyaTypeISigned_neg_exp is a concrete signed specialization.
  • aissenSchoenbergWhitneyForward: the target theorem for the opposite ASW direction.
  • Quiver.Path.sum_weight_exactLength_eq_edgeSumMatrix_pow: exact-length weighted path sums are entries of powers of the edge-sum matrix.
  • StrictToeplitzMinorIndex.pathNetwork_matrix_eq_toeplitzSubmatrix and isPolyaFreqSeq_of_minorOrderedCertificates: the source-row/sink-column orientation bridge and minor-local ordered-LGV endpoint for proving a sequence Pólya-frequency.
  • BrandenLeite.coeff_kernelRow and BrandenLeite.natDegree_kernelRow_le_row: the exact coefficients and sharp row support of the finite kernel polynomial G * (K * G) ^ q for lower G and strictly lower K.
  • LGV.RepeatedChip.kernelSequence_isPolyaFreqSeq and LGV.RepeatedChip.kernelRow_isPFPolynomial: ordered-LGV certificates for nonnegative repeated chip words; natDegree_kernelRow_le_div records the sharper bound when every marked pass drops at least r levels.
  • BrandenLeite.twoKernelRows_pf_and_interl and BrandenLeite.rationalRodRows_pf_and_interl: checked PF/interlacing endpoints for composition rows and factored stationary rod-tiling kernels.
  • IsPolyaFreqSeq.veroneseSectionSeq and IsPolyaFreqSeq_veroneseSectionPolynomial_coeff: Veronese subsequences and Veronese section coefficients preserve Toeplitz total nonnegativity.
  • isRealRootedOrZero_veroneseSectionPolynomial_of_realRooted_nonneg_matrix: the completed cyclic-matrix proof that Veronese sections of a real-rooted nonnegative-coefficient polynomial are zero or real-rooted.
  • not_isUpperHalfPlaneStable_hermiteBiehlerPolynomial_X_neg_one: a checked counterexample documenting why the Hermite-Biehler forward route is exposed only in sign-normalized form.
  • gammaU_strictInterl_gammaV and gammaU_add_C_mul_gammaV_splits: the directed interlacing and all-real-parameter splitness endpoints for the A16634x gamma pencil in every rank at least two.

Combinatorial Examples

The example files prove real-rootedness and, in many cases, Sturm or interlacing sequence statements for standard combinatorial families. Representative declarations include:

  • isRealRooted_eulerianTilde
  • isRealRooted_typeBEulerian
  • isRealRooted_simsun
  • isRealRooted_touchard
  • isRealRooted_coloredSetPartitions
  • isRealRooted_narayana_of_nonnegCoeffs
  • isRealRooted_motzkin
  • peakValuePolynomial_mvRealStable: the peak-value enumerator of permutations is multivariate real stable in every rank.
  • peakValueWeightedDiagonal_consecutive_strictInterl: positive weighted diagonal specializations of consecutive peak-value enumerators strictly interlace (the weighted A008303 application).

Current Roadmap

The Chudnovsky-Seymour and Heilmann-Lieb graph-facing line is now represented by checked theorem interfaces in ChudnovskySeymour.lean and HeilmannLieb.lean. The graph endpoint is Graph.clawFree_indepPoly_splits: finite claw-free graphs have real-rooted independence polynomials. The matching-polynomial corollaries are packaged through the line-graph reduction in HeilmannLieb.

Garloff--Wagner Hadamard proper-position is now proved directly in RealRooted.GarloffWagner and exposed through garloffWagnerHadamardNonnegInterl. It no longer remains as an external standard fact for the SuperEulerian project.

The Braun--Jal generalized-snake development now checks the recurrence, Liu--Wang proper-position, Claim 7, matrix-induction, real-rootedness, and interlacing deductions. The public route is theorem41NonNestingRook_modified_of_modelInputs. The paper's board-model identities and the Stanley / Alexandersson--Jal h^*-to-rook correspondence remain explicit combinatorial inputs. In particular, the development does not claim an unconditional theorem for an arbitrary polynomial family satisfying only the statement-interface type; issue #71 tracks the remaining theorem proof.

Documentation and onboarding use concise challenge entry-point files in RealRooted/Challenges/. This directory is a positive ledger of completed results: every theorem challenge must have an unconditional checked witness. Incomplete theorem targets and strategy surfaces belong in open GitHub issues, not in challenge modules. An explicit metadata block opts a completed module into the generated public catalog; only selected definitions and checked theorem declarations are published. Conjectures, examples, and statement scaffolds are not catalog entries. The same bounded module comment owns the explanatory prose and primary references, while detailed proof infrastructure remains in the main theorem modules. A symmetricfunctions.com link may provide useful context but is not required. The current challenge surface includes ASW, Chudnovsky-Seymour, Leake-Ryder same-phase stability, Hadamard, Wagner, Cauchy interlacing, Obreschkoff, operator and matrix interlacing preservers, Hermite-Biehler, the checked row-oriented Hurwitz counterexamples, Veronese sections, Favard, Kurtz, Hermite-Poulain, Borcea-Branden, and Eulerian polynomials.

The finite complex Borcea--Branden classification is checked using the multivariate stability and polarization infrastructure in this repository, with applications importing its reusable theorem modules rather than the challenge facade. The A16634x gamma-pencil roadmap is complete through its exact parity symbol, finite degree-box preserver, and all-rank oriented proper-position theorem. Further stability work may revisit the correctly oriented classical Hurwitz matrix and its stability criterion; both directions proposed for the current row-oriented matrix are formally refuted.

The Brändén--Saud Leite program is complete through the canonical Whitney resolution of lower-unitriangular totally nonnegative matrices, the chain-polynomial splitting and consecutive-interlacing theorem, zero-constant composition rows, the two-kernel PF/interlacing theorem, stationary and position-dependent tiling recurrences, and the independent repeated-chip LGV certificate.

GitHub issues track individual proof tasks rather than being duplicated here. Current open themes include the Braun--Jal generalized-snake-poset theorem, the Hoster--Stump Chow-polynomial strategy, classical root-counting foundations, infinite PF and transcendental stability classifications, and selected stable-polynomial and combinatorial applications. Liu's opposite-leading-sign theorem is checked as compatible_iff_theorem21RootCountBranchesWithCommon_nonconstant, with the necessary explicit common-root branch; its formerly proposed weaker interface has a checked counterexample. Recent checked issue surfaces include the Braun--Jal route described above, the Gustafsson--Solus interlacing recursion, the Haglund--Zhang s-inversion/A046802 backend, characteristic-polynomial packaging for Cauchy interlacing, and the finite Borcea--Branden symbol classification. The A390883 toric-contribution conjecture is also closed by the stronger fixed-row interlacing and common-interlacer results listed above.

Development Notes

The project does not accept sorry, admit, or source axiom commands as proofs. Track an unproved conjecture in a GitHub issue. If a temporary ...Statement : Prop interface is genuinely useful, list it in PROOF_STATUS.md, document that it is an unproved target, and keep it out of production theorem dependencies. Known false candidate interfaces are retained only when useful for diagnosis, together with checked negations. Any reduction through such an interface must expose it as an explicit hypothesis and document that the route is uninhabited.

New Lean code should follow the Lean community style guidelines and Mathlib naming conventions where practical. In particular, keep declarations explicit, prefer small reusable lemmas, and keep top-level declarations flush-left. The CI import guards check the broad, production, and regression umbrellas separately and reject production closures containing tactic examples. Run python3 scripts/check_root_imports.py --fix to append a new module only to its owning umbrellas; existing qualified imports and comments are preserved.

Proof-surface CI is checked separately with:

python3 scripts/check_proof_status.py --self-test
python3 scripts/check_proof_status.py

The guard rejects sorry, admit, and source axiom commands, the tactic rules below, and reports low-use theorem-shaped propositions that still need an explicit status in PROOF_STATUS.md.

All code accepted into the default branch must build without warnings. The lakefile sets warningAsError, so lake build fails on any warning. Draft branches may use the CI-first verification workflow below.

To maintain clean and reliable build verification, the use of set_option is forbidden in the codebase. All warnings, lint errors, or resource limits should be addressed by refining the underlying proofs and definitions rather than suppressing them.

To ensure proofs are deterministic and maintainable, the use of try, all_goals, and any_goals tactics is forbidden in proofs (they remain permitted inside macro, macro_rules, elab, and elab_rules tactic implementations). Proofs should use structured casing or sequential composition instead. Similarly, simp +decide and simp_all +decide are forbidden. Use lia instead of omega; a goal that lia cannot close may use omega only when its declaration is listed in ALLOWED_OMEGA in scripts/check_proof_status.py.

Please keep repository configuration files (like lakefile.toml and lake-manifest.json) free of hardcoded absolute paths such as /lake-cache/projects/.... Reusable relative repository paths (e.g. .lake/packages and .lake/build) ensure that the builds work out-of-the-box in local developer environments.

CI and PR Policy

Small, independently owned changes may use a CI-first draft PR: run the applicable source checks, commit to a feature branch, and push a draft PR for GitHub-hosted compilation. A local full build is not a prerequisite for that draft checkpoint. State clearly which checks have and have not run; a draft commit is not a verified theorem milestone.

Parallel workers must use isolated branches/worktrees and disjoint file ownership. Keep builds against a shared local Lake cache serialized; isolated GitHub-hosted runners can validate PRs independently. One integrator reviews the theorem statements, assumptions, source changes, and verification results.

Before merging, require successful proof validation of the exact candidate revision: all source guards, the ordinary default build (including Production and tactic regressions), and applicable transitive-axiom checks. The separate Comparator audit covers only its explicitly listed theorem surface. After a rebase or integration change, rerun the relevant checks; never treat cancelled, skipped, stale, or missing checks as success. Fix failed draft checks before marking the work ready. Do not push unverified changes directly to the default branch or enable automatic merging merely to bypass review.

Routine CI does not generate full-library API documentation. High-level public documentation is curated through the compact entry points in RealRooted/Challenges/ and rendered by scripts/build_challenge_pages.py. Pull requests receive a review artifact. After the ordinary build, scripts/audit_challenge_catalog.py verifies the selected declaration kinds and transitive axioms; only that exact validated main revision can deploy to GitHub Pages. Detailed proof infrastructure remains searchable in its owning theorem modules. Documentation is not a substitute for proof validation, and the required build check does not depend on publication.

Repository Cleanliness

To maintain a polished repository:

  • Do not commit transient development artifacts such as build logs (*.log), Git patch files (*.patch), backup files (e.g., *~), or temporary scratch files.
  • Keep issue-specific design or reference notes local. Note that .gitignore ignores new Markdown (*.md) files by default and explicitly allows the maintained top-level guides, architecture/status ledgers, tactic plan and generated tactic coverage, and the public SuperEulerian/ subtree.
  • Ensure any new types of temporary files or scratch directories are kept local or explicitly added to .gitignore.

License

RealRooted is distributed under the Apache License, Version 2.0. See LICENSE.

Bibliography and Links

  • M. Aissen, I. J. Schoenberg, and A. M. Whitney, On the generating functions of totally positive sequences. I, J. Analyse Math. 2 (1952), 93--103.
  • C. A. Athanasiadis and C. H. Wagner, Veronese sections and interlacing matrices of polynomials and formal power series, arXiv:2404.12989.
  • J. Borcea and P. Branden, The Lee-Yang and Polya-Schur programs. I. Linear operators preserving stability, Invent. Math. 177 (2009), 541--569.
  • P. Branden, On operators on polynomials preserving real-rootedness and the Neggers-Stanley conjecture, J. Algebraic Combin. 20 (2004), 119--130.
  • P. Branden, Iterated sequences and the geometry of zeros, J. Reine Angew. Math. 658 (2011), 115--131.
  • P. Branden, Unimodality, log-concavity, real-rootedness and beyond, in Handbook of Enumerative Combinatorics, CRC Press, 2015, 437--483.
  • B. Braun and A. Jal, Order polytopes of generalized snake posets are h^-real-rooted*, arXiv:2607.00922.
  • P. Branden and L. Solus, Symmetric decompositions and real-rootedness, Int. Math. Res. Not. (2019), doi:10.1093/imrn/rnz059.
  • M. Chudnovsky and P. Seymour, The roots of the independence polynomial of a clawfree graph, J. Combin. Theory Ser. B 97 (2007), 350--357.
  • J.-P. Dedieu, Obreschkoff's theorem revisited: what convex sets are contained in the set of hyperbolic polynomials?, J. Pure Appl. Algebra 81 (1992), 269--278.
  • J. Favard, Sur les polynomes de Tchebicheff, C. R. Acad. Sci. Paris 200 (1935), 2052--2053.
  • S. Fisk, A very short proof of Cauchy's interlace theorem for eigenvalues of Hermitian matrices, Amer. Math. Monthly 112 (2005), 118.
  • F. G. Frobenius, Uber die Bernoullischen Zahlen und die Eulerschen Polynome, Sitzungsberichte der Koniglich Preussischen Akademie der Wissenschaften (1910), 809--847.
  • J. Garloff and D. G. Wagner, Hadamard Products of Stable Polynomials Are Stable, J. Math. Anal. Appl. 202 (1996), 797--809.
  • C. D. Godsil, Algebraic Combinatorics, Routledge, 2017.
  • O. J. Heilmann and E. H. Lieb, Theory of monomer-dimer systems, Comm. Math. Phys. 25 (1972), 190--232.
  • J. I. Hutchinson, On a remarkable class of entire functions, Trans. Amer. Math. Soc. 25 (1923), 325--332.
  • O. Holtz, Hermite-Biehler, Routh-Hurwitz, and total positivity, Linear Algebra Appl. 372 (2003), 105--110.
  • D. C. Kurtz, A sufficient condition for all the roots of a polynomial to be real, Amer. Math. Monthly 99 (1992), 259--263.
  • C. A. Micchelli and R. A. Willoughby, On functions which preserve the class of Stieltjes matrices, Linear Algebra Appl. 23 (1979), 141--156.
  • N. Obreschkoff, Verteilung und Berechnung der Nullstellen reeller Polynome, VEB Deutscher Verlag der Wissenschaften, Berlin, 1963.
  • D. G. Wagner, Total positivity of Hadamard products, J. Math. Anal. Appl. 163 (1992), 459--483.
  • Q. Xiao, The real-rootedness of the toric g-contribution polynomials, arXiv:2609.01086.
  • Symmetric Functions Catalog: https://www.symmetricfunctions.com/realRooted.htm, https://www.symmetricfunctions.com/realRootedInterlacing.htm, https://www.symmetricfunctions.com/polyaFrequency.htm, and https://www.symmetricfunctions.com/realRootedWords.htm.

About

Experimental Lean 4 library for real-rooted polynomials and interlacing

www.symmetricfunctions.com

Topics

combinatoricsleanpolynomialsproofproof-assistantsequences-analysis

Resources

Readme
Apache-2.0 license
Activity

Stars

3 stars

Watchers

1 watching

Forks

2 forks
Report repository

Releases

Packages

Contributors

Languages