feat: add milestone challenges and a reader-facing audited catalog

.github/workflows/lean_action_ci.yml

@@ -43,6 +43,10 @@ jobs:
         run: |
           python3 scripts/check_proof_status.py --self-test
           python3 scripts/check_proof_status.py
+      - name: Check milestone catalog sources
+        run: |
+          PYTHONDONTWRITEBYTECODE=1 python3 scripts/test_milestones.py
+          PYTHONDONTWRITEBYTECODE=1 python3 scripts/check_milestones.py
       - name: Free up disk space
         run: |
           df -h /
@@ -56,6 +60,17 @@ jobs:
           # if future Lake metadata changes lean-action auto-detection.
           build: true
           build-args: ""
+      - name: Audit milestone theorem witnesses
+        run: python3 scripts/check_milestones.py --audit --report milestone-audit.json
+      - name: Upload revision-specific milestone evidence
+        uses: actions/upload-artifact@v4
+        with:
+          name: milestone-audit
+          path: |
+            milestone-audit.json
+            MILESTONES.md
+          if-no-files-found: error
+          retention-days: 30
 
   docs:
     name: docs

.gitignore

@@ -9,6 +9,7 @@
 !LEAN_GOLF.md
 !OEIS_THEORY_AUDIT.md
 !PROOF_STATUS.md
+!MILESTONES.md
 !RealRooted/Tactic/PLAN.md
 !RealRooted/Tactic/OEIS_COVERAGE.md
 
@@ -19,6 +20,7 @@ SuperEulerian/.lake/
 SuperEulerian/.lake
 
 # Generated/local artifacts.
+milestone-audit.json
 realrooted-interlacing-seminar-handout.html
 .DS_Store
 *~

MILESTONES.md

@@ -0,0 +1,128 @@
+# Formalization milestones
+
+A curated guide to major theorems, not a count of helper lemmas.
+
+**Reading the status:** “Proved” means the stated theorem has a Lean witness;
+its mathematical hypotheses still apply. “Conditional” means an explicit external
+model identity or other unformalized input remains. An open target has no witness.
+The scope notes are part of the claim, not fine print.
+
+This generated source catalog is not a live CI badge. The `milestone-audit` CI
+artifact records a transitive-axiom audit for one exact Git revision. Only a
+successful full build followed by that audit validates that revision. The separate
+Comparator workflow independently rechecks only its configured theorem list;
+catalog membership does not imply independent-comparator coverage.
+
+Source of truth: [milestones.json](milestones.json). Regenerate with
+`python3 scripts/check_milestones.py --write`.
+
+## Cauchy eigenvalue interlacing
+
+Status: Proved theorem
+
+Delete one row and the matching column from a real symmetric or complex Hermitian matrix. The smaller matrix's eigenvalues lie between those of the original.
+
+Scope: All finite sizes, under the Hermitian hypothesis; the formal statement uses ordered eigenvalues.
+
+- Lean theorem: [RealRooted.Challenges.CauchyInterlacing.principalSubmatrix_eigenvalues_interlace](RealRooted/Challenges/CauchyInterlacing.lean)
+
+## Favard recurrences produce real roots
+
+Status: Proved theorem
+
+A monic three-term recurrence with positive Favard coefficients produces nonzero polynomials with only real roots.
+
+Scope: The standard recurrence and positive coefficients are mathematical hypotheses. This entry covers roots, not existence of an orthogonality measure.
+
+- Lean theorem: [RealRooted.Challenges.Favard.realRooted](RealRooted/Challenges/Favard.lean)
+- Lean theorem: [RealRooted.Challenges.Favard.interlacing](RealRooted/Challenges/Favard.lean)
+
+## Aissen–Schoenberg–Whitney: roots and total positivity
+
+Status: Proved theorem
+
+The finite-polynomial correspondence connects nonpositive real roots with nonnegativity of every minor of the coefficient Toeplitz matrix.
+
+Scope: The reverse direction assumes nonnegative coefficients; both directions use the repository's real-rooted/zero conventions. This is a polynomial theorem, not the classification of arbitrary infinite generating functions.
+
+- Lean theorem: [RealRooted.Challenges.AissenSchoenbergWhitney.forwardTheorem](RealRooted/Challenges/AissenSchoenbergWhitney.lean)
+- Lean theorem: [RealRooted.Challenges.AissenSchoenbergWhitney.reverseTheorem](RealRooted/Challenges/AissenSchoenbergWhitney.lean)
+
+## Obreschkoff: interlacing and real polynomial pencils
+
+Status: Proved theorem
+
+Interlacing guarantees that every real linear combination has only real roots or is zero. Conversely, this pencil property forces interlacing up to orientation.
+
+Scope: The converse witness explicitly assumes nonzero split inputs and equal or consecutive degrees. The catalog does not omit these degree and orientation conventions.
+
+- Lean theorem: [RealRooted.Challenges.Obreschkoff.allCombinationsRealRooted_of_interlaces](RealRooted/Challenges/Obreschkoff.lean)
+- Lean theorem: [RealRooted.Challenges.Obreschkoff.interlaces_or_reverse_of_allCombinationsRealRooted](RealRooted/Challenges/Obreschkoff.lean)
+
+## Claw-free graph independence polynomials
+
+Status: Proved theorem
+
+For every finite claw-free graph, the polynomial counting independent vertex sets by size has only real roots.
+
+Scope: The graph must be claw-free: no induced vertex with three pairwise nonadjacent neighbors. The graph and its independence polynomial are formalized objects.
+
+- Lean theorem: [RealRooted.Challenges.ChudnovskySeymour.clawFree_indepPoly_splits](RealRooted/Challenges/ChudnovskySeymour.lean)
+
+## Ordinary homogenization preserves stability
+
+Status: Proved theorem
+
+Adding one variable to make all monomials have the same total degree preserves multivariate real stability when coefficients are nonnegative.
+
+Scope: Stability means nonvanishing when every variable has positive imaginary part. The strict result assumes a nonzero stable input; a separate witness includes zero. Padding to a larger homogenizing degree is also covered.
+
+- Lean theorem: [RealRooted.Challenges.Homogenization.ordinaryHomogenization_stable](RealRooted/Challenges/Homogenization.lean)
+- Lean theorem: [RealRooted.Challenges.Homogenization.ordinaryHomogenization_stable_of_totalDegree_le](RealRooted/Challenges/Homogenization.lean)
+- Lean theorem: [RealRooted.Challenges.Homogenization.ordinaryHomogenization_stableOrZero](RealRooted/Challenges/Homogenization.lean)
+- [Tracking issue #550](https://github.com/PerAlexandersson/RealRooted/issues/550)
+
+## Totally nonnegative matrix principal interlacing
+
+Status: Proved theorem
+
+For a finite real matrix whose every minor is nonnegative, the characteristic polynomial of its leading or trailing principal section interlaces that of the matrix.
+
+Scope: Includes singular and reducible matrices. Interlacing is weak (coincident roots are allowed), and the sections remove the first or last index; this entry does not claim arbitrary principal deletion.
+
+- Lean theorem: [RealRooted.Challenges.TotallyNonnegative.leadingPrincipal_charpoly_interlaces](RealRooted/Challenges/TotallyNonnegative.lean)
+- Lean theorem: [RealRooted.Challenges.TotallyNonnegative.trailingPrincipal_charpoly_interlaces](RealRooted/Challenges/TotallyNonnegative.lean)
+- [Tracking issue #552](https://github.com/PerAlexandersson/RealRooted/issues/552)
+
+## Pólya–Schur milestone: PF multipliers give real-zero entire functions
+
+Status: Proved theorem
+
+A PF multiplier sequence has an exponential generating function in the Laguerre–Pólya class: a locally uniform limit of real-rooted real polynomials. Unless identically zero, its zeros are real.
+
+Scope: The PF multiplier condition is stronger than coefficient nonnegativity alone. Zero sequences and initial zero coefficients are included. Alternating the coefficient signs reflects the function. This is a proved forward branch, not the full classification.
+
+- Lean theorem: [RealRooted.Challenges.PolyaSchur.pfMultiplier_egf_isLaguerrePolya](RealRooted/Challenges/PolyaSchur.lean)
+- Lean theorem: [RealRooted.Challenges.PolyaSchur.pfMultiplier_egf_real_zero](RealRooted/Challenges/PolyaSchur.lean)
+- Lean theorem: [RealRooted.Challenges.PolyaSchur.pfMultiplier_alternating_egf_isLaguerrePolya](RealRooted/Challenges/PolyaSchur.lean)
+- [Tracking issue #563](https://github.com/PerAlexandersson/RealRooted/issues/563)
+
+## Braun–Jal generalized snake rook polynomials
+
+Status: Conditional theorem — external inputs remain
+
+The formalized recurrence and interlacing machinery yields the generalized-snake rook-polynomial theorem from explicit board-model inputs.
+
+Scope: Conditional: the theorem still takes the auxiliary recurrence, board-difference nonnegativity, snake recurrence, degree identity and constant-board identification as inputs. A theorem with these hypotheses is not an unconditional proof of the complete combinatorial model.
+
+- Lean theorem: [RealRooted.Challenges.BraunJal.generalizedSnakeRookModel_theorem41](RealRooted/Challenges/BraunJal.lean)
+
+## Full analytic Pólya–Schur classification
+
+Status: Open target — not proved
+
+Complete the analytic classification of real-rootedness-preserving multiplier sequences, including the remaining converse and product-description bridges.
+
+Scope: Open at this catalog checkpoint. The proved PF forward branch is listed separately above; a green build or a closed subtask does not settle this larger target.
+
+- [Tracking issue #563](https://github.com/PerAlexandersson/RealRooted/issues/563)

README.md

@@ -3,6 +3,12 @@
 Proof assumptions and refuted legacy interfaces are summarized in
 [`PROOF_STATUS.md`](PROOF_STATUS.md).
 
+For a non-Lean overview of major results, see the curated
+[formalization milestones](MILESTONES.md). Each entry names its mathematical
+scope, an explicit theorem witness, and any remaining external assumptions.
+The machine-readable [catalog](milestones.json) can feed a public progress
+page; a per-revision CI audit checks its theorem witnesses and transitive axioms.
+
 `RealRooted` is an experimental Lean 4 library for real-rooted univariate
 polynomials, interlacing, compatibility, Polya-frequency sequences, and related
 combinatorial applications.
@@ -209,6 +215,14 @@ emulation. These scripts complement `lake build`; they do not replace it.
 - `RealRooted/Challenges/` contains compact entry points for famous theorem
   statements, each linking the Lean-facing declaration to human catalog
   statements and references.
+- `milestones.json` selects high-level challenge witnesses for a public-facing
+  catalog. `MILESTONES.md` is its generated readable view. Source checks run via
+  `python3 scripts/check_milestones.py`; regenerate with `--write`. After a
+  fresh full build, `--audit` checks that every witness is a theorem and uses
+  only the standard permitted axioms. CI uploads the result as
+  `milestone-audit`, stamped with the exact audited revision. Neither source
+  metadata nor this audit automatically verifies the English interpretation;
+  maintainers review that correspondence and every assumption boundary.
 - `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

RealRooted.lean

@@ -1179,3 +1179,6 @@ import RealRooted.PolyaFrequency.EventuallyPolynomial.CausalClosure
 import RealRooted.PolyaFrequency.EventuallyPolynomial.CausalClosure.ZeroPrefix
 import RealRooted.PolynomialValueEulerNumerator.PF.Causal
 import RealRooted.PolynomialValueEulerNumerator.Product.PF.Causal
+import RealRooted.Challenges.Homogenization
+import RealRooted.Challenges.PolyaSchur
+import RealRooted.Challenges.TotallyNonnegative

RealRooted/Challenges/Homogenization.lean

@@ -0,0 +1,53 @@
+import RealRooted.Hyperbolicity
+
+/-!
+# Ordinary stable homogenization challenge entry point
+
+Human statement: ordinary homogenization preserves multivariate real
+stability for a polynomial with nonnegative coefficients (issue #550).
+
+The checked endpoints are `MvRealStable.ordinaryHomogenization` and
+`MvRealStable.ordinaryHomogenization_of_totalDegree_le` in
+`RealRooted.Hyperbolicity`.  The latter permits padding the homogenizing
+degree.  The zero-aware complex formulation is also exposed below.  These
+are challenge-facing wrappers only; the proofs and their assumptions remain
+in the reusable stability module.
+-/
+
+namespace RealRooted
+namespace Challenges
+namespace Homogenization
+
+/-- The exact total-degree ordinary homogenization of a nonzero real-stable
+multivariate polynomial with nonnegative coefficients is real stable. -/
+theorem ordinaryHomogenization_stable
+    {σ : Type*} {P : MvPolynomial σ ℝ} (hst : MvRealStable P)
+    (hnn : MvPolynomial.HasNonnegCoeffs P) (hP : P ≠ 0) :
+    MvRealStable
+      (MvPolynomial.ordinaryHomogenization P P.totalDegree) := by
+  exact hst.ordinaryHomogenization hnn hP
+
+/-- Ordinary homogenization remains real stable when its target degree is any
+degree at least the source total degree. -/
+theorem ordinaryHomogenization_stable_of_totalDegree_le
+    {σ : Type*} {P : MvPolynomial σ ℝ} {d : ℕ}
+    (hst : MvRealStable P) (hnn : MvPolynomial.HasNonnegCoeffs P)
+    (hP : P ≠ 0) (hdeg : P.totalDegree ≤ d) :
+    MvRealStable (MvPolynomial.ordinaryHomogenization P d) := by
+  exact hst.ordinaryHomogenization_of_totalDegree_le hnn hP hdeg
+
+/-- Zero-aware version of the padded ordinary-homogenization result: the
+complexification is either identically zero or upper-half-plane stable. -/
+theorem ordinaryHomogenization_stableOrZero
+    {σ : Type*} {P : MvPolynomial σ ℝ} {d : ℕ}
+    (hst : P = 0 ∨ MvRealStable P)
+    (hnn : MvPolynomial.HasNonnegCoeffs P)
+    (hdeg : P.totalDegree ≤ d) :
+    MvUpperHalfPlaneStableOrZero
+      (complexifyMv (MvPolynomial.ordinaryHomogenization P d)) := by
+  exact mvUpperHalfPlaneStableOrZero_complexify_ordinaryHomogenization
+    hst hnn hdeg
+
+end Homogenization
+end Challenges
+end RealRooted

RealRooted/Challenges/PolyaSchur.lean

@@ -0,0 +1,51 @@
+import RealRooted.MultiplierSequence.PolyaSchur.Growth
+import RealRooted.MultiplierSequence.PolyaSchur.LaguerrePolya.Zeros
+
+/-!
+# Pólya--Schur challenge entry point
+
+Human statement: a pointwise nonnegative (PF) multiplier sequence has a
+Laguerre--Pólya exponential-generating function, and every non-real zero of a
+nonzero such function is excluded (issue #563, partial).
+
+The first assertion is the checked forward endpoint
+`IsPFMultiplierSequence.isLaguerrePolya_complexExpGeneratingFunction`; the
+real-zero conclusion is the checked zero-closure endpoint
+`IsLaguerrePolya.im_eq_zero_of_eq_zero`.  The full analytic Pólya--Schur
+classification, including its converse and canonical product description,
+remains outside this challenge facade.
+-/
+
+namespace RealRooted
+namespace Challenges
+namespace PolyaSchur
+
+/-- The complex exponential-generating function attached to a real sequence. -/
+noncomputable abbrev ComplexExponentialGeneratingFunction (gamma : ℕ → ℝ) : ℂ → ℂ :=
+  complexExpGeneratingFunction gamma
+
+/-- A PF multiplier sequence has a zero-aware Laguerre--Pólya complex EGF. -/
+theorem pfMultiplier_egf_isLaguerrePolya
+    {gamma : ℕ → ℝ} (hgamma : IsPFMultiplierSequence gamma) :
+    IsLaguerrePolya (ComplexExponentialGeneratingFunction gamma) := by
+  exact hgamma.isLaguerrePolya_complexExpGeneratingFunction
+
+/-- Every zero of a nonzero PF-multiplier EGF lies on the real axis. -/
+theorem pfMultiplier_egf_real_zero
+    {gamma : ℕ → ℝ} (hgamma : IsPFMultiplierSequence gamma)
+    (hne : ComplexExponentialGeneratingFunction gamma ≠ 0)
+    {z : ℂ} (hz : ComplexExponentialGeneratingFunction gamma z = 0) :
+    z.im = 0 := by
+  exact (pfMultiplier_egf_isLaguerrePolya hgamma).im_eq_zero_of_eq_zero hne hz
+
+/-- Alternating the signs of a PF multiplier sequence gives the reflected
+Laguerre--Pólya EGF, corresponding to precomposition by `z ↦ -z`. -/
+theorem pfMultiplier_alternating_egf_isLaguerrePolya
+    {gamma : ℕ → ℝ} (hgamma : IsPFMultiplierSequence gamma) :
+    IsLaguerrePolya
+      (complexExpGeneratingFunction (fun k => (-1 : ℝ) ^ k * gamma k)) := by
+  exact hgamma.isLaguerrePolya_complexExpGeneratingFunction_alternating
+
+end PolyaSchur
+end Challenges
+end RealRooted

RealRooted/Challenges/TotallyNonnegative.lean

@@ -0,0 +1,42 @@
+import RealRooted.TotallyNonnegInterlacing
+
+/-!
+# Totally nonnegative principal interlacing challenge entry point
+
+Human statement: the characteristic polynomial of either the leading or the
+trailing codimension-one principal section of a finite totally nonnegative
+matrix weakly interlaces the characteristic polynomial of the full matrix.
+The checked theorem includes singular and reducible matrices (issue #552).
+
+The reusable endpoints are
+`Matrix.IsTotallyNonneg.leading_charpoly_interlaces` and
+`Matrix.IsTotallyNonneg.trailing_charpoly_interlaces` in
+`RealRooted.TotallyNonnegInterlacing`.  This file only gives compact
+challenge-facing names; it is not independent comparator coverage.
+-/
+
+namespace RealRooted
+namespace Challenges
+namespace TotallyNonnegative
+
+/-- Weak trailing-principal characteristic-polynomial interlacing for every
+finite totally nonnegative real matrix, including singular matrices. -/
+theorem trailingPrincipal_charpoly_interlaces {N : ℕ}
+    {A : Matrix (Fin (N + 1)) (Fin (N + 1)) ℝ}
+    (hA : A.IsTotallyNonneg) :
+    RealRooted.Interlaces
+      (A.submatrix Fin.succ Fin.succ).charpoly A.charpoly := by
+  exact hA.trailing_charpoly_interlaces
+
+/-- Weak leading-principal characteristic-polynomial interlacing for every
+finite totally nonnegative real matrix, including singular matrices. -/
+theorem leadingPrincipal_charpoly_interlaces {N : ℕ}
+    {A : Matrix (Fin (N + 1)) (Fin (N + 1)) ℝ}
+    (hA : A.IsTotallyNonneg) :
+    RealRooted.Interlaces
+      (A.submatrix Fin.castSucc Fin.castSucc).charpoly A.charpoly := by
+  exact hA.leading_charpoly_interlaces
+
+end TotallyNonnegative
+end Challenges
+end RealRooted

RealRooted/Production.lean

@@ -1058,6 +1058,9 @@ import RealRooted.PolyaFrequency.EventuallyPolynomial.CausalClosure
 import RealRooted.PolyaFrequency.EventuallyPolynomial.CausalClosure.ZeroPrefix
 import RealRooted.PolynomialValueEulerNumerator.PF.Causal
 import RealRooted.PolynomialValueEulerNumerator.Product.PF.Causal
+import RealRooted.Challenges.Homogenization
+import RealRooted.Challenges.PolyaSchur
+import RealRooted.Challenges.TotallyNonnegative
 
 /-!
 # RealRooted production umbrella