From 6b69da4ee042ec9cac7b2d3e0f477d408c1eb90c Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Fri, 11 Sep 2026 19:40:25 +0000 Subject: [PATCH 1/2] feat: publish auditable high-level formalization milestones --- .github/workflows/lean_action_ci.yml | 15 ++ .gitignore | 2 + MILESTONES.md | 128 ++++++++++++ README.md | 14 ++ RealRooted.lean | 3 + RealRooted/Challenges/Homogenization.lean | 53 +++++ RealRooted/Challenges/PolyaSchur.lean | 51 +++++ RealRooted/Challenges/TotallyNonnegative.lean | 42 ++++ RealRooted/Production.lean | 3 + milestones.json | 180 ++++++++++++++++ scripts/check_milestones.py | 196 ++++++++++++++++++ scripts/import_architecture.json | 4 +- scripts/test_milestones.py | 93 +++++++++ 13 files changed, 782 insertions(+), 2 deletions(-) create mode 100644 MILESTONES.md create mode 100644 RealRooted/Challenges/Homogenization.lean create mode 100644 RealRooted/Challenges/PolyaSchur.lean create mode 100644 RealRooted/Challenges/TotallyNonnegative.lean create mode 100644 milestones.json create mode 100644 scripts/check_milestones.py create mode 100644 scripts/test_milestones.py diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml index 0c21cc22..de2025d2 100644 --- a/.github/workflows/lean_action_ci.yml +++ b/.github/workflows/lean_action_ci.yml @@ -42,6 +42,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 / @@ -55,6 +59,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 diff --git a/.gitignore b/.gitignore index 2637cdd7..8ab26448 100644 --- a/.gitignore +++ b/.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 *~ diff --git a/MILESTONES.md b/MILESTONES.md new file mode 100644 index 00000000..c54844ed --- /dev/null +++ b/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) diff --git a/README.md b/README.md index 8f879099..dbe68b67 100644 --- a/README.md +++ b/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 diff --git a/RealRooted.lean b/RealRooted.lean index b58ef518..67bf5048 100644 --- a/RealRooted.lean +++ b/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 diff --git a/RealRooted/Challenges/Homogenization.lean b/RealRooted/Challenges/Homogenization.lean new file mode 100644 index 00000000..69b603a7 --- /dev/null +++ b/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 diff --git a/RealRooted/Challenges/PolyaSchur.lean b/RealRooted/Challenges/PolyaSchur.lean new file mode 100644 index 00000000..e22b612f --- /dev/null +++ b/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 diff --git a/RealRooted/Challenges/TotallyNonnegative.lean b/RealRooted/Challenges/TotallyNonnegative.lean new file mode 100644 index 00000000..abb63b14 --- /dev/null +++ b/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 diff --git a/RealRooted/Production.lean b/RealRooted/Production.lean index 5d54ae7f..fd089c9f 100644 --- a/RealRooted/Production.lean +++ b/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 diff --git a/milestones.json b/milestones.json new file mode 100644 index 00000000..f9a80400 --- /dev/null +++ b/milestones.json @@ -0,0 +1,180 @@ +{ + "schema_version": 1, + "milestones": [ + { + "id": "cauchy-interlacing", + "title": "Cauchy eigenvalue interlacing", + "summary": "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.", + "status": "proved", + "witnesses": [ + { + "module": "RealRooted.Challenges.CauchyInterlacing", + "declaration": "RealRooted.Challenges.CauchyInterlacing.principalSubmatrix_eigenvalues_interlace" + } + ], + "issues": [] + }, + { + "id": "favard-roots", + "title": "Favard recurrences produce real roots", + "summary": "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.", + "status": "proved", + "witnesses": [ + { + "module": "RealRooted.Challenges.Favard", + "declaration": "RealRooted.Challenges.Favard.realRooted" + }, + { + "module": "RealRooted.Challenges.Favard", + "declaration": "RealRooted.Challenges.Favard.interlacing" + } + ], + "issues": [] + }, + { + "id": "asw", + "title": "Aissen–Schoenberg–Whitney: roots and total positivity", + "summary": "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.", + "status": "proved", + "witnesses": [ + { + "module": "RealRooted.Challenges.AissenSchoenbergWhitney", + "declaration": "RealRooted.Challenges.AissenSchoenbergWhitney.forwardTheorem" + }, + { + "module": "RealRooted.Challenges.AissenSchoenbergWhitney", + "declaration": "RealRooted.Challenges.AissenSchoenbergWhitney.reverseTheorem" + } + ], + "issues": [] + }, + { + "id": "obreschkoff", + "title": "Obreschkoff: interlacing and real polynomial pencils", + "summary": "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.", + "status": "proved", + "witnesses": [ + { + "module": "RealRooted.Challenges.Obreschkoff", + "declaration": "RealRooted.Challenges.Obreschkoff.allCombinationsRealRooted_of_interlaces" + }, + { + "module": "RealRooted.Challenges.Obreschkoff", + "declaration": "RealRooted.Challenges.Obreschkoff.interlaces_or_reverse_of_allCombinationsRealRooted" + } + ], + "issues": [] + }, + { + "id": "claw-free-graphs", + "title": "Claw-free graph independence polynomials", + "summary": "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.", + "status": "proved", + "witnesses": [ + { + "module": "RealRooted.Challenges.ChudnovskySeymour", + "declaration": "RealRooted.Challenges.ChudnovskySeymour.clawFree_indepPoly_splits" + } + ], + "issues": [] + }, + { + "id": "ordinary-homogenization", + "title": "Ordinary homogenization preserves stability", + "summary": "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.", + "status": "proved", + "witnesses": [ + { + "module": "RealRooted.Challenges.Homogenization", + "declaration": "RealRooted.Challenges.Homogenization.ordinaryHomogenization_stable" + }, + { + "module": "RealRooted.Challenges.Homogenization", + "declaration": "RealRooted.Challenges.Homogenization.ordinaryHomogenization_stable_of_totalDegree_le" + }, + { + "module": "RealRooted.Challenges.Homogenization", + "declaration": "RealRooted.Challenges.Homogenization.ordinaryHomogenization_stableOrZero" + } + ], + "issues": [ + "https://github.com/PerAlexandersson/RealRooted/issues/550" + ] + }, + { + "id": "tn-principal-interlacing", + "title": "Totally nonnegative matrix principal interlacing", + "summary": "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.", + "status": "proved", + "witnesses": [ + { + "module": "RealRooted.Challenges.TotallyNonnegative", + "declaration": "RealRooted.Challenges.TotallyNonnegative.leadingPrincipal_charpoly_interlaces" + }, + { + "module": "RealRooted.Challenges.TotallyNonnegative", + "declaration": "RealRooted.Challenges.TotallyNonnegative.trailingPrincipal_charpoly_interlaces" + } + ], + "issues": [ + "https://github.com/PerAlexandersson/RealRooted/issues/552" + ] + }, + { + "id": "pf-multiplier-egf", + "title": "Pólya–Schur milestone: PF multipliers give real-zero entire functions", + "summary": "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.", + "status": "proved", + "witnesses": [ + { + "module": "RealRooted.Challenges.PolyaSchur", + "declaration": "RealRooted.Challenges.PolyaSchur.pfMultiplier_egf_isLaguerrePolya" + }, + { + "module": "RealRooted.Challenges.PolyaSchur", + "declaration": "RealRooted.Challenges.PolyaSchur.pfMultiplier_egf_real_zero" + }, + { + "module": "RealRooted.Challenges.PolyaSchur", + "declaration": "RealRooted.Challenges.PolyaSchur.pfMultiplier_alternating_egf_isLaguerrePolya" + } + ], + "issues": [ + "https://github.com/PerAlexandersson/RealRooted/issues/563" + ] + }, + { + "id": "braun-jal-model", + "title": "Braun–Jal generalized snake rook polynomials", + "summary": "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.", + "status": "conditional", + "witnesses": [ + { + "module": "RealRooted.Challenges.BraunJal", + "declaration": "RealRooted.Challenges.BraunJal.generalizedSnakeRookModel_theorem41" + } + ], + "issues": [] + }, + { + "id": "polya-schur-classification", + "title": "Full analytic Pólya–Schur classification", + "summary": "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.", + "status": "open", + "witnesses": [], + "issues": [ + "https://github.com/PerAlexandersson/RealRooted/issues/563" + ] + } + ] +} diff --git a/scripts/check_milestones.py b/scripts/check_milestones.py new file mode 100644 index 00000000..a8df2842 --- /dev/null +++ b/scripts/check_milestones.py @@ -0,0 +1,196 @@ +#!/usr/bin/env python3 +"""Validate the curated milestone catalog and optionally audit its Lean witnesses. + +The default command is source-only. --audit requires an up-to-date Lake build; +CI runs it after the ordinary full build. An axiom audit does not establish that +the English statement matches the theorem: that remains a review obligation. +""" + +from __future__ import annotations + +import argparse +import json +import re +import subprocess +import tempfile +from pathlib import Path + +ROOT = Path(__file__).resolve().parent.parent +ALLOWED_AXIOMS = {"propext", "Classical.choice", "Quot.sound"} +NAME = re.compile(r"[A-Za-z_][A-Za-z_0-9']*(?:\.[A-Za-z_][A-Za-z_0-9']*)*") +STATUSES = {"proved", "conditional", "open", "refuted"} +STATUS_LABELS = { + "proved": "Proved theorem", + "conditional": "Conditional theorem — external inputs remain", + "open": "Open target — not proved", + "refuted": "Refuted formulation — counterexample proved", +} + + +def validate_catalog(data: dict, root: Path = ROOT) -> None: + if data.get("schema_version") != 1: + raise ValueError("unsupported catalog schema_version") + entries = data.get("milestones") + if not isinstance(entries, list) or not entries: + raise ValueError("milestones must be a nonempty list") + ids: set[str] = set() + for item in entries: + for field in ("id", "title", "summary", "scope", "status"): + if not isinstance(item.get(field), str) or not item[field].strip(): + raise ValueError(f"missing nonempty {field}") + ident = item["id"] + if not re.fullmatch(r"[a-z][a-z0-9-]*", ident) or ident in ids: + raise ValueError(f"invalid or duplicate id: {ident}") + ids.add(ident) + if item["status"] not in STATUSES: + raise ValueError(f"invalid status: {ident}") + if not isinstance(item.get("witnesses"), list): + raise ValueError(f"missing witnesses list: {ident}") + if not isinstance(item.get("issues"), list) or not all( + isinstance(url, str) and re.fullmatch( + r"https://github\.com/[\w-]+/[\w.-]+/issues/[1-9][0-9]*", url + ) for url in item["issues"] + ): + raise ValueError(f"invalid issue links: {ident}") + if item["status"] == "open": + if item["witnesses"] or not item["issues"]: + raise ValueError(f"open target needs an issue and no witness: {ident}") + elif not item["witnesses"]: + raise ValueError(f"non-open milestone needs a theorem witness: {ident}") + seen: set[str] = set() + for witness in item["witnesses"]: + module, theorem = witness.get("module"), witness.get("declaration") + if not isinstance(module, str) or not NAME.fullmatch(module): + raise ValueError(f"invalid module: {ident}") + if not module.startswith("RealRooted.Challenges."): + raise ValueError(f"witness must use a challenge entry point: {ident}") + if not isinstance(theorem, str) or not NAME.fullmatch(theorem): + raise ValueError(f"invalid declaration: {ident}") + if theorem in seen: + raise ValueError(f"duplicate witness: {ident}") + seen.add(theorem) + if not (root / (module.replace(".", "/") + ".lean")).is_file(): + raise ValueError(f"missing challenge module: {module}") + + +def witness_names(data: dict) -> list[str]: + return sorted({w["declaration"] for m in data["milestones"] for w in m["witnesses"]}) + + +def audit_source(data: dict) -> str: + modules = sorted({w["module"] for m in data["milestones"] for w in m["witnesses"]}) + source = "import Lean\n" + "".join(f"import {m}\n" for m in modules) + "\n" + for name in witness_names(data): + # Reject a proposition definition or a source axiom masquerading as a + # theorem witness, even if #print axioms alone would accept it. + source += ( + "run_cmd do\n" + f" match (← Lean.getEnv).find? `{name} with\n" + " | some (.thmInfo _) => pure ()\n" + f' | _ => throwError "Not a theorem witness: {name}"\n' + f"#print axioms {name}\n\n" + ) + return source + + +def parse_axioms(output: str, expected: list[str]) -> dict[str, list[str]]: + pattern = re.compile( + r"'(?P[^'\n]+)' (?:depends on axioms:\s*\[(?P[^]]*)\]" + r"|does not depend on any axioms)", re.MULTILINE + ) + found: dict[str, list[str]] = {} + for match in pattern.finditer(output): + name = match["name"] + if name not in expected: + raise ValueError(f"unexpected axiom result: {name}") + if name in found: + raise ValueError(f"duplicate axiom result: {name}") + axioms = sorted({a.strip() for a in (match["axioms"] or "").split(",") if a.strip()}) + if not set(axioms) <= ALLOWED_AXIOMS: + raise ValueError(f"nonstandard axioms for {name}: {axioms}") + found[name] = axioms + missing = set(expected) - found.keys() + if missing: + raise ValueError(f"missing axiom results: {sorted(missing)}") + return found + + +def markdown(data: dict) -> str: + lines = [ + "# 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`.", "", + ] + for item in data["milestones"]: + lines.extend([f"## {item['title']}", "", f"Status: {STATUS_LABELS[item['status']]}", "", + item["summary"], "", f"Scope: {item['scope']}", ""]) + for witness in item["witnesses"]: + path = witness["module"].replace(".", "/") + ".lean" + lines.append(f"- Lean theorem: [{witness['declaration']}]({path})") + for issue in item["issues"]: + lines.append(f"- [Tracking issue #{issue.rsplit('/', 1)[1]}]({issue})") + lines.append("") + return "\n".join(lines) + + +def run_audit(data: dict, report_path: Path) -> None: + # An isolated scratch file is generated, never added to the library or Git. + with tempfile.TemporaryDirectory(prefix="realrooted-milestones-") as directory: + source = Path(directory) / "Audit.lean" + source.write_text(audit_source(data), encoding="utf-8") + result = subprocess.run( + ["lake", "env", "lean", str(source)], cwd=ROOT, text=True, + stdout=subprocess.PIPE, stderr=subprocess.STDOUT, timeout=1200, + ) + if result.returncode: + raise ValueError(f"Lean axiom audit failed (exit {result.returncode}):\n{result.stdout}") + axioms = parse_axioms(result.stdout, witness_names(data)) + revision = subprocess.check_output(["git", "rev-parse", "HEAD"], cwd=ROOT, text=True).strip() + report = { + "schema_version": 1, "revision": revision, + "verification": "lean-transitive-axiom-audit", + "permitted_axioms": sorted(ALLOWED_AXIOMS), "axioms": axioms, + "independent_comparator_coverage": "See comparator/config.json; not inferred here.", + "milestones": data["milestones"], + } + report_path.parent.mkdir(parents=True, exist_ok=True) + report_path.write_text(json.dumps(report, indent=2, ensure_ascii=False) + "\n", encoding="utf-8") + print(f"Audited {len(axioms)} witnesses at {revision}; report: {report_path}") + + +def main() -> int: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write", action="store_true", help="regenerate MILESTONES.md") + parser.add_argument("--audit", action="store_true", help="run Lean after a fresh full build") + parser.add_argument("--report", type=Path, default=Path("milestone-audit.json")) + args = parser.parse_args() + try: + data = json.loads((ROOT / "milestones.json").read_text(encoding="utf-8")) + validate_catalog(data) + expected = markdown(data) + document = ROOT / "MILESTONES.md" + if args.write: + document.write_text(expected, encoding="utf-8") + elif not document.is_file() or document.read_text(encoding="utf-8") != expected: + raise ValueError("MILESTONES.md is stale; run scripts/check_milestones.py --write") + if args.audit: + run_audit(data, args.report) + print(f"Milestone source checks passed ({len(data['milestones'])} entries).") + return 0 + except (ValueError, OSError, subprocess.SubprocessError) as error: + print(f"Milestone check failed: {error}") + return 1 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/scripts/import_architecture.json b/scripts/import_architecture.json index 14533208..0e548a14 100644 --- a/scripts/import_architecture.json +++ b/scripts/import_architecture.json @@ -10,10 +10,10 @@ }, "budgets": { "RealRooted": { - "max_modules": 1182 + "max_modules": 1185 }, "RealRooted.Production": { - "max_modules": 1061 + "max_modules": 1064 }, "RealRooted.Tactic.Examples": { "max_modules": 633 diff --git a/scripts/test_milestones.py b/scripts/test_milestones.py new file mode 100644 index 00000000..1952ad7e --- /dev/null +++ b/scripts/test_milestones.py @@ -0,0 +1,93 @@ +#!/usr/bin/env python3 +"""Source-only regression tests: no Lean or Lake is invoked.""" + +import copy +import unittest +from unittest.mock import patch + +from check_milestones import audit_source, markdown, parse_axioms, validate_catalog + + +def fixture(): + return {"schema_version": 1, "milestones": [{ + "id": "example", "title": "Example", "summary": "An example theorem.", + "scope": "Under explicit hypotheses.", "status": "proved", "issues": [], + "witnesses": [{"module": "RealRooted.Challenges.Example", "declaration": "Foo.bar"}], + }]} + + +class CatalogTests(unittest.TestCase): + @patch("pathlib.Path.is_file", return_value=True) + def test_valid_catalog(self, _): + validate_catalog(fixture()) + + @patch("pathlib.Path.is_file", return_value=True) + def test_duplicate_ids(self, _): + data = fixture() + data["milestones"].append(copy.deepcopy(data["milestones"][0])) + with self.assertRaisesRegex(ValueError, "duplicate id"): + validate_catalog(data) + + def test_open_requires_issue_not_witness(self): + data = fixture() + data["milestones"][0]["status"] = "open" + with self.assertRaisesRegex(ValueError, "open target"): + validate_catalog(data) + data["milestones"][0]["witnesses"] = [] + data["milestones"][0]["issues"] = ["https://github.com/a/b/issues/1"] + validate_catalog(data) + + def test_proved_requires_witness(self): + data = fixture() + data["milestones"][0]["witnesses"] = [] + with self.assertRaisesRegex(ValueError, "theorem witness"): + validate_catalog(data) + + def test_invalid_lean_name(self): + data = fixture() + data["milestones"][0]["witnesses"][0]["declaration"] = "Foo\naxiom bad : False" + with self.assertRaisesRegex(ValueError, "invalid declaration"): + validate_catalog(data) + + @patch("pathlib.Path.is_file", return_value=False) + def test_missing_module(self, _): + with self.assertRaisesRegex(ValueError, "missing challenge"): + validate_catalog(fixture()) + + def test_source_only_expected_commands(self): + source = audit_source(fixture()) + self.assertIn("import RealRooted.Challenges.Example\n", source) + self.assertIn("#print axioms Foo.bar\n", source) + self.assertIn("some (.thmInfo _)", source) + self.assertIn("Not a theorem witness: Foo.bar", source) + + def test_standard_and_empty_axioms(self): + result = parse_axioms("'Foo.bar' depends on axioms: [propext,\nClassical.choice]\n" + "'Foo.empty' does not depend on any axioms\n", ["Foo.bar", "Foo.empty"]) + self.assertEqual(result["Foo.empty"], []) + + def test_missing_result(self): + with self.assertRaisesRegex(ValueError, "missing axiom"): + parse_axioms("", ["Foo.bar"]) + + def test_nonstandard_axiom(self): + for axiom in ("sorryAx", "customFact"): + with self.assertRaisesRegex(ValueError, "nonstandard"): + parse_axioms(f"'Foo.bar' depends on axioms: [{axiom}]", ["Foo.bar"]) + + def test_duplicate_and_unexpected_results(self): + line = "'Foo.bar' does not depend on any axioms\n" + with self.assertRaisesRegex(ValueError, "duplicate"): + parse_axioms(line * 2, ["Foo.bar"]) + with self.assertRaisesRegex(ValueError, "unexpected"): + parse_axioms(line, ["Other.name"]) + + def test_preview_labels_conditional_as_conditional(self): + data = fixture() + data["milestones"][0]["status"] = "conditional" + self.assertIn("Conditional theorem — external inputs remain", markdown(data)) + self.assertIn("not a live CI badge", markdown(data)) + + +if __name__ == "__main__": + unittest.main() From f8a611e21a5dd0f9758ad28af7bc343275d64120 Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Fri, 11 Sep 2026 19:51:22 +0000 Subject: [PATCH 2/2] test: harden milestone metadata and axiom-name validation --- scripts/check_milestones.py | 16 ++++++++++++- scripts/test_milestones.py | 45 ++++++++++++++++++++++++++++++++----- 2 files changed, 55 insertions(+), 6 deletions(-) diff --git a/scripts/check_milestones.py b/scripts/check_milestones.py index a8df2842..eb9ce6d6 100644 --- a/scripts/check_milestones.py +++ b/scripts/check_milestones.py @@ -28,6 +28,8 @@ def validate_catalog(data: dict, root: Path = ROOT) -> None: + if not isinstance(data, dict): + raise ValueError("catalog must be an object") if data.get("schema_version") != 1: raise ValueError("unsupported catalog schema_version") entries = data.get("milestones") @@ -35,6 +37,8 @@ def validate_catalog(data: dict, root: Path = ROOT) -> None: raise ValueError("milestones must be a nonempty list") ids: set[str] = set() for item in entries: + if not isinstance(item, dict): + raise ValueError("milestone entries must be objects") for field in ("id", "title", "summary", "scope", "status"): if not isinstance(item.get(field), str) or not item[field].strip(): raise ValueError(f"missing nonempty {field}") @@ -59,6 +63,8 @@ def validate_catalog(data: dict, root: Path = ROOT) -> None: raise ValueError(f"non-open milestone needs a theorem witness: {ident}") seen: set[str] = set() for witness in item["witnesses"]: + if not isinstance(witness, dict): + raise ValueError(f"witness entries must be objects: {ident}") module, theorem = witness.get("module"), witness.get("declaration") if not isinstance(module, str) or not NAME.fullmatch(module): raise ValueError(f"invalid module: {ident}") @@ -66,6 +72,11 @@ def validate_catalog(data: dict, root: Path = ROOT) -> None: raise ValueError(f"witness must use a challenge entry point: {ident}") if not isinstance(theorem, str) or not NAME.fullmatch(theorem): raise ValueError(f"invalid declaration: {ident}") + # This bounds the catalog metadata to the named challenge facade. + # It does not prove the declaration is physically defined in that + # file; imported declarations remain a separate Lean-level concern. + if not theorem.startswith(module + "."): + raise ValueError(f"declaration must be in listed challenge module: {ident}") if theorem in seen: raise ValueError(f"duplicate witness: {ident}") seen.add(theorem) @@ -95,7 +106,10 @@ def audit_source(data: dict) -> str: def parse_axioms(output: str, expected: list[str]) -> dict[str, list[str]]: pattern = re.compile( - r"'(?P[^'\n]+)' (?:depends on axioms:\s*\[(?P[^]]*)\]" + # Lean wraps the rendered declaration name in apostrophes. Names may + # themselves contain apostrophes, so terminate at the apostrophe before + # the fixed ` depends`/` does` suffix rather than at the first one. + r"'(?P[^\n]+?)' (?:depends on axioms:\s*\[(?P[^]]*)\]" r"|does not depend on any axioms)", re.MULTILINE ) found: dict[str, list[str]] = {} diff --git a/scripts/test_milestones.py b/scripts/test_milestones.py index 1952ad7e..65ca2148 100644 --- a/scripts/test_milestones.py +++ b/scripts/test_milestones.py @@ -12,11 +12,18 @@ def fixture(): return {"schema_version": 1, "milestones": [{ "id": "example", "title": "Example", "summary": "An example theorem.", "scope": "Under explicit hypotheses.", "status": "proved", "issues": [], - "witnesses": [{"module": "RealRooted.Challenges.Example", "declaration": "Foo.bar"}], + "witnesses": [{ + "module": "RealRooted.Challenges.Example", + "declaration": "RealRooted.Challenges.Example.Foo.bar", + }], }]} class CatalogTests(unittest.TestCase): + def test_malformed_catalog(self): + with self.assertRaisesRegex(ValueError, "catalog must be an object"): + validate_catalog([]) + @patch("pathlib.Path.is_file", return_value=True) def test_valid_catalog(self, _): validate_catalog(fixture()) @@ -28,6 +35,18 @@ def test_duplicate_ids(self, _): with self.assertRaisesRegex(ValueError, "duplicate id"): validate_catalog(data) + def test_malformed_milestone_entry(self): + data = fixture() + data["milestones"] = ["not an object"] + with self.assertRaisesRegex(ValueError, "entries must be objects"): + validate_catalog(data) + + def test_malformed_witness_entry(self): + data = fixture() + data["milestones"][0]["witnesses"] = ["not an object"] + with self.assertRaisesRegex(ValueError, "witness entries must be objects"): + validate_catalog(data) + def test_open_requires_issue_not_witness(self): data = fixture() data["milestones"][0]["status"] = "open" @@ -49,6 +68,12 @@ def test_invalid_lean_name(self): with self.assertRaisesRegex(ValueError, "invalid declaration"): validate_catalog(data) + def test_declaration_must_use_listed_module_namespace(self): + data = fixture() + data["milestones"][0]["witnesses"][0]["declaration"] = "Other.Foo" + with self.assertRaisesRegex(ValueError, "listed challenge module"): + validate_catalog(data) + @patch("pathlib.Path.is_file", return_value=False) def test_missing_module(self, _): with self.assertRaisesRegex(ValueError, "missing challenge"): @@ -57,15 +82,25 @@ def test_missing_module(self, _): def test_source_only_expected_commands(self): source = audit_source(fixture()) self.assertIn("import RealRooted.Challenges.Example\n", source) - self.assertIn("#print axioms Foo.bar\n", source) + self.assertIn("#print axioms RealRooted.Challenges.Example.Foo.bar\n", source) self.assertIn("some (.thmInfo _)", source) - self.assertIn("Not a theorem witness: Foo.bar", source) + self.assertIn( + "Not a theorem witness: RealRooted.Challenges.Example.Foo.bar", source + ) def test_standard_and_empty_axioms(self): - result = parse_axioms("'Foo.bar' depends on axioms: [propext,\nClassical.choice]\n" - "'Foo.empty' does not depend on any axioms\n", ["Foo.bar", "Foo.empty"]) + result = parse_axioms( + "'Foo.bar' depends on axioms: [propext,\nClassical.choice]\n" + "'Foo.empty' does not depend on any axioms\n", + ["Foo.bar", "Foo.empty"], + ) self.assertEqual(result["Foo.empty"], []) + def test_apostrophe_in_declaration_name(self): + name = "RealRooted.Challenges.Example.Foo'bar" + result = parse_axioms(f"'{name}' does not depend on any axioms\n", [name]) + self.assertEqual(result[name], []) + def test_missing_result(self): with self.assertRaisesRegex(ValueError, "missing axiom"): parse_axioms("", ["Foo.bar"])