From 751ad08b134c79216f383c7bd63ab7dd100e0765 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Sun, 23 Aug 2026 10:25:26 +0000 Subject: [PATCH 01/16] ci: check Lean snippets in released READMEs --- .github/workflows/ci.yml | 7 +++++++ HexBareiss/README.md | 4 ++-- HexBareissMathlib/README.md | 6 +++--- HexConway/README.md | 4 ++-- HexDeterminant/README.md | 6 +++--- HexDeterminantMathlib/README.md | 6 +++--- HexGF2/README.md | 4 ++-- HexGF2Mathlib/README.md | 6 +++--- HexGFq/README.md | 4 ++-- HexGFqField/README.md | 4 ++-- HexGFqMathlib/README.md | 8 ++++---- HexGramSchmidt/README.md | 4 ++-- HexGramSchmidtMathlib/README.md | 8 ++++---- HexMatrixMathlib/README.md | 10 +++++----- HexMvPoly/README.md | 4 ++-- HexMvPolyMathlib/README.md | 6 +++--- HexPolyFpMathlib/README.md | 2 +- HexRealRoots/README.md | 14 +++++++++----- HexRealRootsMathlib/README.md | 6 ++++++ HexRoots/README.md | 2 ++ HexRootsMathlib/README.md | 14 +++++++++----- HexRowReduce/README.md | 6 +++--- HexRowReduceMathlib/README.md | 6 +++--- SPEC/readme.md | 14 ++++++++------ lake-manifest.json | 10 ++++++++++ lakefile.lean | 4 ++++ 26 files changed, 104 insertions(+), 65 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 04f81e95e..36892d6e5 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -194,6 +194,13 @@ jobs: hexnumberfieldtower_emit_fixtures - name: Build HexManual run: lake build HexManual + - name: Check README Lean snippets + run: | + # lean-readme's initial release cannot process a second file after a + # file that imports modules, so use one process per README source. + for readme in Hex*/README.md scripts/release/hex-README.md; do + lake exe lean-readme "$readme" + done # Publish hex-dev's oleans on a trusted main push so later builds (and any # consumer) restore them. Skips silently without the upload key. - name: Publish hex-dev oleans to the Lake cache (main only) diff --git a/HexBareiss/README.md b/HexBareiss/README.md index 6c23cd600..5442d208e 100644 --- a/HexBareiss/README.md +++ b/HexBareiss/README.md @@ -62,7 +62,7 @@ determinant encoded by `bareissData`. The public determinant agrees with the encoded data, `bareiss_eq_bareissData_det`: -```lean +```lean nocheck theorem bareiss_eq_bareissData_det (M : Matrix Int n n) : bareiss M = (bareissData M).det ``` @@ -70,7 +70,7 @@ theorem bareiss_eq_bareissData_det (M : Matrix Int n n) : The no-pivot run, when it reaches the final pivot without a singular step, reads off the last diagonal entry, `bareiss_eq_noPivotLoop_last_of_no_singular`: -```lean +```lean nocheck theorem bareiss_eq_noPivotLoop_last_of_no_singular {k : Nat} (M : Matrix Int (k + 1) (k + 1)) (h_no_sing : diff --git a/HexBareissMathlib/README.md b/HexBareissMathlib/README.md index 734f88458..4a57242b2 100644 --- a/HexBareissMathlib/README.md +++ b/HexBareissMathlib/README.md @@ -57,14 +57,14 @@ hold outright, with no hypothesis to discharge. The executable Bareiss determinant equals the Leibniz determinant, `bareiss_eq_det`: -```lean +```lean nocheck theorem bareiss_eq_det (M : Hex.Matrix Int n n) : Hex.Matrix.bareiss M = Hex.Matrix.det M ``` It also equals Mathlib's determinant, `bareissDet_eq_det`: -```lean +```lean nocheck theorem bareissDet_eq_det (M : Hex.Matrix Int n n) : Hex.Matrix.bareiss M = Matrix.det (matrixEquiv M) ``` @@ -72,7 +72,7 @@ theorem bareissDet_eq_det (M : Hex.Matrix Int n n) : The Mathlib statement is proven directly by running the Bareiss loop and tracking the bordered-minor invariant step by step, `bareiss_eq_mathlib_det`: -```lean +```lean nocheck theorem bareiss_eq_mathlib_det (M : Hex.Matrix Int n n) : Hex.Matrix.bareiss M = Matrix.det (matrixEquiv M) ``` diff --git a/HexConway/README.md b/HexConway/README.md index c772bd74a..4a8b6e770 100644 --- a/HexConway/README.md +++ b/HexConway/README.md @@ -75,7 +75,7 @@ that the kernel replays; `native_decide` is not used anywhere. The aggregate dispatch theorem is `luebeckConwayPolynomial?_irreducible`, and the API-facing form is -```lean +```lean nocheck theorem conwayPoly_irreducible (p n : Nat) [ZMod64.Bounds p] (h : SupportedEntry p n) : FpPoly.Irreducible (conwayPoly p n h) @@ -87,7 +87,7 @@ as a negative control so the check is visibly not vacuous. The `Bool` is promoted to a statement about field elements, which is the well-definedness input a subfield embedding needs: -```lean +```lean nocheck theorem eval_conwayPoly_subfieldGen_eq_zero {p m n : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (hm : SupportedEntry p m) (hn : SupportedEntry p n) diff --git a/HexDeterminant/README.md b/HexDeterminant/README.md index f24370671..08ccb91d1 100644 --- a/HexDeterminant/README.md +++ b/HexDeterminant/README.md @@ -59,7 +59,7 @@ The headline theorem for each of the remaining results (with Column linearity, `det_setCol_add`: -```lean +```lean nocheck theorem det_setCol_add (M : Matrix R n n) (dst : Fin n) (v w : Fin n → R) : det (setCol M dst (fun r => v r + w r)) = det (setCol M dst v) + det (setCol M dst w) @@ -67,7 +67,7 @@ theorem det_setCol_add (M : Matrix R n n) (dst : Fin n) (v w : Fin n → R) : Laplace cofactor expansion along a row, `det_eq_finFoldl_laplace_row`: -```lean +```lean nocheck theorem det_eq_finFoldl_laplace_row (M : Matrix R (n + 1) (n + 1)) (row : Fin (n + 1)) : det M = Fin.foldl (n + 1) @@ -86,7 +86,7 @@ their names apart. `det_setRow_setRow_mul_det` is the two-row replacement identity, the `2 × 2` case of Jacobi's adjugate-minor identity: for distinct rows `a`, `b` and arbitrary vectors `u`, `v`, -```lean +```lean nocheck theorem det_setRow_setRow_mul_det (M : Matrix R (n + 1) (n + 1)) (a b : Fin (n + 1)) (hab : a ≠ b) (u v : Vector R (n + 1)) : diff --git a/HexDeterminantMathlib/README.md b/HexDeterminantMathlib/README.md index 8981a5c7a..8a489cc25 100644 --- a/HexDeterminantMathlib/README.md +++ b/HexDeterminantMathlib/README.md @@ -67,7 +67,7 @@ Desnanot-Jacobi. The determinant correspondence is fully proven over a `CommRing`. The headline theorem identifies the two determinants: -```lean +```lean nocheck theorem det_eq [CommRing R] (M : Hex.Matrix R n n) : Hex.Matrix.det M = Matrix.det (matrixEquiv M) ``` @@ -76,7 +76,7 @@ The unrestricted three-term Grassmann-Plücker relation, for any three ordered rows `p1 < p2 < p3` (`hex-determinant` proves the Mathlib-free specialisation where `p2` and `p3` are the last two rows): -```lean +```lean nocheck theorem det_plucker_three_term {R : Type u} [CommRing R] {n : Nat} (B : Hex.Matrix R (n + 3) (n + 1)) (v : Vector R (n + 3)) @@ -89,7 +89,7 @@ theorem det_plucker_three_term The Desnanot-Jacobi identity over Mathlib matrices: -```lean +```lean nocheck theorem desnanot_jacobi {R : Type*} [CommRing R] {n : ℕ} (M : Matrix (Fin (n + 2)) (Fin (n + 2)) R) : M.det * (M.submatrix (Fin.succAbove 0 ∘ (Fin.last n).succAbove) diff --git a/HexGF2/README.md b/HexGF2/README.md index 7feb61483..2e2e764b3 100644 --- a/HexGF2/README.md +++ b/HexGF2/README.md @@ -69,7 +69,7 @@ Irreducibility is proved rather than tabulated. The Rabin test is sound, and so is certificate replay, which is what lets a committed modulus be checked by the kernel without `native_decide`: -```lean +```lean nocheck theorem rabinTest_imp_irreducible (f : GF2Poly) (hrabin : rabinTest f = true) : GF2Poly.Irreducible f @@ -85,7 +85,7 @@ laws need more: `GF2Poly.Irreducible` is satisfied by the constant `1`, and the quotient by a constant is trivial, so nonconstancy is a separate hypothesis and the field laws are functions rather than instances. -```lean +```lean nocheck def fieldOfDegreePos (hdeg : 0 < f.degree) : Lean.Grind.Field (GF2nPoly f hirr) theorem isCharPOfDegreePos (hdeg : 0 < f.degree) : diff --git a/HexGF2Mathlib/README.md b/HexGF2Mathlib/README.md index f6c0e45bd..27e0fb7a8 100644 --- a/HexGF2Mathlib/README.md +++ b/HexGF2Mathlib/README.md @@ -65,7 +65,7 @@ compose with other `RingEquiv`s and are accepted by Mathlib's equivalence APIs. The equivalences are the content. The packed polynomial representation corresponds to the generic one, and composing reaches Mathlib: -```lean +```lean nocheck def equiv : Hex.GF2Poly ≃+* Hex.FpPoly 2 noncomputable def equivPolynomial : Hex.GF2Poly ≃+* Polynomial (ZMod 2) @@ -78,7 +78,7 @@ keep the executable operations rather than transported copies, so The single-word wrapper, in namespace `HexGF2Mathlib.GF2n`: -```lean +```lean nocheck def equiv : Hex.GF2n n irr hn hn64 hirr ≃+* GenericFiniteField (n := n) (irr := irr) (hn := hn) (hn64 := hn64) (hirr := hirr) @@ -88,7 +88,7 @@ theorem fintype_card : The arbitrary-degree wrapper, in namespace `HexGF2Mathlib.GF2nPoly`: -```lean +```lean nocheck def equiv : Hex.GF2nPoly f hirr ≃+* GenericFiniteField (f := f) (hirr := hirr) (hdeg := hdeg) theorem fintype_card : diff --git a/HexGFq/README.md b/HexGFq/README.md index 7e28c65f6..bbe2c1eb3 100644 --- a/HexGFq/README.md +++ b/HexGFq/README.md @@ -72,7 +72,7 @@ def d := GF2q.toGFq c The field type is built directly from the Conway table's proofs, so a `GFq` that elaborates is a field: -```lean +```lean nocheck abbrev GFq (p n : Nat) [ZMod64.Bounds p] (h : Conway.SupportedEntry p n) : Type := GFqField.FiniteField (Conway.conwayPoly p n h) (Conway.conwayPoly_nonconstant p n h) @@ -91,7 +91,7 @@ The packed binary constructor is the part with its own proof obligation. Each modulus, replayed from a Rabin certificate by the kernel, and a proof that the packed word denotes the same polynomial as the committed Conway entry: -```lean +```lean nocheck class PackedGF2Entry (n : Nat) where entry : SupportedEntry 2 n lower : UInt64 diff --git a/HexGFqField/README.md b/HexGFqField/README.md index 415ab27a2..e4dbb0062 100644 --- a/HexGFqField/README.md +++ b/HexGFqField/README.md @@ -71,7 +71,7 @@ example : frob α = α ^ 5 := frob_eq_pow α The field laws are proved, not asserted. Inverse cancellation is the result the rest rests on: -```lean +```lean nocheck theorem mul_inv_cancel {f : FpPoly p} {hf : 0 < FpPoly.degree f} {hirr : FpPoly.Irreducible f} {x : FiniteField f hf hp hirr} (hx : x ≠ 0) : @@ -84,7 +84,7 @@ instances, which hold for every modulus the type admits, because the type already carries both the irreducibility proof and the positive-degree hypothesis: -```lean +```lean nocheck instance {f : FpPoly p} {hf : 0 < FpPoly.degree f} {hirr : FpPoly.Irreducible f} : Lean.Grind.Field (FiniteField f hf hp hirr) diff --git a/HexGFqMathlib/README.md b/HexGFqMathlib/README.md index 516ef6947..7ece9fd4c 100644 --- a/HexGFqMathlib/README.md +++ b/HexGFqMathlib/README.md @@ -69,7 +69,7 @@ example {p n : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] The executable field carries Mathlib's `Field` structure, and the carrier is finite with the cardinality its construction promises: -```lean +```lean nocheck noncomputable instance field : Field (Hex.GFqField.FiniteField f hf hp hirr) @@ -86,7 +86,7 @@ Cardinality is the whole input to the Mathlib correspondence. that the two counts agree, so it needs `Fact p.Prime` and `n ≠ 0` as hypotheses, neither of which the executable side carries: -```lean +```lean nocheck noncomputable def equivGaloisField [Fact p.Prime] (h : Hex.Conway.SupportedEntry p n) (hn : n ≠ 0) : _root_.RingEquiv (Hex.GFq p n h) (GaloisField p n) @@ -96,7 +96,7 @@ The packed binary constructor reaches the same place in two legs, the first built on hex-gf2-mathlib's `GF2n.equiv` and computable, the second inheriting the choice `ringEquivOfCardEq` makes: -```lean +```lean nocheck def equivGFq : RingEquiv (GF2q n) (GFq 2 n h.entry) noncomputable def equivGaloisField : RingEquiv (GF2q n) (GaloisField 2 n) @@ -105,7 +105,7 @@ noncomputable def equivGaloisField : RingEquiv (GF2q n) (GaloisField 2 n) The subfield embedding is a genuine ring homomorphism, on a committed divisor pair carrying a `Conway.Compatible` witness rather than a bare `m ∣ n` proof: -```lean +```lean nocheck noncomputable def conwayEmbed (p m n : Nat) [Hex.ZMod64.Bounds p] [Hex.ZMod64.PrimeModulus p] (hm : Hex.Conway.SupportedEntry p m) (hn : Hex.Conway.SupportedEntry p n) diff --git a/HexGramSchmidt/README.md b/HexGramSchmidt/README.md index 83909da32..990d32484 100644 --- a/HexGramSchmidt/README.md +++ b/HexGramSchmidt/README.md @@ -71,7 +71,7 @@ lower-unitriangular coefficient matrix) are available over both rings. The orthogonalization theory is proven over the Mathlib-free integer and rational cores. The orthogonal basis, `basis_orthogonal`: -```lean +```lean nocheck theorem basis_orthogonal (b : Matrix Int n m) (i j : Nat) (hi : i < n) (hj : j < n) (hij : i ≠ j) : ((basis b).row ⟨i, hi⟩).dotProduct ((basis b).row ⟨j, hj⟩) = 0 @@ -82,7 +82,7 @@ coefficient laws `coeffs_diag` and `coeffs_upper`, the span equality `basis_span`, and the update laws for `sizeReduce` and `adjacentSwap`. The key lattice estimate, `normSq_latticeVec_ge_min_basis_normSq`: -```lean +```lean nocheck theorem normSq_latticeVec_ge_min_basis_normSq (b : Matrix Int n m) (_hli : independent b) (v : Vector Int m) (hv : memLattice b v) (hv' : v ≠ 0) : diff --git a/HexGramSchmidtMathlib/README.md b/HexGramSchmidtMathlib/README.md index b0bcb1769..7ee36eae0 100644 --- a/HexGramSchmidtMathlib/README.md +++ b/HexGramSchmidtMathlib/README.md @@ -61,7 +61,7 @@ The proof-facing API splits into two parts. The rowwise correspondence with Mathlib's orthogonalization is fully proven. Over the rationals: -```lean +```lean nocheck theorem rat_basis_row_eq_gramSchmidt (b : Matrix Rat n m) (i : Fin n) : rowToEuclidean ((Hex.GramSchmidt.Rat.basis b).row i) = InnerProductSpace.gramSchmidt ℝ (ratRowFamily b) i @@ -69,7 +69,7 @@ theorem rat_basis_row_eq_gramSchmidt (b : Matrix Rat n m) (i : Fin n) : and the integer version, casting the integer rows first: -```lean +```lean nocheck theorem int_basis_row_eq_gramSchmidt (b : Matrix Int n m) (i : Fin n) : rowToEuclidean ((Hex.GramSchmidt.Int.basis b).row i) = InnerProductSpace.gramSchmidt ℝ (intRowFamily b) i @@ -78,7 +78,7 @@ theorem int_basis_row_eq_gramSchmidt (b : Matrix Int n m) (i : Fin n) : The fraction-free integer surface is identified with Bareiss determinants. Below the diagonal the scaled coefficients are exactly: -```lean +```lean nocheck theorem scaledCoeffs_eq_scaledCoeffMatrix_bareiss (b : Matrix Int n m) (i j : Fin n) (hji : j.val < i.val) : GramSchmidt.entry (scaledCoeffs b) i j = @@ -88,7 +88,7 @@ theorem scaledCoeffs_eq_scaledCoeffMatrix_bareiss and for an independent matrix the leading Gram determinant is the product of squared Gram-Schmidt norms: -```lean +```lean nocheck theorem gramDet_eq_prod_normSq (b : Matrix Int n m) (hli : independent b) (k : Nat) (hk : k ≤ n) : (gramDet b k hk : Rat) = gramSchmidtNormProduct b k hk diff --git a/HexMatrixMathlib/README.md b/HexMatrixMathlib/README.md index cfa6ddb46..4b14ebb15 100644 --- a/HexMatrixMathlib/README.md +++ b/HexMatrixMathlib/README.md @@ -68,11 +68,11 @@ two representations. The headline equivalence sends each matrix to the Mathlib matrix with the same entries: -```lean +```lean nocheck def matrixEquiv : Hex.Matrix R n m ≃ Matrix (Fin n) (Fin m) R ``` -```lean +```lean nocheck theorem matrixEquiv_apply (M : Hex.Matrix R n m) (i : Fin n) (j : Fin m) : matrixEquiv M i j = M[i][j] ``` @@ -80,14 +80,14 @@ theorem matrixEquiv_apply (M : Hex.Matrix R n m) (i : Fin n) (j : Fin m) : The elementary row operations correspond to Mathlib's elementary matrices. A swap is left multiplication by the permutation matrix `Matrix.swap`: -```lean +```lean nocheck theorem matrixEquiv_rowSwap (M : Hex.Matrix R n m) (i j : Fin n) : matrixEquiv (Hex.Matrix.rowSwap M i j) = Matrix.swap R i j * matrixEquiv M ``` A row addition is left multiplication by `Matrix.transvection`: -```lean +```lean nocheck theorem matrixEquiv_rowAdd (M : Hex.Matrix R n m) (src dst : Fin n) (c : R) : matrixEquiv (Hex.Matrix.rowAdd M src dst c) = Matrix.transvection dst src c * matrixEquiv M @@ -95,7 +95,7 @@ theorem matrixEquiv_rowAdd (M : Hex.Matrix R n m) (src dst : Fin n) (c : R) : The matrix-vector product transports to Mathlib's `Matrix.mulVec`: -```lean +```lean nocheck theorem vectorEquiv_mulVec [Semiring R] (M : Hex.Matrix R n m) (v : Vector R m) : vectorEquiv (M * v) = (matrixEquiv M).mulVec (vectorEquiv v) ``` diff --git a/HexMvPoly/README.md b/HexMvPoly/README.md index 9842e7bb0..08f587292 100644 --- a/HexMvPoly/README.md +++ b/HexMvPoly/README.md @@ -64,7 +64,7 @@ recursive-view laws. A product coefficient is the convolution over every monomial split: -```lean +```lean nocheck theorem coeff_mul [Lean.Grind.Semiring R] [DecidableEq R] (m : Mono n) (p q : MvPoly n R cmp) : coeff m (p * q) = @@ -74,7 +74,7 @@ theorem coeff_mul [Lean.Grind.Semiring R] [DecidableEq R] Sparse Horner evaluation agrees with direct evaluation: -```lean +```lean nocheck theorem evalHorner_eq [Lean.Grind.CommSemiring R] (x : Fin n → R) (p : MvPoly n R cmp) : evalHorner x p = eval x p diff --git a/HexMvPolyMathlib/README.md b/HexMvPolyMathlib/README.md index 92ad256ce..574dfbfbd 100644 --- a/HexMvPolyMathlib/README.md +++ b/HexMvPolyMathlib/README.md @@ -57,14 +57,14 @@ example (p q : P) : The correspondence is fully proven in both directions: -```lean +```lean nocheck def equiv [CommSemiring R] [DecidableEq R] : MvPoly n R cmp ≃+* MvPolynomial (Fin n) R ``` It preserves every coefficient: -```lean +```lean nocheck theorem coeff_toMvPolynomial [CommSemiring R] [DecidableEq R] (m : Mono n) (p : MvPoly n R cmp) : MvPolynomial.coeff (monoEquiv m) (toMvPolynomial p) = @@ -73,7 +73,7 @@ theorem coeff_toMvPolynomial [CommSemiring R] [DecidableEq R] Executable evaluation is Mathlib algebra evaluation after conversion: -```lean +```lean nocheck theorem aeval_apply [CommSemiring R] [DecidableEq R] [CommSemiring S] [Algebra R S] (x : Fin n → S) (p : MvPoly n R cmp) : diff --git a/HexPolyFpMathlib/README.md b/HexPolyFpMathlib/README.md index 40346bd51..087e41db7 100644 --- a/HexPolyFpMathlib/README.md +++ b/HexPolyFpMathlib/README.md @@ -48,7 +48,7 @@ polynomials and Mathlib's: The headline result is the ring equivalence: -```lean +```lean nocheck def fpPolyEquiv : Hex.FpPoly p ≃+* Polynomial (ZMod p) ``` diff --git a/HexRealRoots/README.md b/HexRealRoots/README.md index 0f98f2f45..abcb3dc27 100644 --- a/HexRealRoots/README.md +++ b/HexRealRoots/README.md @@ -28,6 +28,8 @@ import HexRealRoots # Functionality ```lean +import HexRealRoots + open Hex def p : ZPoly := DensePoly.ofCoeffs #[-2, 0, 0, 0, 1] @@ -38,11 +40,13 @@ def p : ZPoly := DensePoly.ofCoeffs #[-2, 0, 0, 0, 1] The stable executable API is: ```lean -Hex.isolate? -- Descartes search, certified by Sturm; Sturm fallback -Hex.isolateSturm? -- direct Sturm bisection -Hex.isolateDescartes? -- Descartes-only search, still Sturm-certified -Hex.rootCount -- exact total real-root count -Hex.sturmCount -- exact count in one half-open interval +import HexRealRoots + +#check Hex.isolate? -- Descartes search, certified by Sturm; Sturm fallback +#check Hex.isolateSturm? -- direct Sturm bisection +#check Hex.isolateDescartes? -- Descartes-only search, still Sturm-certified +#check Hex.rootCount -- exact total real-root count +#check Hex.sturmCount -- exact count in one half-open interval ``` `isolate?` rejects the zero polynomial and, at the core level, expects a diff --git a/HexRealRootsMathlib/README.md b/HexRealRootsMathlib/README.md index 1aa8f199a..58d8083cb 100644 --- a/HexRealRootsMathlib/README.md +++ b/HexRealRootsMathlib/README.md @@ -28,6 +28,8 @@ import HexRealRootsMathlib # Functionality ```lean +import HexRealRootsMathlib + open Hex Polynomial noncomputable def roots := @@ -46,6 +48,10 @@ real roots. An optional exact width refines every interval: ```lean +import HexRealRootsMathlib + +open Hex Polynomial + noncomputable def tight := isolate_roots (width := 2 ^ (-20 : ℤ)) (X ^ 4 - 2 : Polynomial ℝ) diff --git a/HexRoots/README.md b/HexRoots/README.md index aff5a7074..3a534d995 100644 --- a/HexRoots/README.md +++ b/HexRoots/README.md @@ -29,6 +29,8 @@ import HexRoots # Functionality ```lean +import HexRoots + open Hex def p : ZPoly := DensePoly.ofCoeffs #[-1, -1, 0, 1] diff --git a/HexRootsMathlib/README.md b/HexRootsMathlib/README.md index 9eb57c699..7e83333ea 100644 --- a/HexRootsMathlib/README.md +++ b/HexRootsMathlib/README.md @@ -31,6 +31,8 @@ import HexRootsMathlib the hypotheses required by completeness: ```lean +import HexRootsMathlib + open Hex HexRootsMathlib def p : ZPoly := DensePoly.ofCoeffs #[-1, -1, 0, 1] @@ -45,11 +47,13 @@ noncomputable def roots : Array (DyadicRootIsolation p) := The associated theorems are the main consumption surface: ```lean -isolate!_eq -- the array is the successful Hex.isolate result -isolate!_count -- one atom per complex root -isolate!_roots -- selected semantic roots equal p.roots.toFinset -isolate!_prec -- every square meets the requested precision -isolate!_disjoint -- distinct squares have disjoint circumscribed discs +import HexRootsMathlib + +#check HexRootsMathlib.isolate!_eq -- the successful Hex.isolate result +#check HexRootsMathlib.isolate!_count -- one atom per complex root +#check HexRootsMathlib.isolate!_roots -- selected roots equal p.roots.toFinset +#check HexRootsMathlib.isolate!_prec -- every square meets the requested precision +#check HexRootsMathlib.isolate!_disjoint -- distinct squares have disjoint discs ``` Clients that already have a successful `Hex.isolate` call can instead use diff --git a/HexRowReduce/README.md b/HexRowReduce/README.md index 9d7f6701c..c2e1e0983 100644 --- a/HexRowReduce/README.md +++ b/HexRowReduce/README.md @@ -58,13 +58,13 @@ Over a field the reduction is fully proven. The headline theorem states that sorted and equal to 1, all other pivot-column entries zero, trailing rows zero, and an invertible transform with `transform * M = echelon`): -```lean +```lean nocheck theorem rowReduce_isRowReduced (M : Matrix R n m) : IsRowReduced M (rowReduce M) ``` The row-span wrappers are sound, with `spanCoeffs_sound`: -```lean +```lean nocheck theorem spanCoeffs_sound [Lean.Grind.Field R] [DecidableEq R] (M : Matrix R n m) (v : Vector R m) (c : Vector R n) : spanCoeffs M v = some c → rowCombination M c = v @@ -73,7 +73,7 @@ theorem spanCoeffs_sound [Lean.Grind.Field R] [DecidableEq R] The nullspace basis is both sound and complete, `nullspace_sound` and `nullspace_complete`: -```lean +```lean nocheck theorem nullspace_sound [Lean.Grind.Field R] [DecidableEq R] (M : Matrix R n m) (k : Fin (m - rowReduce_rank M)) : M * (nullspace M).get k = 0 diff --git a/HexRowReduceMathlib/README.md b/HexRowReduceMathlib/README.md index 7f152aa2d..922959a22 100644 --- a/HexRowReduceMathlib/README.md +++ b/HexRowReduceMathlib/README.md @@ -64,7 +64,7 @@ row span, and nullspace are computable witnesses for Mathlib's noncomputable Rank, `rank_eq`: -```lean +```lean nocheck theorem rank_eq [Field R] {M : Hex.Matrix R n m} {D : Hex.Matrix.RowEchelonData R n m} (E : Hex.Matrix.IsRowReduced M D) : @@ -73,7 +73,7 @@ theorem rank_eq [Field R] Nullspace, `nullspace_span_eq_ker`: -```lean +```lean nocheck theorem nullspace_span_eq_ker [Field R] {M : Hex.Matrix R n m} {D : Hex.Matrix.RowEchelonData R n m} (E : Hex.Matrix.IsRowReduced M D) : @@ -83,7 +83,7 @@ theorem nullspace_span_eq_ker [Field R] Span, `spanContains_iff_mem_span`: -```lean +```lean nocheck theorem spanContains_iff_mem_span [Field R] [DecidableEq R] {M : Hex.Matrix R n m} {D : Hex.Matrix.RowEchelonData R n m} (E : Hex.Matrix.IsRowReduced M D) (v : Vector R m) : diff --git a/SPEC/readme.md b/SPEC/readme.md index c52c26c4e..c0beb05b7 100644 --- a/SPEC/readme.md +++ b/SPEC/readme.md @@ -29,10 +29,11 @@ Use these five level-1 headings, in this order. 2. **`# Quickstart`**. The `lakefile.toml` `[[require]]` block for the released repo, followed by a single code block of at most 20 lines that shows off the executable surface. The code must compile; build-check it - against the monorepo before committing (a throwaway file run through - `lake env lean`, or as a temporary module). For a `*-mathlib` library - with no executable surface of its own, show the correspondence instead: - import the bridge and state the headline equivalence or transfer lemma. + against the monorepo before committing. CI checks every executable Lean + block with `lean-readme`; make each block self-contained, including its + imports. For a `*-mathlib` library with no executable surface of its own, + show the correspondence instead: import the bridge and state the headline + equivalence or transfer lemma. 3. **`# Functionality`**. A brief, non-exhaustive description of the executable operations the library provides. Bullets, naming the real @@ -44,8 +45,9 @@ Use these five level-1 headings, in this order. for executable use only. Where it helps the reader, quote the headline theorem for each significant result as a Lean signature (name plus statement, proof elided) in a `lean` code block, copied verbatim from - the source so it stays accurate. Point at the sibling library where the - rest of the theory lives. + the source so it stays accurate. Mark these intentionally incomplete + signature blocks as `lean nocheck`; executable examples must remain checked. + Point at the sibling library where the rest of the theory lives. 5. **`# Contributing`**. State that development happens in the [`hex-dev`](https://github.com/kim-em/hex-dev) monorepo, not in the diff --git a/lake-manifest.json b/lake-manifest.json index 5f5b01e43..520c158ad 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -21,6 +21,16 @@ "inputRev": "master", "inherited": false, "configFile": "lakefile.toml"}, + {"url": "https://github.com/david-christiansen/lean-readme.git", + "type": "git", + "subDir": null, + "scope": "", + "rev": "cccf47290b379d39972b659dd3ede88ebe3c1018", + "name": "«lean-readme»", + "manifestFile": "lake-manifest.json", + "inputRev": "cccf47290b379d39972b659dd3ede88ebe3c1018", + "inherited": false, + "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover/verso.git", "type": "git", "subDir": null, diff --git a/lakefile.lean b/lakefile.lean index ff87edbbb..3ab43562f 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -14,6 +14,10 @@ package Hex where require verso from git "https://github.com/leanprover/verso.git" @ "v4.33.0-rc1" +require «lean-readme» from git + "https://github.com/david-christiansen/lean-readme.git" @ + "cccf47290b379d39972b659dd3ede88ebe3c1018" + require «lean-bench» from git "https://github.com/kim-em/lean-bench.git" @ "master" From 4a4e95cffdf795bb7032a93efe4c6a171c8a9aac Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Sun, 23 Aug 2026 11:06:24 +0000 Subject: [PATCH 02/16] fix: check quoted README theorem signatures --- HexBareiss/README.md | 12 ++++++++++-- HexBareissMathlib/README.md | 18 +++++++++++++++--- HexConway/README.md | 12 ++++++++++-- HexDeterminant/README.md | 18 +++++++++++++++--- HexDeterminantMathlib/README.md | 18 +++++++++++++++--- HexGF2/README.md | 12 ++++++++++-- HexGF2Mathlib/README.md | 18 +++++++++++++++--- HexGFq/README.md | 12 ++++++++++-- HexGFqField/README.md | 12 ++++++++++-- HexGFqMathlib/README.md | 24 ++++++++++++++++++++---- HexGramSchmidt/README.md | 12 ++++++++++-- HexGramSchmidtMathlib/README.md | 24 ++++++++++++++++++++---- HexMatrixMathlib/README.md | 30 +++++++++++++++++++++++++----- HexMvPoly/README.md | 12 ++++++++++-- HexMvPolyMathlib/README.md | 21 ++++++++++++++++++--- HexPolyFpMathlib/README.md | 4 +++- HexRowReduce/README.md | 18 +++++++++++++++--- HexRowReduceMathlib/README.md | 18 +++++++++++++++--- SPEC/readme.md | 10 +++++++--- lake-manifest.json | 6 +++--- lakefile.lean | 4 ++-- 21 files changed, 258 insertions(+), 57 deletions(-) diff --git a/HexBareiss/README.md b/HexBareiss/README.md index 5442d208e..144850727 100644 --- a/HexBareiss/README.md +++ b/HexBareiss/README.md @@ -62,7 +62,11 @@ determinant encoded by `bareissData`. The public determinant agrees with the encoded data, `bareiss_eq_bareissData_det`: -```lean nocheck +```lean recall +import HexBareiss + +open Hex + theorem bareiss_eq_bareissData_det (M : Matrix Int n n) : bareiss M = (bareissData M).det ``` @@ -70,7 +74,11 @@ theorem bareiss_eq_bareissData_det (M : Matrix Int n n) : The no-pivot run, when it reaches the final pivot without a singular step, reads off the last diagonal entry, `bareiss_eq_noPivotLoop_last_of_no_singular`: -```lean nocheck +```lean recall +import HexBareiss + +open Hex + theorem bareiss_eq_noPivotLoop_last_of_no_singular {k : Nat} (M : Matrix Int (k + 1) (k + 1)) (h_no_sing : diff --git a/HexBareissMathlib/README.md b/HexBareissMathlib/README.md index 4a57242b2..ba32754f0 100644 --- a/HexBareissMathlib/README.md +++ b/HexBareissMathlib/README.md @@ -57,14 +57,22 @@ hold outright, with no hypothesis to discharge. The executable Bareiss determinant equals the Leibniz determinant, `bareiss_eq_det`: -```lean nocheck +```lean recall +import HexBareissMathlib + +open HexMatrixMathlib + theorem bareiss_eq_det (M : Hex.Matrix Int n n) : Hex.Matrix.bareiss M = Hex.Matrix.det M ``` It also equals Mathlib's determinant, `bareissDet_eq_det`: -```lean nocheck +```lean recall +import HexBareissMathlib + +open HexMatrixMathlib + theorem bareissDet_eq_det (M : Hex.Matrix Int n n) : Hex.Matrix.bareiss M = Matrix.det (matrixEquiv M) ``` @@ -72,7 +80,11 @@ theorem bareissDet_eq_det (M : Hex.Matrix Int n n) : The Mathlib statement is proven directly by running the Bareiss loop and tracking the bordered-minor invariant step by step, `bareiss_eq_mathlib_det`: -```lean nocheck +```lean recall +import HexBareissMathlib + +open HexMatrixMathlib + theorem bareiss_eq_mathlib_det (M : Hex.Matrix Int n n) : Hex.Matrix.bareiss M = Matrix.det (matrixEquiv M) ``` diff --git a/HexConway/README.md b/HexConway/README.md index 4a8b6e770..860144d82 100644 --- a/HexConway/README.md +++ b/HexConway/README.md @@ -75,7 +75,11 @@ that the kernel replays; `native_decide` is not used anywhere. The aggregate dispatch theorem is `luebeckConwayPolynomial?_irreducible`, and the API-facing form is -```lean nocheck +```lean recall +import HexConway + +open Hex Hex.Conway + theorem conwayPoly_irreducible (p n : Nat) [ZMod64.Bounds p] (h : SupportedEntry p n) : FpPoly.Irreducible (conwayPoly p n h) @@ -87,7 +91,11 @@ as a negative control so the check is visibly not vacuous. The `Bool` is promoted to a statement about field elements, which is the well-definedness input a subfield embedding needs: -```lean nocheck +```lean recall +import HexConway + +open Hex Hex.Conway + theorem eval_conwayPoly_subfieldGen_eq_zero {p m n : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (hm : SupportedEntry p m) (hn : SupportedEntry p n) diff --git a/HexDeterminant/README.md b/HexDeterminant/README.md index 08ccb91d1..57fbccc70 100644 --- a/HexDeterminant/README.md +++ b/HexDeterminant/README.md @@ -59,7 +59,11 @@ The headline theorem for each of the remaining results (with Column linearity, `det_setCol_add`: -```lean nocheck +```lean recall +import HexDeterminant + +open Hex + theorem det_setCol_add (M : Matrix R n n) (dst : Fin n) (v w : Fin n → R) : det (setCol M dst (fun r => v r + w r)) = det (setCol M dst v) + det (setCol M dst w) @@ -67,7 +71,11 @@ theorem det_setCol_add (M : Matrix R n n) (dst : Fin n) (v w : Fin n → R) : Laplace cofactor expansion along a row, `det_eq_finFoldl_laplace_row`: -```lean nocheck +```lean recall +import HexDeterminant + +open Hex + theorem det_eq_finFoldl_laplace_row (M : Matrix R (n + 1) (n + 1)) (row : Fin (n + 1)) : det M = Fin.foldl (n + 1) @@ -86,7 +94,11 @@ their names apart. `det_setRow_setRow_mul_det` is the two-row replacement identity, the `2 × 2` case of Jacobi's adjugate-minor identity: for distinct rows `a`, `b` and arbitrary vectors `u`, `v`, -```lean nocheck +```lean recall +import HexDeterminant + +open Hex + theorem det_setRow_setRow_mul_det (M : Matrix R (n + 1) (n + 1)) (a b : Fin (n + 1)) (hab : a ≠ b) (u v : Vector R (n + 1)) : diff --git a/HexDeterminantMathlib/README.md b/HexDeterminantMathlib/README.md index 8a489cc25..baa0bea1f 100644 --- a/HexDeterminantMathlib/README.md +++ b/HexDeterminantMathlib/README.md @@ -67,7 +67,11 @@ Desnanot-Jacobi. The determinant correspondence is fully proven over a `CommRing`. The headline theorem identifies the two determinants: -```lean nocheck +```lean recall +import HexDeterminantMathlib + +open Hex HexMatrixMathlib + theorem det_eq [CommRing R] (M : Hex.Matrix R n n) : Hex.Matrix.det M = Matrix.det (matrixEquiv M) ``` @@ -76,7 +80,11 @@ The unrestricted three-term Grassmann-Plücker relation, for any three ordered rows `p1 < p2 < p3` (`hex-determinant` proves the Mathlib-free specialisation where `p2` and `p3` are the last two rows): -```lean nocheck +```lean recall +import HexDeterminantMathlib + +open Hex HexMatrixMathlib + theorem det_plucker_three_term {R : Type u} [CommRing R] {n : Nat} (B : Hex.Matrix R (n + 3) (n + 1)) (v : Vector R (n + 3)) @@ -89,7 +97,11 @@ theorem det_plucker_three_term The Desnanot-Jacobi identity over Mathlib matrices: -```lean nocheck +```lean recall +import HexDeterminantMathlib + +open Hex HexMatrixMathlib + theorem desnanot_jacobi {R : Type*} [CommRing R] {n : ℕ} (M : Matrix (Fin (n + 2)) (Fin (n + 2)) R) : M.det * (M.submatrix (Fin.succAbove 0 ∘ (Fin.last n).succAbove) diff --git a/HexGF2/README.md b/HexGF2/README.md index 2e2e764b3..89a92ee06 100644 --- a/HexGF2/README.md +++ b/HexGF2/README.md @@ -69,7 +69,11 @@ Irreducibility is proved rather than tabulated. The Rabin test is sound, and so is certificate replay, which is what lets a committed modulus be checked by the kernel without `native_decide`: -```lean nocheck +```lean recall +import HexGF2 + +open Hex + theorem rabinTest_imp_irreducible (f : GF2Poly) (hrabin : rabinTest f = true) : GF2Poly.Irreducible f @@ -85,7 +89,11 @@ laws need more: `GF2Poly.Irreducible` is satisfied by the constant `1`, and the quotient by a constant is trivial, so nonconstancy is a separate hypothesis and the field laws are functions rather than instances. -```lean nocheck +```lean recall +import HexGF2 + +open Hex + def fieldOfDegreePos (hdeg : 0 < f.degree) : Lean.Grind.Field (GF2nPoly f hirr) theorem isCharPOfDegreePos (hdeg : 0 < f.degree) : diff --git a/HexGF2Mathlib/README.md b/HexGF2Mathlib/README.md index 27e0fb7a8..fab8365dd 100644 --- a/HexGF2Mathlib/README.md +++ b/HexGF2Mathlib/README.md @@ -65,7 +65,11 @@ compose with other `RingEquiv`s and are accepted by Mathlib's equivalence APIs. The equivalences are the content. The packed polynomial representation corresponds to the generic one, and composing reaches Mathlib: -```lean nocheck +```lean +import HexGF2Mathlib + +open Hex + def equiv : Hex.GF2Poly ≃+* Hex.FpPoly 2 noncomputable def equivPolynomial : Hex.GF2Poly ≃+* Polynomial (ZMod 2) @@ -78,7 +82,11 @@ keep the executable operations rather than transported copies, so The single-word wrapper, in namespace `HexGF2Mathlib.GF2n`: -```lean nocheck +```lean recall +import HexGF2Mathlib + +open Hex + def equiv : Hex.GF2n n irr hn hn64 hirr ≃+* GenericFiniteField (n := n) (irr := irr) (hn := hn) (hn64 := hn64) (hirr := hirr) @@ -88,7 +96,11 @@ theorem fintype_card : The arbitrary-degree wrapper, in namespace `HexGF2Mathlib.GF2nPoly`: -```lean nocheck +```lean recall +import HexGF2Mathlib + +open Hex + def equiv : Hex.GF2nPoly f hirr ≃+* GenericFiniteField (f := f) (hirr := hirr) (hdeg := hdeg) theorem fintype_card : diff --git a/HexGFq/README.md b/HexGFq/README.md index bbe2c1eb3..31a192ee8 100644 --- a/HexGFq/README.md +++ b/HexGFq/README.md @@ -72,7 +72,11 @@ def d := GF2q.toGFq c The field type is built directly from the Conway table's proofs, so a `GFq` that elaborates is a field: -```lean nocheck +```lean +import HexGFq + +open Hex + abbrev GFq (p n : Nat) [ZMod64.Bounds p] (h : Conway.SupportedEntry p n) : Type := GFqField.FiniteField (Conway.conwayPoly p n h) (Conway.conwayPoly_nonconstant p n h) @@ -91,7 +95,11 @@ The packed binary constructor is the part with its own proof obligation. Each modulus, replayed from a Rabin certificate by the kernel, and a proof that the packed word denotes the same polynomial as the committed Conway entry: -```lean nocheck +```lean +import HexGFq + +open Hex + class PackedGF2Entry (n : Nat) where entry : SupportedEntry 2 n lower : UInt64 diff --git a/HexGFqField/README.md b/HexGFqField/README.md index e4dbb0062..d2814f2d0 100644 --- a/HexGFqField/README.md +++ b/HexGFqField/README.md @@ -71,7 +71,11 @@ example : frob α = α ^ 5 := frob_eq_pow α The field laws are proved, not asserted. Inverse cancellation is the result the rest rests on: -```lean nocheck +```lean recall +import HexGFqField + +open Hex Hex.GFqField + theorem mul_inv_cancel {f : FpPoly p} {hf : 0 < FpPoly.degree f} {hirr : FpPoly.Irreducible f} {x : FiniteField f hf hp hirr} (hx : x ≠ 0) : @@ -84,7 +88,11 @@ instances, which hold for every modulus the type admits, because the type already carries both the irreducibility proof and the positive-degree hypothesis: -```lean nocheck +```lean +import HexGFqField + +open Hex Hex.GFqField + instance {f : FpPoly p} {hf : 0 < FpPoly.degree f} {hirr : FpPoly.Irreducible f} : Lean.Grind.Field (FiniteField f hf hp hirr) diff --git a/HexGFqMathlib/README.md b/HexGFqMathlib/README.md index 7ece9fd4c..1facc21ea 100644 --- a/HexGFqMathlib/README.md +++ b/HexGFqMathlib/README.md @@ -69,7 +69,11 @@ example {p n : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] The executable field carries Mathlib's `Field` structure, and the carrier is finite with the cardinality its construction promises: -```lean nocheck +```lean recall +import HexGFqMathlib + +open Hex + noncomputable instance field : Field (Hex.GFqField.FiniteField f hf hp hirr) @@ -86,7 +90,11 @@ Cardinality is the whole input to the Mathlib correspondence. that the two counts agree, so it needs `Fact p.Prime` and `n ≠ 0` as hypotheses, neither of which the executable side carries: -```lean nocheck +```lean +import HexGFqMathlib + +open Hex + noncomputable def equivGaloisField [Fact p.Prime] (h : Hex.Conway.SupportedEntry p n) (hn : n ≠ 0) : _root_.RingEquiv (Hex.GFq p n h) (GaloisField p n) @@ -96,7 +104,11 @@ The packed binary constructor reaches the same place in two legs, the first built on hex-gf2-mathlib's `GF2n.equiv` and computable, the second inheriting the choice `ringEquivOfCardEq` makes: -```lean nocheck +```lean +import HexGFqMathlib + +open Hex + def equivGFq : RingEquiv (GF2q n) (GFq 2 n h.entry) noncomputable def equivGaloisField : RingEquiv (GF2q n) (GaloisField 2 n) @@ -105,7 +117,11 @@ noncomputable def equivGaloisField : RingEquiv (GF2q n) (GaloisField 2 n) The subfield embedding is a genuine ring homomorphism, on a committed divisor pair carrying a `Conway.Compatible` witness rather than a bare `m ∣ n` proof: -```lean nocheck +```lean +import HexGFqMathlib + +open Hex + noncomputable def conwayEmbed (p m n : Nat) [Hex.ZMod64.Bounds p] [Hex.ZMod64.PrimeModulus p] (hm : Hex.Conway.SupportedEntry p m) (hn : Hex.Conway.SupportedEntry p n) diff --git a/HexGramSchmidt/README.md b/HexGramSchmidt/README.md index 990d32484..5a8e320be 100644 --- a/HexGramSchmidt/README.md +++ b/HexGramSchmidt/README.md @@ -71,7 +71,11 @@ lower-unitriangular coefficient matrix) are available over both rings. The orthogonalization theory is proven over the Mathlib-free integer and rational cores. The orthogonal basis, `basis_orthogonal`: -```lean nocheck +```lean recall +import HexGramSchmidt + +open Hex + theorem basis_orthogonal (b : Matrix Int n m) (i j : Nat) (hi : i < n) (hj : j < n) (hij : i ≠ j) : ((basis b).row ⟨i, hi⟩).dotProduct ((basis b).row ⟨j, hj⟩) = 0 @@ -82,7 +86,11 @@ coefficient laws `coeffs_diag` and `coeffs_upper`, the span equality `basis_span`, and the update laws for `sizeReduce` and `adjacentSwap`. The key lattice estimate, `normSq_latticeVec_ge_min_basis_normSq`: -```lean nocheck +```lean recall +import HexGramSchmidt + +open Hex + theorem normSq_latticeVec_ge_min_basis_normSq (b : Matrix Int n m) (_hli : independent b) (v : Vector Int m) (hv : memLattice b v) (hv' : v ≠ 0) : diff --git a/HexGramSchmidtMathlib/README.md b/HexGramSchmidtMathlib/README.md index 7ee36eae0..51b571e9a 100644 --- a/HexGramSchmidtMathlib/README.md +++ b/HexGramSchmidtMathlib/README.md @@ -61,7 +61,11 @@ The proof-facing API splits into two parts. The rowwise correspondence with Mathlib's orthogonalization is fully proven. Over the rationals: -```lean nocheck +```lean recall +import HexGramSchmidtMathlib + +open Hex + theorem rat_basis_row_eq_gramSchmidt (b : Matrix Rat n m) (i : Fin n) : rowToEuclidean ((Hex.GramSchmidt.Rat.basis b).row i) = InnerProductSpace.gramSchmidt ℝ (ratRowFamily b) i @@ -69,7 +73,11 @@ theorem rat_basis_row_eq_gramSchmidt (b : Matrix Rat n m) (i : Fin n) : and the integer version, casting the integer rows first: -```lean nocheck +```lean recall +import HexGramSchmidtMathlib + +open Hex + theorem int_basis_row_eq_gramSchmidt (b : Matrix Int n m) (i : Fin n) : rowToEuclidean ((Hex.GramSchmidt.Int.basis b).row i) = InnerProductSpace.gramSchmidt ℝ (intRowFamily b) i @@ -78,7 +86,11 @@ theorem int_basis_row_eq_gramSchmidt (b : Matrix Int n m) (i : Fin n) : The fraction-free integer surface is identified with Bareiss determinants. Below the diagonal the scaled coefficients are exactly: -```lean nocheck +```lean recall +import HexGramSchmidtMathlib + +open Hex + theorem scaledCoeffs_eq_scaledCoeffMatrix_bareiss (b : Matrix Int n m) (i j : Fin n) (hji : j.val < i.val) : GramSchmidt.entry (scaledCoeffs b) i j = @@ -88,7 +100,11 @@ theorem scaledCoeffs_eq_scaledCoeffMatrix_bareiss and for an independent matrix the leading Gram determinant is the product of squared Gram-Schmidt norms: -```lean nocheck +```lean recall +import HexGramSchmidtMathlib + +open Hex + theorem gramDet_eq_prod_normSq (b : Matrix Int n m) (hli : independent b) (k : Nat) (hk : k ≤ n) : (gramDet b k hk : Rat) = gramSchmidtNormProduct b k hk diff --git a/HexMatrixMathlib/README.md b/HexMatrixMathlib/README.md index 4b14ebb15..f0a67b1de 100644 --- a/HexMatrixMathlib/README.md +++ b/HexMatrixMathlib/README.md @@ -68,11 +68,19 @@ two representations. The headline equivalence sends each matrix to the Mathlib matrix with the same entries: -```lean nocheck +```lean +import HexMatrixMathlib + +open Hex HexMatrixMathlib + def matrixEquiv : Hex.Matrix R n m ≃ Matrix (Fin n) (Fin m) R ``` -```lean nocheck +```lean recall +import HexMatrixMathlib + +open Hex HexMatrixMathlib + theorem matrixEquiv_apply (M : Hex.Matrix R n m) (i : Fin n) (j : Fin m) : matrixEquiv M i j = M[i][j] ``` @@ -80,14 +88,22 @@ theorem matrixEquiv_apply (M : Hex.Matrix R n m) (i : Fin n) (j : Fin m) : The elementary row operations correspond to Mathlib's elementary matrices. A swap is left multiplication by the permutation matrix `Matrix.swap`: -```lean nocheck +```lean recall +import HexMatrixMathlib + +open Hex HexMatrixMathlib + theorem matrixEquiv_rowSwap (M : Hex.Matrix R n m) (i j : Fin n) : matrixEquiv (Hex.Matrix.rowSwap M i j) = Matrix.swap R i j * matrixEquiv M ``` A row addition is left multiplication by `Matrix.transvection`: -```lean nocheck +```lean recall +import HexMatrixMathlib + +open Hex HexMatrixMathlib + theorem matrixEquiv_rowAdd (M : Hex.Matrix R n m) (src dst : Fin n) (c : R) : matrixEquiv (Hex.Matrix.rowAdd M src dst c) = Matrix.transvection dst src c * matrixEquiv M @@ -95,7 +111,11 @@ theorem matrixEquiv_rowAdd (M : Hex.Matrix R n m) (src dst : Fin n) (c : R) : The matrix-vector product transports to Mathlib's `Matrix.mulVec`: -```lean nocheck +```lean recall +import HexMatrixMathlib + +open Hex HexMatrixMathlib + theorem vectorEquiv_mulVec [Semiring R] (M : Hex.Matrix R n m) (v : Vector R m) : vectorEquiv (M * v) = (matrixEquiv M).mulVec (vectorEquiv v) ``` diff --git a/HexMvPoly/README.md b/HexMvPoly/README.md index 08f587292..3760085de 100644 --- a/HexMvPoly/README.md +++ b/HexMvPoly/README.md @@ -64,7 +64,11 @@ recursive-view laws. A product coefficient is the convolution over every monomial split: -```lean nocheck +```lean recall +import HexMvPoly + +open Hex Hex.MvPoly + theorem coeff_mul [Lean.Grind.Semiring R] [DecidableEq R] (m : Mono n) (p q : MvPoly n R cmp) : coeff m (p * q) = @@ -74,7 +78,11 @@ theorem coeff_mul [Lean.Grind.Semiring R] [DecidableEq R] Sparse Horner evaluation agrees with direct evaluation: -```lean nocheck +```lean recall +import HexMvPoly + +open Hex Hex.MvPoly + theorem evalHorner_eq [Lean.Grind.CommSemiring R] (x : Fin n → R) (p : MvPoly n R cmp) : evalHorner x p = eval x p diff --git a/HexMvPolyMathlib/README.md b/HexMvPolyMathlib/README.md index 574dfbfbd..87910f78f 100644 --- a/HexMvPolyMathlib/README.md +++ b/HexMvPolyMathlib/README.md @@ -57,14 +57,24 @@ example (p q : P) : The correspondence is fully proven in both directions: -```lean nocheck +```lean +import HexMvPolyMathlib + +open Hex Hex.MvPoly HexMvPolyMathlib +open scoped HexMvPolyMathlib + def equiv [CommSemiring R] [DecidableEq R] : MvPoly n R cmp ≃+* MvPolynomial (Fin n) R ``` It preserves every coefficient: -```lean nocheck +```lean recall +import HexMvPolyMathlib + +open Hex Hex.MvPoly HexMvPolyMathlib +open scoped HexMvPolyMathlib + theorem coeff_toMvPolynomial [CommSemiring R] [DecidableEq R] (m : Mono n) (p : MvPoly n R cmp) : MvPolynomial.coeff (monoEquiv m) (toMvPolynomial p) = @@ -73,7 +83,12 @@ theorem coeff_toMvPolynomial [CommSemiring R] [DecidableEq R] Executable evaluation is Mathlib algebra evaluation after conversion: -```lean nocheck +```lean recall +import HexMvPolyMathlib + +open Hex Hex.MvPoly HexMvPolyMathlib +open scoped HexMvPolyMathlib + theorem aeval_apply [CommSemiring R] [DecidableEq R] [CommSemiring S] [Algebra R S] (x : Fin n → S) (p : MvPoly n R cmp) : diff --git a/HexPolyFpMathlib/README.md b/HexPolyFpMathlib/README.md index 087e41db7..19acf84c9 100644 --- a/HexPolyFpMathlib/README.md +++ b/HexPolyFpMathlib/README.md @@ -48,7 +48,9 @@ polynomials and Mathlib's: The headline result is the ring equivalence: -```lean nocheck +```lean +import HexPolyFpMathlib + def fpPolyEquiv : Hex.FpPoly p ≃+* Polynomial (ZMod p) ``` diff --git a/HexRowReduce/README.md b/HexRowReduce/README.md index c2e1e0983..6e7c23cb2 100644 --- a/HexRowReduce/README.md +++ b/HexRowReduce/README.md @@ -58,13 +58,21 @@ Over a field the reduction is fully proven. The headline theorem states that sorted and equal to 1, all other pivot-column entries zero, trailing rows zero, and an invertible transform with `transform * M = echelon`): -```lean nocheck +```lean recall +import HexRowReduce + +open Hex + theorem rowReduce_isRowReduced (M : Matrix R n m) : IsRowReduced M (rowReduce M) ``` The row-span wrappers are sound, with `spanCoeffs_sound`: -```lean nocheck +```lean recall +import HexRowReduce + +open Hex + theorem spanCoeffs_sound [Lean.Grind.Field R] [DecidableEq R] (M : Matrix R n m) (v : Vector R m) (c : Vector R n) : spanCoeffs M v = some c → rowCombination M c = v @@ -73,7 +81,11 @@ theorem spanCoeffs_sound [Lean.Grind.Field R] [DecidableEq R] The nullspace basis is both sound and complete, `nullspace_sound` and `nullspace_complete`: -```lean nocheck +```lean recall +import HexRowReduce + +open Hex + theorem nullspace_sound [Lean.Grind.Field R] [DecidableEq R] (M : Matrix R n m) (k : Fin (m - rowReduce_rank M)) : M * (nullspace M).get k = 0 diff --git a/HexRowReduceMathlib/README.md b/HexRowReduceMathlib/README.md index 922959a22..de7d2dc18 100644 --- a/HexRowReduceMathlib/README.md +++ b/HexRowReduceMathlib/README.md @@ -64,7 +64,11 @@ row span, and nullspace are computable witnesses for Mathlib's noncomputable Rank, `rank_eq`: -```lean nocheck +```lean recall +import HexRowReduceMathlib + +open HexMatrixMathlib + theorem rank_eq [Field R] {M : Hex.Matrix R n m} {D : Hex.Matrix.RowEchelonData R n m} (E : Hex.Matrix.IsRowReduced M D) : @@ -73,7 +77,11 @@ theorem rank_eq [Field R] Nullspace, `nullspace_span_eq_ker`: -```lean nocheck +```lean recall +import HexRowReduceMathlib + +open HexMatrixMathlib + theorem nullspace_span_eq_ker [Field R] {M : Hex.Matrix R n m} {D : Hex.Matrix.RowEchelonData R n m} (E : Hex.Matrix.IsRowReduced M D) : @@ -83,7 +91,11 @@ theorem nullspace_span_eq_ker [Field R] Span, `spanContains_iff_mem_span`: -```lean nocheck +```lean recall +import HexRowReduceMathlib + +open HexMatrixMathlib + theorem spanContains_iff_mem_span [Field R] [DecidableEq R] {M : Hex.Matrix R n m} {D : Hex.Matrix.RowEchelonData R n m} (E : Hex.Matrix.IsRowReduced M D) (v : Vector R m) : diff --git a/SPEC/readme.md b/SPEC/readme.md index c0beb05b7..4b2556eee 100644 --- a/SPEC/readme.md +++ b/SPEC/readme.md @@ -45,9 +45,13 @@ Use these five level-1 headings, in this order. for executable use only. Where it helps the reader, quote the headline theorem for each significant result as a Lean signature (name plus statement, proof elided) in a `lean` code block, copied verbatim from - the source so it stays accurate. Mark these intentionally incomplete - signature blocks as `lean nocheck`; executable examples must remain checked. - Point at the sibling library where the rest of the theory lives. + the source so it stays accurate. Mark theorem blocks as `lean recall`: + `lean-readme` then checks each displayed `theorem` statement directly against + the declaration in the imported library, without changing the rendered + Markdown or depending on Mathlib's `recall` command. Other quoted declaration + kinds remain ordinary `lean` blocks. + Executable examples must remain checked. Point at the sibling library where + the rest of the theory lives. 5. **`# Contributing`**. State that development happens in the [`hex-dev`](https://github.com/kim-em/hex-dev) monorepo, not in the diff --git a/lake-manifest.json b/lake-manifest.json index 520c158ad..236b73514 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -21,14 +21,14 @@ "inputRev": "master", "inherited": false, "configFile": "lakefile.toml"}, - {"url": "https://github.com/david-christiansen/lean-readme.git", + {"url": "https://github.com/kim-em/lean-readme.git", "type": "git", "subDir": null, "scope": "", - "rev": "cccf47290b379d39972b659dd3ede88ebe3c1018", + "rev": "135c926eb9539434eef0a952faf91098d7bf2fec", "name": "«lean-readme»", "manifestFile": "lake-manifest.json", - "inputRev": "cccf47290b379d39972b659dd3ede88ebe3c1018", + "inputRev": "135c926eb9539434eef0a952faf91098d7bf2fec", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover/verso.git", diff --git a/lakefile.lean b/lakefile.lean index 3ab43562f..bf1232ccc 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -15,8 +15,8 @@ require verso from git "https://github.com/leanprover/verso.git" @ "v4.33.0-rc1" require «lean-readme» from git - "https://github.com/david-christiansen/lean-readme.git" @ - "cccf47290b379d39972b659dd3ede88ebe3c1018" + "https://github.com/kim-em/lean-readme.git" @ + "135c926eb9539434eef0a952faf91098d7bf2fec" require «lean-bench» from git "https://github.com/kim-em/lean-bench.git" @ "master" From 78ffdf67bc50258c10296c074acd9cbdd8f3eac8 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Sun, 23 Aug 2026 11:47:20 +0000 Subject: [PATCH 03/16] fix: hide setup in recalled theorem blocks --- .github/workflows/ci.yml | 6 ++--- .lean-readme/Aggregate.lean | 10 ++++++++ HexBareiss/README.md | 16 ++++--------- HexBareissMathlib/README.md | 12 ---------- HexBerlekampZassenhaus/README.md | 4 ++-- HexBerlekampZassenhausMathlib/README.md | 7 ++---- HexConway/README.md | 8 ------- HexDeterminant/README.md | 20 +++++----------- HexDeterminantMathlib/README.md | 12 ---------- HexGF2/README.md | 13 ++--------- HexGF2Mathlib/README.md | 18 +++----------- HexGFq/README.md | 2 +- HexGFqField/README.md | 5 +--- HexGFqMathlib/README.md | 13 ++++------- HexGramSchmidt/README.md | 8 ------- HexGramSchmidtMathlib/README.md | 16 ------------- HexMatrixMathlib/README.md | 22 ++++-------------- HexMvPoly/README.md | 15 ++++-------- HexMvPolyMathlib/README.md | 23 ++++++++---------- HexPolyFpMathlib/README.md | 3 ++- HexRowReduce/README.md | 31 +++++++++++-------------- HexRowReduceMathlib/README.md | 12 ---------- SPEC/readme.md | 7 +++++- lake-manifest.json | 4 ++-- lakefile.lean | 2 +- 25 files changed, 81 insertions(+), 208 deletions(-) create mode 100644 .lean-readme/Aggregate.lean diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 36892d6e5..b0b3dd8b3 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -196,11 +196,11 @@ jobs: run: lake build HexManual - name: Check README Lean snippets run: | - # lean-readme's initial release cannot process a second file after a - # file that imports modules, so use one process per README source. - for readme in Hex*/README.md scripts/release/hex-README.md; do + for readme in Hex*/README.md; do lake exe lean-readme "$readme" done + lake exe lean-readme --prefix .lean-readme/Aggregate.lean \ + scripts/release/hex-README.md # Publish hex-dev's oleans on a trusted main push so later builds (and any # consumer) restore them. Skips silently without the upload key. - name: Publish hex-dev oleans to the Lake cache (main only) diff --git a/.lean-readme/Aggregate.lean b/.lean-readme/Aggregate.lean new file mode 100644 index 000000000..b5bf9b7ce --- /dev/null +++ b/.lean-readme/Aggregate.lean @@ -0,0 +1,10 @@ +/- +Copyright (c) 2026 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kim Morrison +-/ + +module + +import HexLLL + diff --git a/HexBareiss/README.md b/HexBareiss/README.md index 144850727..25127aa3c 100644 --- a/HexBareiss/README.md +++ b/HexBareiss/README.md @@ -30,12 +30,12 @@ open Hex -- A 3×3 integer matrix with a zero leading pivot, forcing a row swap. def M : Matrix Int 3 3 := Matrix.ofFn fun i j => (i + 2 * j : Int) -#eval Matrix.bareiss M -- fraction-free determinant -#eval Matrix.bareiss (Matrix.identity (R := Int) 4) -- 1 +#check Matrix.bareiss M +#check Matrix.bareiss (Matrix.identity (R := Int) 4) -- bareissData also records the row-swap count alongside the determinant. -#eval (Matrix.bareissData M).det -#eval (Matrix.bareissData M).rowSwaps +#check (Matrix.bareissData M).det +#check (Matrix.bareissData M).rowSwaps ``` # Functionality @@ -63,10 +63,6 @@ determinant encoded by `bareissData`. The public determinant agrees with the encoded data, `bareiss_eq_bareissData_det`: ```lean recall -import HexBareiss - -open Hex - theorem bareiss_eq_bareissData_det (M : Matrix Int n n) : bareiss M = (bareissData M).det ``` @@ -75,10 +71,6 @@ The no-pivot run, when it reaches the final pivot without a singular step, reads off the last diagonal entry, `bareiss_eq_noPivotLoop_last_of_no_singular`: ```lean recall -import HexBareiss - -open Hex - theorem bareiss_eq_noPivotLoop_last_of_no_singular {k : Nat} (M : Matrix Int (k + 1) (k + 1)) (h_no_sing : diff --git a/HexBareissMathlib/README.md b/HexBareissMathlib/README.md index ba32754f0..9be6cda59 100644 --- a/HexBareissMathlib/README.md +++ b/HexBareissMathlib/README.md @@ -58,10 +58,6 @@ The executable Bareiss determinant equals the Leibniz determinant, `bareiss_eq_det`: ```lean recall -import HexBareissMathlib - -open HexMatrixMathlib - theorem bareiss_eq_det (M : Hex.Matrix Int n n) : Hex.Matrix.bareiss M = Hex.Matrix.det M ``` @@ -69,10 +65,6 @@ theorem bareiss_eq_det (M : Hex.Matrix Int n n) : It also equals Mathlib's determinant, `bareissDet_eq_det`: ```lean recall -import HexBareissMathlib - -open HexMatrixMathlib - theorem bareissDet_eq_det (M : Hex.Matrix Int n n) : Hex.Matrix.bareiss M = Matrix.det (matrixEquiv M) ``` @@ -81,10 +73,6 @@ The Mathlib statement is proven directly by running the Bareiss loop and tracking the bordered-minor invariant step by step, `bareiss_eq_mathlib_det`: ```lean recall -import HexBareissMathlib - -open HexMatrixMathlib - theorem bareiss_eq_mathlib_det (M : Hex.Matrix Int n n) : Hex.Matrix.bareiss M = Matrix.det (matrixEquiv M) ``` diff --git a/HexBerlekampZassenhaus/README.md b/HexBerlekampZassenhaus/README.md index c0fbfdcac..e0b1941ca 100644 --- a/HexBerlekampZassenhaus/README.md +++ b/HexBerlekampZassenhaus/README.md @@ -51,8 +51,8 @@ open Hex def f : ZPoly := DensePoly.ofCoeffs #[1, 0, 1] -noncomputable def fFactored := factor_poly f -theorem fIrreducible : ZPoly.Irreducible f := irreducibility f +#check factor_poly +#check irreducibility ``` Import `HexBerlekampZassenhaus.All` only when developing the algorithms and diff --git a/HexBerlekampZassenhausMathlib/README.md b/HexBerlekampZassenhausMathlib/README.md index 4efa225ab..20186dc34 100644 --- a/HexBerlekampZassenhausMathlib/README.md +++ b/HexBerlekampZassenhausMathlib/README.md @@ -45,11 +45,8 @@ import HexBerlekampZassenhausMathlib open Polynomial -noncomputable def fac := - factor_poly ((X - 1) ^ 2 * (X ^ 2 + 1) : Polynomial ℤ) - -example : Irreducible (X ^ 4 + 8 * X + 12 : Polynomial ℤ) := by - irreducibility +#check factor_poly +#check irreducibility ``` Import `HexBerlekampZassenhausMathlib.All` only when developing the detailed diff --git a/HexConway/README.md b/HexConway/README.md index 860144d82..aa25909a3 100644 --- a/HexConway/README.md +++ b/HexConway/README.md @@ -76,10 +76,6 @@ dispatch theorem is `luebeckConwayPolynomial?_irreducible`, and the API-facing form is ```lean recall -import HexConway - -open Hex Hex.Conway - theorem conwayPoly_irreducible (p n : Nat) [ZMod64.Bounds p] (h : SupportedEntry p n) : FpPoly.Irreducible (conwayPoly p n h) @@ -92,10 +88,6 @@ promoted to a statement about field elements, which is the well-definedness input a subfield embedding needs: ```lean recall -import HexConway - -open Hex Hex.Conway - theorem eval_conwayPoly_subfieldGen_eq_zero {p m n : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (hm : SupportedEntry p m) (hn : SupportedEntry p n) diff --git a/HexDeterminant/README.md b/HexDeterminant/README.md index 57fbccc70..2752d7032 100644 --- a/HexDeterminant/README.md +++ b/HexDeterminant/README.md @@ -60,11 +60,8 @@ The headline theorem for each of the remaining results (with Column linearity, `det_setCol_add`: ```lean recall -import HexDeterminant - -open Hex - -theorem det_setCol_add (M : Matrix R n n) (dst : Fin n) (v w : Fin n → R) : +theorem det_setCol_add {R : Type u} [Lean.Grind.CommRing R] {n : Nat} + (M : Matrix R n n) (dst : Fin n) (v w : Fin n → R) : det (setCol M dst (fun r => v r + w r)) = det (setCol M dst v) + det (setCol M dst w) ``` @@ -72,11 +69,9 @@ theorem det_setCol_add (M : Matrix R n n) (dst : Fin n) (v w : Fin n → R) : Laplace cofactor expansion along a row, `det_eq_finFoldl_laplace_row`: ```lean recall -import HexDeterminant - -open Hex - -theorem det_eq_finFoldl_laplace_row (M : Matrix R (n + 1) (n + 1)) (row : Fin (n + 1)) : +theorem det_eq_finFoldl_laplace_row + {R : Type u} [Lean.Grind.CommRing R] {n : Nat} + (M : Matrix R (n + 1) (n + 1)) (row : Fin (n + 1)) : det M = Fin.foldl (n + 1) (fun acc col => acc + M[row][col] * cofactor M row col) 0 @@ -95,11 +90,8 @@ identity, the `2 × 2` case of Jacobi's adjugate-minor identity: for distinct rows `a`, `b` and arbitrary vectors `u`, `v`, ```lean recall -import HexDeterminant - -open Hex - theorem det_setRow_setRow_mul_det + {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Matrix R (n + 1) (n + 1)) (a b : Fin (n + 1)) (hab : a ≠ b) (u v : Vector R (n + 1)) : det M * det (setRow (setRow M a u) b v) = diff --git a/HexDeterminantMathlib/README.md b/HexDeterminantMathlib/README.md index baa0bea1f..916c24f5a 100644 --- a/HexDeterminantMathlib/README.md +++ b/HexDeterminantMathlib/README.md @@ -68,10 +68,6 @@ The determinant correspondence is fully proven over a `CommRing`. The headline theorem identifies the two determinants: ```lean recall -import HexDeterminantMathlib - -open Hex HexMatrixMathlib - theorem det_eq [CommRing R] (M : Hex.Matrix R n n) : Hex.Matrix.det M = Matrix.det (matrixEquiv M) ``` @@ -81,10 +77,6 @@ rows `p1 < p2 < p3` (`hex-determinant` proves the Mathlib-free specialisation where `p2` and `p3` are the last two rows): ```lean recall -import HexDeterminantMathlib - -open Hex HexMatrixMathlib - theorem det_plucker_three_term {R : Type u} [CommRing R] {n : Nat} (B : Hex.Matrix R (n + 3) (n + 1)) (v : Vector R (n + 3)) @@ -98,10 +90,6 @@ theorem det_plucker_three_term The Desnanot-Jacobi identity over Mathlib matrices: ```lean recall -import HexDeterminantMathlib - -open Hex HexMatrixMathlib - theorem desnanot_jacobi {R : Type*} [CommRing R] {n : ℕ} (M : Matrix (Fin (n + 2)) (Fin (n + 2)) R) : M.det * (M.submatrix (Fin.succAbove 0 ∘ (Fin.last n).succAbove) diff --git a/HexGF2/README.md b/HexGF2/README.md index 89a92ee06..ed65abfca 100644 --- a/HexGF2/README.md +++ b/HexGF2/README.md @@ -70,10 +70,6 @@ is certificate replay, which is what lets a committed modulus be checked by the kernel without `native_decide`: ```lean recall -import HexGF2 - -open Hex - theorem rabinTest_imp_irreducible (f : GF2Poly) (hrabin : rabinTest f = true) : GF2Poly.Irreducible f @@ -90,13 +86,8 @@ quotient by a constant is trivial, so nonconstancy is a separate hypothesis and the field laws are functions rather than instances. ```lean recall -import HexGF2 - -open Hex - -def fieldOfDegreePos (hdeg : 0 < f.degree) : Lean.Grind.Field (GF2nPoly f hirr) - -theorem isCharPOfDegreePos (hdeg : 0 < f.degree) : +theorem isCharPOfDegreePos {f : GF2Poly} {hirr : GF2Poly.Irreducible f} + (hdeg : 0 < f.degree) : Lean.Grind.IsCharP (GF2nPoly f hirr) 2 ``` diff --git a/HexGF2Mathlib/README.md b/HexGF2Mathlib/README.md index fab8365dd..1ca1d4c3c 100644 --- a/HexGF2Mathlib/README.md +++ b/HexGF2Mathlib/README.md @@ -83,27 +83,15 @@ keep the executable operations rather than transported copies, so The single-word wrapper, in namespace `HexGF2Mathlib.GF2n`: ```lean recall -import HexGF2Mathlib - -open Hex - -def equiv : Hex.GF2n n irr hn hn64 hirr ≃+* - GenericFiniteField (n := n) (irr := irr) (hn := hn) (hn64 := hn64) (hirr := hirr) - -theorem fintype_card : +theorem fintype_card {n : Nat} {irr : UInt64} {hn : 0 < n} {hn64 : n < 64} + {hirr : Hex.GF2Poly.Irreducible (Hex.GF2Poly.ofUInt64Monic irr n)} : Fintype.card (Hex.GF2n n irr hn hn64 hirr) = 2 ^ n ``` The arbitrary-degree wrapper, in namespace `HexGF2Mathlib.GF2nPoly`: ```lean recall -import HexGF2Mathlib - -open Hex - -def equiv : Hex.GF2nPoly f hirr ≃+* GenericFiniteField (f := f) (hirr := hirr) (hdeg := hdeg) - -theorem fintype_card : +theorem fintype_card {f : Hex.GF2Poly} {hirr : Hex.GF2Poly.Irreducible f} : Fintype.card (Hex.GF2nPoly f hirr) = 2 ^ f.degree ``` diff --git a/HexGFq/README.md b/HexGFq/README.md index 31a192ee8..790de68ec 100644 --- a/HexGFq/README.md +++ b/HexGFq/README.md @@ -98,7 +98,7 @@ packed word denotes the same polynomial as the committed Conway entry: ```lean import HexGFq -open Hex +open Hex Hex.GFq Hex.Conway class PackedGF2Entry (n : Nat) where entry : SupportedEntry 2 n diff --git a/HexGFqField/README.md b/HexGFqField/README.md index d2814f2d0..82984ad87 100644 --- a/HexGFqField/README.md +++ b/HexGFqField/README.md @@ -72,11 +72,8 @@ The field laws are proved, not asserted. Inverse cancellation is the result the rest rests on: ```lean recall -import HexGFqField - -open Hex Hex.GFqField - theorem mul_inv_cancel + {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {hp : Hex.Nat.Prime p} {f : FpPoly p} {hf : 0 < FpPoly.degree f} {hirr : FpPoly.Irreducible f} {x : FiniteField f hf hp hirr} (hx : x ≠ 0) : x * x⁻¹ = 1 diff --git a/HexGFqMathlib/README.md b/HexGFqMathlib/README.md index 1facc21ea..584606c57 100644 --- a/HexGFqMathlib/README.md +++ b/HexGFqMathlib/README.md @@ -70,14 +70,8 @@ The executable field carries Mathlib's `Field` structure, and the carrier is finite with the cardinality its construction promises: ```lean recall -import HexGFqMathlib - -open Hex - -noncomputable instance field : - Field (Hex.GFqField.FiniteField f hf hp hirr) - -theorem fintype_card_eq_pow (h : Hex.Conway.SupportedEntry p n) : +theorem fintype_card_eq_pow {p n : Nat} [Hex.ZMod64.Bounds p] + (h : Hex.Conway.SupportedEntry p n) : Fintype.card (Hex.GFq p n h) = p ^ n ``` @@ -95,7 +89,8 @@ import HexGFqMathlib open Hex -noncomputable def equivGaloisField [Fact p.Prime] +noncomputable def equivGaloisField {p n : Nat} [Hex.ZMod64.Bounds p] + [Hex.ZMod64.PrimeModulus p] [Fact p.Prime] (h : Hex.Conway.SupportedEntry p n) (hn : n ≠ 0) : _root_.RingEquiv (Hex.GFq p n h) (GaloisField p n) ``` diff --git a/HexGramSchmidt/README.md b/HexGramSchmidt/README.md index 5a8e320be..cdf8444da 100644 --- a/HexGramSchmidt/README.md +++ b/HexGramSchmidt/README.md @@ -72,10 +72,6 @@ The orthogonalization theory is proven over the Mathlib-free integer and rational cores. The orthogonal basis, `basis_orthogonal`: ```lean recall -import HexGramSchmidt - -open Hex - theorem basis_orthogonal (b : Matrix Int n m) (i j : Nat) (hi : i < n) (hj : j < n) (hij : i ≠ j) : ((basis b).row ⟨i, hi⟩).dotProduct ((basis b).row ⟨j, hj⟩) = 0 @@ -87,10 +83,6 @@ coefficient laws `coeffs_diag` and `coeffs_upper`, the span equality key lattice estimate, `normSq_latticeVec_ge_min_basis_normSq`: ```lean recall -import HexGramSchmidt - -open Hex - theorem normSq_latticeVec_ge_min_basis_normSq (b : Matrix Int n m) (_hli : independent b) (v : Vector Int m) (hv : memLattice b v) (hv' : v ≠ 0) : diff --git a/HexGramSchmidtMathlib/README.md b/HexGramSchmidtMathlib/README.md index 51b571e9a..95f9dae9a 100644 --- a/HexGramSchmidtMathlib/README.md +++ b/HexGramSchmidtMathlib/README.md @@ -62,10 +62,6 @@ The rowwise correspondence with Mathlib's orthogonalization is fully proven. Over the rationals: ```lean recall -import HexGramSchmidtMathlib - -open Hex - theorem rat_basis_row_eq_gramSchmidt (b : Matrix Rat n m) (i : Fin n) : rowToEuclidean ((Hex.GramSchmidt.Rat.basis b).row i) = InnerProductSpace.gramSchmidt ℝ (ratRowFamily b) i @@ -74,10 +70,6 @@ theorem rat_basis_row_eq_gramSchmidt (b : Matrix Rat n m) (i : Fin n) : and the integer version, casting the integer rows first: ```lean recall -import HexGramSchmidtMathlib - -open Hex - theorem int_basis_row_eq_gramSchmidt (b : Matrix Int n m) (i : Fin n) : rowToEuclidean ((Hex.GramSchmidt.Int.basis b).row i) = InnerProductSpace.gramSchmidt ℝ (intRowFamily b) i @@ -87,10 +79,6 @@ The fraction-free integer surface is identified with Bareiss determinants. Below the diagonal the scaled coefficients are exactly: ```lean recall -import HexGramSchmidtMathlib - -open Hex - theorem scaledCoeffs_eq_scaledCoeffMatrix_bareiss (b : Matrix Int n m) (i j : Fin n) (hji : j.val < i.val) : GramSchmidt.entry (scaledCoeffs b) i j = @@ -101,10 +89,6 @@ and for an independent matrix the leading Gram determinant is the product of squared Gram-Schmidt norms: ```lean recall -import HexGramSchmidtMathlib - -open Hex - theorem gramDet_eq_prod_normSq (b : Matrix Int n m) (hli : independent b) (k : Nat) (hk : k ≤ n) : (gramDet b k hk : Rat) = gramSchmidtNormProduct b k hk diff --git a/HexMatrixMathlib/README.md b/HexMatrixMathlib/README.md index f0a67b1de..54610bf2c 100644 --- a/HexMatrixMathlib/README.md +++ b/HexMatrixMathlib/README.md @@ -77,10 +77,6 @@ def matrixEquiv : Hex.Matrix R n m ≃ Matrix (Fin n) (Fin m) R ``` ```lean recall -import HexMatrixMathlib - -open Hex HexMatrixMathlib - theorem matrixEquiv_apply (M : Hex.Matrix R n m) (i : Fin n) (j : Fin m) : matrixEquiv M i j = M[i][j] ``` @@ -89,22 +85,16 @@ The elementary row operations correspond to Mathlib's elementary matrices. A swap is left multiplication by the permutation matrix `Matrix.swap`: ```lean recall -import HexMatrixMathlib - -open Hex HexMatrixMathlib - -theorem matrixEquiv_rowSwap (M : Hex.Matrix R n m) (i j : Fin n) : +theorem matrixEquiv_rowSwap {R : Type u} [Semiring R] {n m : Nat} + (M : Hex.Matrix R n m) (i j : Fin n) : matrixEquiv (Hex.Matrix.rowSwap M i j) = Matrix.swap R i j * matrixEquiv M ``` A row addition is left multiplication by `Matrix.transvection`: ```lean recall -import HexMatrixMathlib - -open Hex HexMatrixMathlib - -theorem matrixEquiv_rowAdd (M : Hex.Matrix R n m) (src dst : Fin n) (c : R) : +theorem matrixEquiv_rowAdd {R : Type u} [CommRing R] {n m : Nat} + (M : Hex.Matrix R n m) (src dst : Fin n) (c : R) : matrixEquiv (Hex.Matrix.rowAdd M src dst c) = Matrix.transvection dst src c * matrixEquiv M ``` @@ -112,10 +102,6 @@ theorem matrixEquiv_rowAdd (M : Hex.Matrix R n m) (src dst : Fin n) (c : R) : The matrix-vector product transports to Mathlib's `Matrix.mulVec`: ```lean recall -import HexMatrixMathlib - -open Hex HexMatrixMathlib - theorem vectorEquiv_mulVec [Semiring R] (M : Hex.Matrix R n m) (v : Vector R m) : vectorEquiv (M * v) = (matrixEquiv M).mulVec (vectorEquiv v) ``` diff --git a/HexMvPoly/README.md b/HexMvPoly/README.md index 3760085de..2c1a9e246 100644 --- a/HexMvPoly/README.md +++ b/HexMvPoly/README.md @@ -65,11 +65,9 @@ recursive-view laws. A product coefficient is the convolution over every monomial split: ```lean recall -import HexMvPoly - -open Hex Hex.MvPoly - -theorem coeff_mul [Lean.Grind.Semiring R] [DecidableEq R] +theorem coeff_mul {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} + [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] + [Lean.Grind.Semiring R] [DecidableEq R] (m : Mono n) (p q : MvPoly n R cmp) : coeff m (p * q) = (Mono.splits m).foldl @@ -79,11 +77,8 @@ theorem coeff_mul [Lean.Grind.Semiring R] [DecidableEq R] Sparse Horner evaluation agrees with direct evaluation: ```lean recall -import HexMvPoly - -open Hex Hex.MvPoly - -theorem evalHorner_eq [Lean.Grind.CommSemiring R] +theorem evalHorner_eq {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} + [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Lean.Grind.CommSemiring R] (x : Fin n → R) (p : MvPoly n R cmp) : evalHorner x p = eval x p ``` diff --git a/HexMvPolyMathlib/README.md b/HexMvPolyMathlib/README.md index 87910f78f..9b4d04a90 100644 --- a/HexMvPolyMathlib/README.md +++ b/HexMvPolyMathlib/README.md @@ -63,19 +63,18 @@ import HexMvPolyMathlib open Hex Hex.MvPoly HexMvPolyMathlib open scoped HexMvPolyMathlib -def equiv [CommSemiring R] [DecidableEq R] : +def equiv {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} + [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] + [CommSemiring R] [DecidableEq R] : MvPoly n R cmp ≃+* MvPolynomial (Fin n) R ``` It preserves every coefficient: ```lean recall -import HexMvPolyMathlib - -open Hex Hex.MvPoly HexMvPolyMathlib -open scoped HexMvPolyMathlib - -theorem coeff_toMvPolynomial [CommSemiring R] [DecidableEq R] +theorem coeff_toMvPolynomial + {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} + [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [CommSemiring R] [DecidableEq R] (m : Mono n) (p : MvPoly n R cmp) : MvPolynomial.coeff (monoEquiv m) (toMvPolynomial p) = coeff m p @@ -84,12 +83,10 @@ theorem coeff_toMvPolynomial [CommSemiring R] [DecidableEq R] Executable evaluation is Mathlib algebra evaluation after conversion: ```lean recall -import HexMvPolyMathlib - -open Hex Hex.MvPoly HexMvPolyMathlib -open scoped HexMvPolyMathlib - -theorem aeval_apply [CommSemiring R] [DecidableEq R] +theorem aeval_apply + {n : Nat} {R : Type u} {S : Type v} {cmp : Mono n → Mono n → Ordering} + [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] + [CommSemiring R] [DecidableEq R] [CommSemiring S] [Algebra R S] (x : Fin n → S) (p : MvPoly n R cmp) : aeval x p = MvPolynomial.aeval x (toMvPolynomial p) diff --git a/HexPolyFpMathlib/README.md b/HexPolyFpMathlib/README.md index 19acf84c9..1a648d1f1 100644 --- a/HexPolyFpMathlib/README.md +++ b/HexPolyFpMathlib/README.md @@ -51,7 +51,8 @@ The headline result is the ring equivalence: ```lean import HexPolyFpMathlib -def fpPolyEquiv : Hex.FpPoly p ≃+* Polynomial (ZMod p) +def fpPolyEquiv {p : Nat} [Hex.ZMod64.Bounds p] : + Hex.FpPoly p ≃+* Polynomial (ZMod p) ``` The equivalence and transport lemmas are stated under the executable bounds diff --git a/HexRowReduce/README.md b/HexRowReduce/README.md index 6e7c23cb2..fa46e44b7 100644 --- a/HexRowReduce/README.md +++ b/HexRowReduce/README.md @@ -47,7 +47,7 @@ def M : Matrix Rat 2 3 := Matrix.ofFn fun i j => (i + 1) * (j + 1 : Rat) - `rowReduce_rank`: the rank read off the reduction; - `spanCoeffs` and `spanContains`: solve for row-combination coefficients of a vector, or test row-span membership; -- `rowCombination`: the linear combination of the rows of a matrix; +- `vecMul`: the linear combination of the rows of a matrix; - `nullspace` and `nullspaceBasisMatrix`: a basis for the nullspace, one vector per free column, as a vector of vectors or as a matrix of columns. @@ -59,38 +59,33 @@ sorted and equal to 1, all other pivot-column entries zero, trailing rows zero, and an invertible transform with `transform * M = echelon`): ```lean recall -import HexRowReduce - -open Hex - -theorem rowReduce_isRowReduced (M : Matrix R n m) : IsRowReduced M (rowReduce M) +theorem rowReduce_isRowReduced + {R : Type u} {n m : Nat} [Lean.Grind.Field R] [DecidableEq R] + (M : Matrix R n m) : IsRowReduced M (rowReduce M) ``` The row-span wrappers are sound, with `spanCoeffs_sound`: ```lean recall -import HexRowReduce - -open Hex - -theorem spanCoeffs_sound [Lean.Grind.Field R] [DecidableEq R] +theorem spanCoeffs_sound + {R : Type u} {n m : Nat} [Lean.Grind.Field R] [DecidableEq R] (M : Matrix R n m) (v : Vector R m) (c : Vector R n) : - spanCoeffs M v = some c → rowCombination M c = v + spanCoeffs M v = some c → vecMul c M = v ``` The nullspace basis is both sound and complete, `nullspace_sound` and `nullspace_complete`: ```lean recall -import HexRowReduce - -open Hex - -theorem nullspace_sound [Lean.Grind.Field R] [DecidableEq R] (M : Matrix R n m) +theorem nullspace_sound + {R : Type u} {n m : Nat} [Lean.Grind.Field R] [DecidableEq R] + (M : Matrix R n m) (k : Fin (m - rowReduce_rank M)) : M * (nullspace M).get k = 0 -theorem nullspace_complete [Lean.Grind.Field R] [DecidableEq R] (M : Matrix R n m) +theorem nullspace_complete + {R : Type u} {n m : Nat} [Lean.Grind.Field R] [DecidableEq R] + (M : Matrix R n m) (v : Vector R m) : M * v = 0 → ∃ c : Vector R (m - rowReduce_rank M), nullspaceBasisMatrix M * c = v ``` diff --git a/HexRowReduceMathlib/README.md b/HexRowReduceMathlib/README.md index de7d2dc18..fd19998d1 100644 --- a/HexRowReduceMathlib/README.md +++ b/HexRowReduceMathlib/README.md @@ -65,10 +65,6 @@ row span, and nullspace are computable witnesses for Mathlib's noncomputable Rank, `rank_eq`: ```lean recall -import HexRowReduceMathlib - -open HexMatrixMathlib - theorem rank_eq [Field R] {M : Hex.Matrix R n m} {D : Hex.Matrix.RowEchelonData R n m} (E : Hex.Matrix.IsRowReduced M D) : @@ -78,10 +74,6 @@ theorem rank_eq [Field R] Nullspace, `nullspace_span_eq_ker`: ```lean recall -import HexRowReduceMathlib - -open HexMatrixMathlib - theorem nullspace_span_eq_ker [Field R] {M : Hex.Matrix R n m} {D : Hex.Matrix.RowEchelonData R n m} (E : Hex.Matrix.IsRowReduced M D) : @@ -92,10 +84,6 @@ theorem nullspace_span_eq_ker [Field R] Span, `spanContains_iff_mem_span`: ```lean recall -import HexRowReduceMathlib - -open HexMatrixMathlib - theorem spanContains_iff_mem_span [Field R] [DecidableEq R] {M : Hex.Matrix R n m} {D : Hex.Matrix.RowEchelonData R n m} (E : Hex.Matrix.IsRowReduced M D) (v : Vector R m) : diff --git a/SPEC/readme.md b/SPEC/readme.md index 4b2556eee..37dd09927 100644 --- a/SPEC/readme.md +++ b/SPEC/readme.md @@ -49,7 +49,9 @@ Use these five level-1 headings, in this order. `lean-readme` then checks each displayed `theorem` statement directly against the declaration in the imported library, without changing the rendered Markdown or depending on Mathlib's `recall` command. Other quoted declaration - kinds remain ordinary `lean` blocks. + kinds remain ordinary `lean` blocks. Because blocks are checked in order, + `lean recall` blocks reuse the Quickstart block's imports and namespace + openings rather than repeating them in the rendered theorem quotation. Executable examples must remain checked. Point at the sibling library where the rest of the theory lives. @@ -65,6 +67,9 @@ Use these five level-1 headings, in this order. `/README.md` to come from. It is generated instead: the prose lives in `scripts/release/hex-README.md` and the library table is rendered from `released.yml` by `scripts/release/aggregate_readme.py` during the sync. +The monorepo's own `Hex` module is test infrastructure rather than the released +aggregate, so CI checks this template with `.lean-readme/Aggregate.lean` as a +hidden prefix supplying the released APIs used by its example. Releasing a library therefore adds it to the aggregate README with no hand edit, provided its manifest entry carries a `component:` label naming the row diff --git a/lake-manifest.json b/lake-manifest.json index 236b73514..20f337787 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -25,10 +25,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "135c926eb9539434eef0a952faf91098d7bf2fec", + "rev": "4ef92a1dcaedc189ab41b59ba04fe40ac6afd4b9", "name": "«lean-readme»", "manifestFile": "lake-manifest.json", - "inputRev": "135c926eb9539434eef0a952faf91098d7bf2fec", + "inputRev": "4ef92a1dcaedc189ab41b59ba04fe40ac6afd4b9", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover/verso.git", diff --git a/lakefile.lean b/lakefile.lean index bf1232ccc..b00574f4e 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -16,7 +16,7 @@ require verso from git require «lean-readme» from git "https://github.com/kim-em/lean-readme.git" @ - "135c926eb9539434eef0a952faf91098d7bf2fec" + "4ef92a1dcaedc189ab41b59ba04fe40ac6afd4b9" require «lean-bench» from git "https://github.com/kim-em/lean-bench.git" @ "master" From be5a783115655058584c51e90b10babf66d3b6c3 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Sun, 23 Aug 2026 11:57:37 +0000 Subject: [PATCH 04/16] fix: preserve executable README examples --- .github/workflows/ci.yml | 9 ++++++++- .lean-readme/Native.lean | 25 +++++++++++++++++++++++++ HexBareiss/README.md | 8 ++++---- HexBerlekampZassenhaus/README.md | 4 ++-- HexBerlekampZassenhausMathlib/README.md | 7 +++++-- SPEC/readme.md | 5 +++++ 6 files changed, 49 insertions(+), 9 deletions(-) create mode 100644 .lean-readme/Native.lean diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index b0b3dd8b3..8525ff71a 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -197,7 +197,14 @@ jobs: - name: Check README Lean snippets run: | for readme in Hex*/README.md; do - lake exe lean-readme "$readme" + case "$readme" in + HexBareiss/README.md|HexBerlekampZassenhaus/README.md|HexBerlekampZassenhausMathlib/README.md) + lake exe lean-readme --prefix .lean-readme/Native.lean "$readme" + ;; + *) + lake exe lean-readme "$readme" + ;; + esac done lake exe lean-readme --prefix .lean-readme/Aggregate.lean \ scripts/release/hex-README.md diff --git a/.lean-readme/Native.lean b/.lean-readme/Native.lean new file mode 100644 index 000000000..c4463214b --- /dev/null +++ b/.lean-readme/Native.lean @@ -0,0 +1,25 @@ +/- +Copyright (c) 2026 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kim Morrison +-/ + +module + +import Lean +public meta import HexBareiss + +public section + +private def loadReadmeDynlib (dir stem : String) : IO Unit := do + let ext := if System.Platform.isOSX then "dylib" else "so" + Lean.loadDynlib s!".lake/build/lib/{dir}{stem}.{ext}" + +run_cmd loadReadmeDynlib "" "libhexarithffi" +run_cmd loadReadmeDynlib "" "libHex_HexArith" +run_cmd loadReadmeDynlib "" "libhexmodarithffi" +run_cmd loadReadmeDynlib "" "libHex_HexModArith" +run_cmd loadReadmeDynlib "lean/" "Hex_HexHensel_WordMul" +run_cmd loadReadmeDynlib "" "libHex_HexBasic" +run_cmd loadReadmeDynlib "" "libHex_HexMatrix" +run_cmd loadReadmeDynlib "" "libHex_HexBareiss" diff --git a/HexBareiss/README.md b/HexBareiss/README.md index 25127aa3c..77e9ada2f 100644 --- a/HexBareiss/README.md +++ b/HexBareiss/README.md @@ -30,12 +30,12 @@ open Hex -- A 3×3 integer matrix with a zero leading pivot, forcing a row swap. def M : Matrix Int 3 3 := Matrix.ofFn fun i j => (i + 2 * j : Int) -#check Matrix.bareiss M -#check Matrix.bareiss (Matrix.identity (R := Int) 4) +#eval Matrix.bareiss M -- fraction-free determinant +#eval Matrix.bareiss (Matrix.identity (R := Int) 4) -- 1 -- bareissData also records the row-swap count alongside the determinant. -#check (Matrix.bareissData M).det -#check (Matrix.bareissData M).rowSwaps +#eval (Matrix.bareissData M).det +#eval (Matrix.bareissData M).rowSwaps ``` # Functionality diff --git a/HexBerlekampZassenhaus/README.md b/HexBerlekampZassenhaus/README.md index e0b1941ca..c0fbfdcac 100644 --- a/HexBerlekampZassenhaus/README.md +++ b/HexBerlekampZassenhaus/README.md @@ -51,8 +51,8 @@ open Hex def f : ZPoly := DensePoly.ofCoeffs #[1, 0, 1] -#check factor_poly -#check irreducibility +noncomputable def fFactored := factor_poly f +theorem fIrreducible : ZPoly.Irreducible f := irreducibility f ``` Import `HexBerlekampZassenhaus.All` only when developing the algorithms and diff --git a/HexBerlekampZassenhausMathlib/README.md b/HexBerlekampZassenhausMathlib/README.md index 20186dc34..4efa225ab 100644 --- a/HexBerlekampZassenhausMathlib/README.md +++ b/HexBerlekampZassenhausMathlib/README.md @@ -45,8 +45,11 @@ import HexBerlekampZassenhausMathlib open Polynomial -#check factor_poly -#check irreducibility +noncomputable def fac := + factor_poly ((X - 1) ^ 2 * (X ^ 2 + 1) : Polynomial ℤ) + +example : Irreducible (X ^ 4 + 8 * X + 12 : Polynomial ℤ) := by + irreducibility ``` Import `HexBerlekampZassenhausMathlib.All` only when developing the detailed diff --git a/SPEC/readme.md b/SPEC/readme.md index 37dd09927..2a1deae3d 100644 --- a/SPEC/readme.md +++ b/SPEC/readme.md @@ -55,6 +55,11 @@ Use these five level-1 headings, in this order. Executable examples must remain checked. Point at the sibling library where the rest of the theory lives. +Examples whose elaboration or evaluation uses a native implementation are +checked with `.lean-readme/Native.lean`. This hidden prefix loads the same +precompiled libraries that Lean loads when compiling an ordinary source file; +do not weaken such examples to API-name-only `#check` blocks. + 5. **`# Contributing`**. State that development happens in the [`hex-dev`](https://github.com/kim-em/hex-dev) monorepo, not in the published mirror, and that contributions are welcome as pull requests to From 63acff3f252056efa617daca6f64a7dc74f451dc Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Sun, 23 Aug 2026 11:58:57 +0000 Subject: [PATCH 05/16] ci: exempt README tooling from benchmark freshness --- scripts/bench/proof_only_runtime_exemptions.json | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/scripts/bench/proof_only_runtime_exemptions.json b/scripts/bench/proof_only_runtime_exemptions.json index c32ddc139..88c8b7302 100644 --- a/scripts/bench/proof_only_runtime_exemptions.json +++ b/scripts/bench/proof_only_runtime_exemptions.json @@ -766,5 +766,17 @@ "baseline_blob": "1063ee045056aabe060a319d7dbe48460e6fdd75", "current_blob": "635c202971d2276a498505da9842deac1c833c9f", "reason": "Updates diagnostic-service projections from the duplicate small-prime record to the representation-identical bundled ZMod64.Prime record; every measured operation and branch is unchanged." + }, + { + "path": "lakefile.lean", + "baseline_blob": "ff87edbbbf7524190b536ae4ce92a57968275aa9", + "current_blob": "b00574f4e87aeacd2b07598d3e8c6bd4b9a8dc82", + "reason": "Adds and pins the lean-readme documentation checker only; the factorization service target and its executable dependency graph are unchanged." + }, + { + "path": "lake-manifest.json", + "baseline_blob": "5f5b01e430fb8241d938d392298d786b38f67104", + "current_blob": "20f3377876c8d17e4c711d0e7edc452011913b28", + "reason": "Updates only the pinned lean-readme documentation checker revision; every factorization dependency remains unchanged." } ] From ca37040a8a7292710f55d9cce3718f961b434802 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 24 Aug 2026 03:29:38 +0000 Subject: [PATCH 06/16] ci: target recalled README theorems explicitly --- .lean-readme/Aggregate.lean | 17 ++++++++++++++++- HexBareiss/README.md | 4 ++-- HexBareissMathlib/README.md | 6 +++--- HexConway/README.md | 4 ++-- HexDeterminant/README.md | 6 +++--- HexDeterminantMathlib/README.md | 6 +++--- HexGF2/README.md | 6 ++++-- HexGF2Mathlib/README.md | 4 ++-- HexGFqField/README.md | 2 +- HexGFqMathlib/README.md | 2 +- HexGramSchmidt/README.md | 4 ++-- HexGramSchmidtMathlib/README.md | 8 ++++---- HexMatrixMathlib/README.md | 8 ++++---- HexMvPoly/README.md | 4 ++-- HexMvPolyMathlib/README.md | 4 ++-- HexRowReduce/README.md | 8 +++++--- HexRowReduceMathlib/README.md | 6 +++--- SPEC/readme.md | 16 +++++++++------- lake-manifest.json | 4 ++-- lakefile.lean | 2 +- 20 files changed, 71 insertions(+), 50 deletions(-) diff --git a/.lean-readme/Aggregate.lean b/.lean-readme/Aggregate.lean index b5bf9b7ce..a4d101ce8 100644 --- a/.lean-readme/Aggregate.lean +++ b/.lean-readme/Aggregate.lean @@ -6,5 +6,20 @@ Authors: Kim Morrison module -import HexLLL +import Lean +public meta import HexLLL +public section + +private def loadReadmeDynlib (dir stem : String) : IO Unit := do + let ext := if System.Platform.isOSX then "dylib" else "so" + Lean.loadDynlib s!".lake/build/lib/{dir}{stem}.{ext}" + +run_cmd loadReadmeDynlib "" "libhexarithffi" +run_cmd loadReadmeDynlib "" "libHex_HexArith" +run_cmd loadReadmeDynlib "" "libhexmodarithffi" +run_cmd loadReadmeDynlib "" "libHex_HexModArith" +run_cmd loadReadmeDynlib "lean/" "Hex_HexHensel_WordMul" +run_cmd loadReadmeDynlib "" "libHex_HexBasic" +run_cmd loadReadmeDynlib "" "libHex_HexMatrix" +run_cmd loadReadmeDynlib "" "libHex_HexBareiss" diff --git a/HexBareiss/README.md b/HexBareiss/README.md index 77e9ada2f..7b744a873 100644 --- a/HexBareiss/README.md +++ b/HexBareiss/README.md @@ -62,7 +62,7 @@ determinant encoded by `bareissData`. The public determinant agrees with the encoded data, `bareiss_eq_bareissData_det`: -```lean recall +```lean recall Hex.Matrix.bareiss_eq_bareissData_det theorem bareiss_eq_bareissData_det (M : Matrix Int n n) : bareiss M = (bareissData M).det ``` @@ -70,7 +70,7 @@ theorem bareiss_eq_bareissData_det (M : Matrix Int n n) : The no-pivot run, when it reaches the final pivot without a singular step, reads off the last diagonal entry, `bareiss_eq_noPivotLoop_last_of_no_singular`: -```lean recall +```lean recall Hex.Matrix.bareiss_eq_noPivotLoop_last_of_no_singular theorem bareiss_eq_noPivotLoop_last_of_no_singular {k : Nat} (M : Matrix Int (k + 1) (k + 1)) (h_no_sing : diff --git a/HexBareissMathlib/README.md b/HexBareissMathlib/README.md index 9be6cda59..8a5c97cf3 100644 --- a/HexBareissMathlib/README.md +++ b/HexBareissMathlib/README.md @@ -57,14 +57,14 @@ hold outright, with no hypothesis to discharge. The executable Bareiss determinant equals the Leibniz determinant, `bareiss_eq_det`: -```lean recall +```lean recall HexMatrixMathlib.bareiss_eq_det theorem bareiss_eq_det (M : Hex.Matrix Int n n) : Hex.Matrix.bareiss M = Hex.Matrix.det M ``` It also equals Mathlib's determinant, `bareissDet_eq_det`: -```lean recall +```lean recall HexMatrixMathlib.bareissDet_eq_det theorem bareissDet_eq_det (M : Hex.Matrix Int n n) : Hex.Matrix.bareiss M = Matrix.det (matrixEquiv M) ``` @@ -72,7 +72,7 @@ theorem bareissDet_eq_det (M : Hex.Matrix Int n n) : The Mathlib statement is proven directly by running the Bareiss loop and tracking the bordered-minor invariant step by step, `bareiss_eq_mathlib_det`: -```lean recall +```lean recall HexMatrixMathlib.bareiss_eq_mathlib_det theorem bareiss_eq_mathlib_det (M : Hex.Matrix Int n n) : Hex.Matrix.bareiss M = Matrix.det (matrixEquiv M) ``` diff --git a/HexConway/README.md b/HexConway/README.md index aa25909a3..3b8ee4269 100644 --- a/HexConway/README.md +++ b/HexConway/README.md @@ -75,7 +75,7 @@ that the kernel replays; `native_decide` is not used anywhere. The aggregate dispatch theorem is `luebeckConwayPolynomial?_irreducible`, and the API-facing form is -```lean recall +```lean recall Hex.Conway.conwayPoly_irreducible theorem conwayPoly_irreducible (p n : Nat) [ZMod64.Bounds p] (h : SupportedEntry p n) : FpPoly.Irreducible (conwayPoly p n h) @@ -87,7 +87,7 @@ as a negative control so the check is visibly not vacuous. The `Bool` is promoted to a statement about field elements, which is the well-definedness input a subfield embedding needs: -```lean recall +```lean recall Hex.Conway.eval_conwayPoly_subfieldGen_eq_zero theorem eval_conwayPoly_subfieldGen_eq_zero {p m n : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (hm : SupportedEntry p m) (hn : SupportedEntry p n) diff --git a/HexDeterminant/README.md b/HexDeterminant/README.md index 2752d7032..aa7a22811 100644 --- a/HexDeterminant/README.md +++ b/HexDeterminant/README.md @@ -59,7 +59,7 @@ The headline theorem for each of the remaining results (with Column linearity, `det_setCol_add`: -```lean recall +```lean recall Hex.Matrix.det_setCol_add theorem det_setCol_add {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Matrix R n n) (dst : Fin n) (v w : Fin n → R) : det (setCol M dst (fun r => v r + w r)) = @@ -68,7 +68,7 @@ theorem det_setCol_add {R : Type u} [Lean.Grind.CommRing R] {n : Nat} Laplace cofactor expansion along a row, `det_eq_finFoldl_laplace_row`: -```lean recall +```lean recall Hex.Matrix.det_eq_finFoldl_laplace_row theorem det_eq_finFoldl_laplace_row {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Matrix R (n + 1) (n + 1)) (row : Fin (n + 1)) : @@ -89,7 +89,7 @@ their names apart. `det_setRow_setRow_mul_det` is the two-row replacement identity, the `2 × 2` case of Jacobi's adjugate-minor identity: for distinct rows `a`, `b` and arbitrary vectors `u`, `v`, -```lean recall +```lean recall Hex.Matrix.det_setRow_setRow_mul_det theorem det_setRow_setRow_mul_det {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Matrix R (n + 1) (n + 1)) (a b : Fin (n + 1)) (hab : a ≠ b) diff --git a/HexDeterminantMathlib/README.md b/HexDeterminantMathlib/README.md index 916c24f5a..2cafe0199 100644 --- a/HexDeterminantMathlib/README.md +++ b/HexDeterminantMathlib/README.md @@ -67,7 +67,7 @@ Desnanot-Jacobi. The determinant correspondence is fully proven over a `CommRing`. The headline theorem identifies the two determinants: -```lean recall +```lean recall HexMatrixMathlib.det_eq theorem det_eq [CommRing R] (M : Hex.Matrix R n n) : Hex.Matrix.det M = Matrix.det (matrixEquiv M) ``` @@ -76,7 +76,7 @@ The unrestricted three-term Grassmann-Plücker relation, for any three ordered rows `p1 < p2 < p3` (`hex-determinant` proves the Mathlib-free specialisation where `p2` and `p3` are the last two rows): -```lean recall +```lean recall HexMatrixMathlib.det_plucker_three_term theorem det_plucker_three_term {R : Type u} [CommRing R] {n : Nat} (B : Hex.Matrix R (n + 3) (n + 1)) (v : Vector R (n + 3)) @@ -89,7 +89,7 @@ theorem det_plucker_three_term The Desnanot-Jacobi identity over Mathlib matrices: -```lean recall +```lean recall desnanot_jacobi theorem desnanot_jacobi {R : Type*} [CommRing R] {n : ℕ} (M : Matrix (Fin (n + 2)) (Fin (n + 2)) R) : M.det * (M.submatrix (Fin.succAbove 0 ∘ (Fin.last n).succAbove) diff --git a/HexGF2/README.md b/HexGF2/README.md index ed65abfca..9cac7b35a 100644 --- a/HexGF2/README.md +++ b/HexGF2/README.md @@ -69,10 +69,12 @@ Irreducibility is proved rather than tabulated. The Rabin test is sound, and so is certificate replay, which is what lets a committed modulus be checked by the kernel without `native_decide`: -```lean recall +```lean recall Hex.GF2Poly.rabinTest_imp_irreducible theorem rabinTest_imp_irreducible (f : GF2Poly) (hrabin : rabinTest f = true) : GF2Poly.Irreducible f +``` +```lean recall Hex.GF2Poly.checkIrreducibilityCertificate_imp_irreducible theorem checkIrreducibilityCertificate_imp_irreducible (f : GF2Poly) (cert : IrreducibilityCertificate) (hcheck : checkIrreducibilityCertificate f cert = true) : @@ -85,7 +87,7 @@ laws need more: `GF2Poly.Irreducible` is satisfied by the constant `1`, and the quotient by a constant is trivial, so nonconstancy is a separate hypothesis and the field laws are functions rather than instances. -```lean recall +```lean recall Hex.GF2nPoly.isCharPOfDegreePos theorem isCharPOfDegreePos {f : GF2Poly} {hirr : GF2Poly.Irreducible f} (hdeg : 0 < f.degree) : Lean.Grind.IsCharP (GF2nPoly f hirr) 2 diff --git a/HexGF2Mathlib/README.md b/HexGF2Mathlib/README.md index 1ca1d4c3c..53452df89 100644 --- a/HexGF2Mathlib/README.md +++ b/HexGF2Mathlib/README.md @@ -82,7 +82,7 @@ keep the executable operations rather than transported copies, so The single-word wrapper, in namespace `HexGF2Mathlib.GF2n`: -```lean recall +```lean recall HexGF2Mathlib.GF2n.fintype_card theorem fintype_card {n : Nat} {irr : UInt64} {hn : 0 < n} {hn64 : n < 64} {hirr : Hex.GF2Poly.Irreducible (Hex.GF2Poly.ofUInt64Monic irr n)} : Fintype.card (Hex.GF2n n irr hn hn64 hirr) = 2 ^ n @@ -90,7 +90,7 @@ theorem fintype_card {n : Nat} {irr : UInt64} {hn : 0 < n} {hn64 : n < 64} The arbitrary-degree wrapper, in namespace `HexGF2Mathlib.GF2nPoly`: -```lean recall +```lean recall HexGF2Mathlib.GF2nPoly.fintype_card theorem fintype_card {f : Hex.GF2Poly} {hirr : Hex.GF2Poly.Irreducible f} : Fintype.card (Hex.GF2nPoly f hirr) = 2 ^ f.degree ``` diff --git a/HexGFqField/README.md b/HexGFqField/README.md index 82984ad87..2970894c2 100644 --- a/HexGFqField/README.md +++ b/HexGFqField/README.md @@ -71,7 +71,7 @@ example : frob α = α ^ 5 := frob_eq_pow α The field laws are proved, not asserted. Inverse cancellation is the result the rest rests on: -```lean recall +```lean recall Hex.GFqField.mul_inv_cancel theorem mul_inv_cancel {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {hp : Hex.Nat.Prime p} {f : FpPoly p} {hf : 0 < FpPoly.degree f} {hirr : FpPoly.Irreducible f} diff --git a/HexGFqMathlib/README.md b/HexGFqMathlib/README.md index 584606c57..3a038bb09 100644 --- a/HexGFqMathlib/README.md +++ b/HexGFqMathlib/README.md @@ -69,7 +69,7 @@ example {p n : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] The executable field carries Mathlib's `Field` structure, and the carrier is finite with the cardinality its construction promises: -```lean recall +```lean recall HexGFqMathlib.GFq.fintype_card_eq_pow theorem fintype_card_eq_pow {p n : Nat} [Hex.ZMod64.Bounds p] (h : Hex.Conway.SupportedEntry p n) : Fintype.card (Hex.GFq p n h) = p ^ n diff --git a/HexGramSchmidt/README.md b/HexGramSchmidt/README.md index cdf8444da..c4f99c9c1 100644 --- a/HexGramSchmidt/README.md +++ b/HexGramSchmidt/README.md @@ -71,7 +71,7 @@ lower-unitriangular coefficient matrix) are available over both rings. The orthogonalization theory is proven over the Mathlib-free integer and rational cores. The orthogonal basis, `basis_orthogonal`: -```lean recall +```lean recall Hex.GramSchmidt.Int.basis_orthogonal theorem basis_orthogonal (b : Matrix Int n m) (i j : Nat) (hi : i < n) (hj : j < n) (hij : i ≠ j) : ((basis b).row ⟨i, hi⟩).dotProduct ((basis b).row ⟨j, hj⟩) = 0 @@ -82,7 +82,7 @@ coefficient laws `coeffs_diag` and `coeffs_upper`, the span equality `basis_span`, and the update laws for `sizeReduce` and `adjacentSwap`. The key lattice estimate, `normSq_latticeVec_ge_min_basis_normSq`: -```lean recall +```lean recall Hex.GramSchmidt.Int.normSq_latticeVec_ge_min_basis_normSq theorem normSq_latticeVec_ge_min_basis_normSq (b : Matrix Int n m) (_hli : independent b) (v : Vector Int m) (hv : memLattice b v) (hv' : v ≠ 0) : diff --git a/HexGramSchmidtMathlib/README.md b/HexGramSchmidtMathlib/README.md index 95f9dae9a..c2b0daac2 100644 --- a/HexGramSchmidtMathlib/README.md +++ b/HexGramSchmidtMathlib/README.md @@ -61,7 +61,7 @@ The proof-facing API splits into two parts. The rowwise correspondence with Mathlib's orthogonalization is fully proven. Over the rationals: -```lean recall +```lean recall Hex.GramSchmidtMathlib.rat_basis_row_eq_gramSchmidt theorem rat_basis_row_eq_gramSchmidt (b : Matrix Rat n m) (i : Fin n) : rowToEuclidean ((Hex.GramSchmidt.Rat.basis b).row i) = InnerProductSpace.gramSchmidt ℝ (ratRowFamily b) i @@ -69,7 +69,7 @@ theorem rat_basis_row_eq_gramSchmidt (b : Matrix Rat n m) (i : Fin n) : and the integer version, casting the integer rows first: -```lean recall +```lean recall Hex.GramSchmidtMathlib.int_basis_row_eq_gramSchmidt theorem int_basis_row_eq_gramSchmidt (b : Matrix Int n m) (i : Fin n) : rowToEuclidean ((Hex.GramSchmidt.Int.basis b).row i) = InnerProductSpace.gramSchmidt ℝ (intRowFamily b) i @@ -78,7 +78,7 @@ theorem int_basis_row_eq_gramSchmidt (b : Matrix Int n m) (i : Fin n) : The fraction-free integer surface is identified with Bareiss determinants. Below the diagonal the scaled coefficients are exactly: -```lean recall +```lean recall Hex.GramSchmidt.Int.scaledCoeffs_eq_scaledCoeffMatrix_bareiss theorem scaledCoeffs_eq_scaledCoeffMatrix_bareiss (b : Matrix Int n m) (i j : Fin n) (hji : j.val < i.val) : GramSchmidt.entry (scaledCoeffs b) i j = @@ -88,7 +88,7 @@ theorem scaledCoeffs_eq_scaledCoeffMatrix_bareiss and for an independent matrix the leading Gram determinant is the product of squared Gram-Schmidt norms: -```lean recall +```lean recall Hex.GramSchmidt.Int.gramDet_eq_prod_normSq theorem gramDet_eq_prod_normSq (b : Matrix Int n m) (hli : independent b) (k : Nat) (hk : k ≤ n) : (gramDet b k hk : Rat) = gramSchmidtNormProduct b k hk diff --git a/HexMatrixMathlib/README.md b/HexMatrixMathlib/README.md index 54610bf2c..81aa9e0d6 100644 --- a/HexMatrixMathlib/README.md +++ b/HexMatrixMathlib/README.md @@ -76,7 +76,7 @@ open Hex HexMatrixMathlib def matrixEquiv : Hex.Matrix R n m ≃ Matrix (Fin n) (Fin m) R ``` -```lean recall +```lean recall HexMatrixMathlib.matrixEquiv_apply theorem matrixEquiv_apply (M : Hex.Matrix R n m) (i : Fin n) (j : Fin m) : matrixEquiv M i j = M[i][j] ``` @@ -84,7 +84,7 @@ theorem matrixEquiv_apply (M : Hex.Matrix R n m) (i : Fin n) (j : Fin m) : The elementary row operations correspond to Mathlib's elementary matrices. A swap is left multiplication by the permutation matrix `Matrix.swap`: -```lean recall +```lean recall HexMatrixMathlib.matrixEquiv_rowSwap theorem matrixEquiv_rowSwap {R : Type u} [Semiring R] {n m : Nat} (M : Hex.Matrix R n m) (i j : Fin n) : matrixEquiv (Hex.Matrix.rowSwap M i j) = Matrix.swap R i j * matrixEquiv M @@ -92,7 +92,7 @@ theorem matrixEquiv_rowSwap {R : Type u} [Semiring R] {n m : Nat} A row addition is left multiplication by `Matrix.transvection`: -```lean recall +```lean recall HexMatrixMathlib.matrixEquiv_rowAdd theorem matrixEquiv_rowAdd {R : Type u} [CommRing R] {n m : Nat} (M : Hex.Matrix R n m) (src dst : Fin n) (c : R) : matrixEquiv (Hex.Matrix.rowAdd M src dst c) = @@ -101,7 +101,7 @@ theorem matrixEquiv_rowAdd {R : Type u} [CommRing R] {n m : Nat} The matrix-vector product transports to Mathlib's `Matrix.mulVec`: -```lean recall +```lean recall HexMatrixMathlib.vectorEquiv_mulVec theorem vectorEquiv_mulVec [Semiring R] (M : Hex.Matrix R n m) (v : Vector R m) : vectorEquiv (M * v) = (matrixEquiv M).mulVec (vectorEquiv v) ``` diff --git a/HexMvPoly/README.md b/HexMvPoly/README.md index 2c1a9e246..9ed6fba8f 100644 --- a/HexMvPoly/README.md +++ b/HexMvPoly/README.md @@ -64,7 +64,7 @@ recursive-view laws. A product coefficient is the convolution over every monomial split: -```lean recall +```lean recall Hex.MvPoly.coeff_mul theorem coeff_mul {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [Lean.Grind.Semiring R] [DecidableEq R] @@ -76,7 +76,7 @@ theorem coeff_mul {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} Sparse Horner evaluation agrees with direct evaluation: -```lean recall +```lean recall Hex.MvPoly.evalHorner_eq theorem evalHorner_eq {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Lean.Grind.CommSemiring R] (x : Fin n → R) (p : MvPoly n R cmp) : diff --git a/HexMvPolyMathlib/README.md b/HexMvPolyMathlib/README.md index 9b4d04a90..54da50029 100644 --- a/HexMvPolyMathlib/README.md +++ b/HexMvPolyMathlib/README.md @@ -71,7 +71,7 @@ def equiv {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} It preserves every coefficient: -```lean recall +```lean recall HexMvPolyMathlib.coeff_toMvPolynomial theorem coeff_toMvPolynomial {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [CommSemiring R] [DecidableEq R] @@ -82,7 +82,7 @@ theorem coeff_toMvPolynomial Executable evaluation is Mathlib algebra evaluation after conversion: -```lean recall +```lean recall HexMvPolyMathlib.aeval_apply theorem aeval_apply {n : Nat} {R : Type u} {S : Type v} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] diff --git a/HexRowReduce/README.md b/HexRowReduce/README.md index fa46e44b7..a3276c94f 100644 --- a/HexRowReduce/README.md +++ b/HexRowReduce/README.md @@ -58,7 +58,7 @@ Over a field the reduction is fully proven. The headline theorem states that sorted and equal to 1, all other pivot-column entries zero, trailing rows zero, and an invertible transform with `transform * M = echelon`): -```lean recall +```lean recall Hex.Matrix.rowReduce_isRowReduced theorem rowReduce_isRowReduced {R : Type u} {n m : Nat} [Lean.Grind.Field R] [DecidableEq R] (M : Matrix R n m) : IsRowReduced M (rowReduce M) @@ -66,7 +66,7 @@ theorem rowReduce_isRowReduced The row-span wrappers are sound, with `spanCoeffs_sound`: -```lean recall +```lean recall Hex.Matrix.spanCoeffs_sound theorem spanCoeffs_sound {R : Type u} {n m : Nat} [Lean.Grind.Field R] [DecidableEq R] (M : Matrix R n m) (v : Vector R m) (c : Vector R n) : @@ -76,13 +76,15 @@ theorem spanCoeffs_sound The nullspace basis is both sound and complete, `nullspace_sound` and `nullspace_complete`: -```lean recall +```lean recall Hex.Matrix.nullspace_sound theorem nullspace_sound {R : Type u} {n m : Nat} [Lean.Grind.Field R] [DecidableEq R] (M : Matrix R n m) (k : Fin (m - rowReduce_rank M)) : M * (nullspace M).get k = 0 +``` +```lean recall Hex.Matrix.nullspace_complete theorem nullspace_complete {R : Type u} {n m : Nat} [Lean.Grind.Field R] [DecidableEq R] (M : Matrix R n m) diff --git a/HexRowReduceMathlib/README.md b/HexRowReduceMathlib/README.md index fd19998d1..10e761abd 100644 --- a/HexRowReduceMathlib/README.md +++ b/HexRowReduceMathlib/README.md @@ -64,7 +64,7 @@ row span, and nullspace are computable witnesses for Mathlib's noncomputable Rank, `rank_eq`: -```lean recall +```lean recall HexMatrixMathlib.rank_eq theorem rank_eq [Field R] {M : Hex.Matrix R n m} {D : Hex.Matrix.RowEchelonData R n m} (E : Hex.Matrix.IsRowReduced M D) : @@ -73,7 +73,7 @@ theorem rank_eq [Field R] Nullspace, `nullspace_span_eq_ker`: -```lean recall +```lean recall HexMatrixMathlib.nullspace_span_eq_ker theorem nullspace_span_eq_ker [Field R] {M : Hex.Matrix R n m} {D : Hex.Matrix.RowEchelonData R n m} (E : Hex.Matrix.IsRowReduced M D) : @@ -83,7 +83,7 @@ theorem nullspace_span_eq_ker [Field R] Span, `spanContains_iff_mem_span`: -```lean recall +```lean recall HexMatrixMathlib.spanContains_iff_mem_span theorem spanContains_iff_mem_span [Field R] [DecidableEq R] {M : Hex.Matrix R n m} {D : Hex.Matrix.RowEchelonData R n m} (E : Hex.Matrix.IsRowReduced M D) (v : Vector R m) : diff --git a/SPEC/readme.md b/SPEC/readme.md index 2a1deae3d..852536c65 100644 --- a/SPEC/readme.md +++ b/SPEC/readme.md @@ -45,13 +45,15 @@ Use these five level-1 headings, in this order. for executable use only. Where it helps the reader, quote the headline theorem for each significant result as a Lean signature (name plus statement, proof elided) in a `lean` code block, copied verbatim from - the source so it stays accurate. Mark theorem blocks as `lean recall`: - `lean-readme` then checks each displayed `theorem` statement directly against - the declaration in the imported library, without changing the rendered - Markdown or depending on Mathlib's `recall` command. Other quoted declaration - kinds remain ordinary `lean` blocks. Because blocks are checked in order, - `lean recall` blocks reuse the Quickstart block's imports and namespace - openings rather than repeating them in the rendered theorem quotation. + the source so it stays accurate. Mark theorem blocks as + `lean recall Fully.Qualified.theoremName`: `lean-readme` then checks each + displayed `theorem` statement directly against that declaration in the + imported library, without changing the rendered Markdown or depending on + Mathlib's `recall` command. The explicit target makes the check independent + of namespace openings and unambiguous when declarations share a short name. + Other quoted declaration kinds remain ordinary `lean` blocks. Because blocks + are checked in order, recall blocks reuse the Quickstart block's imports + rather than repeating them in the rendered theorem quotation. Executable examples must remain checked. Point at the sibling library where the rest of the theory lives. diff --git a/lake-manifest.json b/lake-manifest.json index 20f337787..535454416 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -25,10 +25,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "4ef92a1dcaedc189ab41b59ba04fe40ac6afd4b9", + "rev": "2a286f42701c22dffafc9d2ff3222f8d3ac4994a", "name": "«lean-readme»", "manifestFile": "lake-manifest.json", - "inputRev": "4ef92a1dcaedc189ab41b59ba04fe40ac6afd4b9", + "inputRev": "2a286f42701c22dffafc9d2ff3222f8d3ac4994a", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover/verso.git", diff --git a/lakefile.lean b/lakefile.lean index b00574f4e..598fe521d 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -16,7 +16,7 @@ require verso from git require «lean-readme» from git "https://github.com/kim-em/lean-readme.git" @ - "4ef92a1dcaedc189ab41b59ba04fe40ac6afd4b9" + "2a286f42701c22dffafc9d2ff3222f8d3ac4994a" require «lean-bench» from git "https://github.com/kim-em/lean-bench.git" @ "master" From 525c5f13c61bd02fc1a8d10bc3c8a738b742fcdf Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 24 Aug 2026 03:32:55 +0000 Subject: [PATCH 07/16] ci: refresh README tooling exemptions --- scripts/bench/proof_only_runtime_exemptions.json | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/scripts/bench/proof_only_runtime_exemptions.json b/scripts/bench/proof_only_runtime_exemptions.json index c244a3a43..b945c391d 100644 --- a/scripts/bench/proof_only_runtime_exemptions.json +++ b/scripts/bench/proof_only_runtime_exemptions.json @@ -770,13 +770,13 @@ { "path": "lakefile.lean", "baseline_blob": "ff87edbbbf7524190b536ae4ce92a57968275aa9", - "current_blob": "b00574f4e87aeacd2b07598d3e8c6bd4b9a8dc82", + "current_blob": "598fe521d5ced1dfef712ae8b0162029d67d56f2", "reason": "Adds and pins the lean-readme documentation checker only; the factorization service target and its executable dependency graph are unchanged." }, { "path": "lake-manifest.json", "baseline_blob": "5f5b01e430fb8241d938d392298d786b38f67104", - "current_blob": "20f3377876c8d17e4c711d0e7edc452011913b28", + "current_blob": "5354544164736bfa1c724e2cca77be0a8c96f0a0", "reason": "Updates only the pinned lean-readme documentation checker revision; every factorization dependency remains unchanged." }, { From 438b3b57a09060ef1cb913b92f7d44218bf017a4 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 24 Aug 2026 03:37:04 +0000 Subject: [PATCH 08/16] ci: rebase README exemptions on current measurements --- scripts/bench/proof_only_runtime_exemptions.json | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/scripts/bench/proof_only_runtime_exemptions.json b/scripts/bench/proof_only_runtime_exemptions.json index ca0ad6b60..9b028dad9 100644 --- a/scripts/bench/proof_only_runtime_exemptions.json +++ b/scripts/bench/proof_only_runtime_exemptions.json @@ -787,14 +787,14 @@ }, { "path": "lakefile.lean", - "baseline_blob": "ff87edbbbf7524190b536ae4ce92a57968275aa9", - "current_blob": "598fe521d5ced1dfef712ae8b0162029d67d56f2", - "reason": "Adds and pins the lean-readme documentation checker only; the factorization service target and its executable dependency graph are unchanged." + "baseline_blob": "a1b87406682dbf908d990f01676f326499b906e5", + "current_blob": "204a091e087f8da8f227e6adc5dc2d8f85c862e4", + "reason": "Registers the upstream sparse-poly and modular conformance targets together with the pinned lean-readme documentation checker; the factorization service target, executable dependency graph, definitions, and build flags are unchanged." }, { "path": "lake-manifest.json", - "baseline_blob": "5f5b01e430fb8241d938d392298d786b38f67104", - "current_blob": "5354544164736bfa1c724e2cca77be0a8c96f0a0", + "baseline_blob": "d7675a65d5bec03396cb8f75c81bff62479b64e9", + "current_blob": "baa97c4e3953de6e3a7eea9bdea72e493d1c1534", "reason": "Updates only the pinned lean-readme documentation checker revision; every factorization dependency remains unchanged." }, { From d7cdfe167a9fafa39fec667affaeb32eec2af9a8 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 24 Aug 2026 03:48:03 +0000 Subject: [PATCH 09/16] docs: recall sparse polynomial theorems explicitly --- HexSparsePoly/README.md | 5 +++-- HexSparsePolyMathlib/README.md | 11 ++++++++--- 2 files changed, 11 insertions(+), 5 deletions(-) diff --git a/HexSparsePoly/README.md b/HexSparsePoly/README.md index b3bf09fc6..0ab899160 100644 --- a/HexSparsePoly/README.md +++ b/HexSparsePoly/README.md @@ -61,8 +61,9 @@ implementation is selected by a proved `@[csimp]` equality, and every public operation has a coefficient lemma; equalities reduce to coefficient extensionality: -```lean -theorem ext_coeff {s t : SparsePoly R} +```lean recall Hex.SparsePoly.ext_coeff +theorem ext_coeff {R : Type u} [Zero R] [DecidableEq R] + {s t : SparsePoly R} (h : ∀ e : Nat, s.coeff e = t.coeff e) : s = t ``` diff --git a/HexSparsePolyMathlib/README.md b/HexSparsePolyMathlib/README.md index b075466dc..0e053d9ff 100644 --- a/HexSparsePolyMathlib/README.md +++ b/HexSparsePolyMathlib/README.md @@ -54,10 +54,15 @@ example (p : SparsePoly Int) (x : Int) : (equiv p).eval x = p.eval x := by Everything is proved; there is no axiom and no `sorry`. The headline is the exact identification and its two semantic clauses: -```lean -theorem coeff_equiv (s : Hex.SparsePoly R) (e : Nat) : +```lean recall HexSparsePolyMathlib.coeff_equiv +theorem coeff_equiv {R : Type u} [CommRing R] [DecidableEq R] + (s : Hex.SparsePoly R) (e : Nat) : (equiv s).coeff e = s.coeff e -theorem equiv_support (s : Hex.SparsePoly R) : +``` + +```lean recall HexSparsePolyMathlib.equiv_support +theorem equiv_support {R : Type u} [CommRing R] [DecidableEq R] + (s : Hex.SparsePoly R) : (equiv s).support = s.support.toList.toFinset ``` From f94e5e9e89e7351cf788556d370893d09ceb9e19 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 24 Aug 2026 04:06:08 +0000 Subject: [PATCH 10/16] ci: refresh README exemption after main merge --- scripts/bench/proof_only_runtime_exemptions.json | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/scripts/bench/proof_only_runtime_exemptions.json b/scripts/bench/proof_only_runtime_exemptions.json index f82081d21..bcf7b270d 100644 --- a/scripts/bench/proof_only_runtime_exemptions.json +++ b/scripts/bench/proof_only_runtime_exemptions.json @@ -788,8 +788,8 @@ { "path": "lakefile.lean", "baseline_blob": "a1b87406682dbf908d990f01676f326499b906e5", - "current_blob": "204a091e087f8da8f227e6adc5dc2d8f85c862e4", - "reason": "Registers the upstream sparse-poly and modular conformance targets together with the pinned lean-readme documentation checker; the factorization service target, executable dependency graph, definitions, and build flags are unchanged." + "current_blob": "2765df3feaa834e1241686e49445edf1d8b186d8", + "reason": "Registers the upstream sparse-poly, modular, and interval runtime conformance targets together with the pinned lean-readme documentation checker; the factorization service target, executable dependency graph, definitions, and build flags are unchanged." }, { "path": "lake-manifest.json", From 9f730b73f61cd22212189f727d667f319e400b88 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 24 Aug 2026 04:19:59 +0000 Subject: [PATCH 11/16] ci: expose Lean import to aggregate README prefix --- .lean-readme/Aggregate.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.lean-readme/Aggregate.lean b/.lean-readme/Aggregate.lean index a4d101ce8..4eed52e57 100644 --- a/.lean-readme/Aggregate.lean +++ b/.lean-readme/Aggregate.lean @@ -6,7 +6,7 @@ Authors: Kim Morrison module -import Lean +public import Lean public meta import HexLLL public section From 7762b8c1a6839c9a1d3e593abd145d6acc21dcf3 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 24 Aug 2026 04:35:08 +0000 Subject: [PATCH 12/16] ci: keep aggregate README setup private --- .lean-readme/Aggregate.lean | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/.lean-readme/Aggregate.lean b/.lean-readme/Aggregate.lean index 4eed52e57..5ec8c5176 100644 --- a/.lean-readme/Aggregate.lean +++ b/.lean-readme/Aggregate.lean @@ -6,11 +6,9 @@ Authors: Kim Morrison module -public import Lean +import Lean public meta import HexLLL -public section - private def loadReadmeDynlib (dir stem : String) : IO Unit := do let ext := if System.Platform.isOSX then "dylib" else "so" Lean.loadDynlib s!".lake/build/lib/{dir}{stem}.{ext}" From 6a2fc94c8e682e76c100aad5083ce2a87b4b8568 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 24 Aug 2026 04:48:58 +0000 Subject: [PATCH 13/16] ci: build the top-level Hex helper --- .github/workflows/ci.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index ec6542e7a..333f27adb 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -158,7 +158,7 @@ jobs: # fresh against the restored libs, which is cheap. - name: Define the hex-dev cache + build target sets run: | - echo "HEX_LIB_TARGETS=HexBasic HexArith HexPoly HexMvPoly HexModArith HexGF2 HexPolyZ HexRoots HexResultant HexInterval HexIntervalExperiment HexIntervalMathlib HexIntervalMathlibExperiment HexIntervalReplayProbe HexIntervalMathlibReplayProbe HexRealRootsMathlibReplayProbe HexRCFProofProbe HexPolyFp HexGFqRing HexGFqField HexBerlekamp HexHensel HexConway HexGFq HexBerlekampZassenhaus HexRealRoots HexMatrix HexRowReduce HexDeterminant HexBareiss HexCharPoly HexGramSchmidt HexLLL HexMatrixMathlib HexCharPolyMathlib HexGramSchmidtMathlib HexLLLMathlib HexBerlekampZassenhausMathlib HexPolyFpMathlib HexFactorizationModules HexRealRootsMathlib HexGF2Mathlib HexGFqMathlib HexMvPolyMathlib HexMvPolyMathlibProofProbe HexRCF HexRCFTests HexRootsMathlib HexResultantMathlib HexNumberField HexNumberFieldMathlib HexNumberFieldTower HexNumberFieldTowerMathlib HexReleaseTests HexReleaseExamples HexAggregateCheck" >> "$GITHUB_ENV" + echo "HEX_LIB_TARGETS=Hex HexBasic HexArith HexPoly HexMvPoly HexModArith HexGF2 HexPolyZ HexRoots HexResultant HexInterval HexIntervalExperiment HexIntervalMathlib HexIntervalMathlibExperiment HexIntervalReplayProbe HexIntervalMathlibReplayProbe HexRealRootsMathlibReplayProbe HexRCFProofProbe HexPolyFp HexGFqRing HexGFqField HexBerlekamp HexHensel HexConway HexGFq HexBerlekampZassenhaus HexRealRoots HexMatrix HexRowReduce HexDeterminant HexBareiss HexCharPoly HexGramSchmidt HexLLL HexMatrixMathlib HexCharPolyMathlib HexGramSchmidtMathlib HexLLLMathlib HexBerlekampZassenhausMathlib HexPolyFpMathlib HexFactorizationModules HexRealRootsMathlib HexGF2Mathlib HexGFqMathlib HexMvPolyMathlib HexMvPolyMathlibProofProbe HexRCF HexRCFTests HexRootsMathlib HexResultantMathlib HexNumberField HexNumberFieldMathlib HexNumberFieldTower HexNumberFieldTowerMathlib HexReleaseTests HexReleaseExamples HexAggregateCheck" >> "$GITHUB_ENV" echo "HEX_EXE_TARGETS=hexarith_bench hexpoly_bench hexmvpoly_bench hexsparsepoly_bench hexpolyz_bench hexpolyfp_bench hexmodarith_bench hexgf2_bench hexgfqring_bench hexgfqfield_bench hexgfq_bench hexhensel_bench hexberlekamp_bench hexbz_bench hexconway_bench hexmatrix_bench hexstrassen_compare hexdeterminant_bench hexbareiss_bench hexcharpoly_bench hexgramschmidt_bench hexrealroots_bench hexrcf_bench hexroots_bench hexresultant_bench hexnumberfield_bench hexnumberfieldtower_bench hexinterval_decision_bench hexroots_demo hex_interval_representation_spike hex_interval_center_spike hex_interval_scale_spike hex_interval_scheduler_spike hex_interval_policy_frontier_spike hex_arith_floor hexlll_bench hexlll_gram_bench hexlll_external_reduction hexbz_factor_service" >> "$GITHUB_ENV" # Shared build. The libraries, bench exes, conformance #guard drivers, and # emit-fixture exes are all elaborated here so the two verification tails From 7b7bc06093d58bc9c04a43c4c3edc39118562ef9 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 24 Aug 2026 04:52:29 +0000 Subject: [PATCH 14/16] ci: refresh README exemption after main merge --- scripts/bench/proof_only_runtime_exemptions.json | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/scripts/bench/proof_only_runtime_exemptions.json b/scripts/bench/proof_only_runtime_exemptions.json index 8e8789fb9..edaf1eabf 100644 --- a/scripts/bench/proof_only_runtime_exemptions.json +++ b/scripts/bench/proof_only_runtime_exemptions.json @@ -788,8 +788,8 @@ { "path": "lakefile.lean", "baseline_blob": "a1b87406682dbf908d990f01676f326499b906e5", - "current_blob": "2765df3feaa834e1241686e49445edf1d8b186d8", - "reason": "Registers the upstream sparse-poly, modular, and interval runtime conformance targets together with the pinned lean-readme documentation checker; the factorization service target, executable dependency graph, definitions, and build flags are unchanged." + "current_blob": "75e7981def51aaac0e6125d1a0838f80f0f885f6", + "reason": "Registers the upstream sparse-poly, modular, interval runtime, and polynomial-gcd conformance targets together with the pinned lean-readme documentation checker; the factorization service target, executable dependency graph, definitions, and build flags are unchanged." }, { "path": "lake-manifest.json", From cb5b9b4ad08b8ff59d150e7aa488256d938225c5 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 27 Aug 2026 09:06:53 +1000 Subject: [PATCH 15/16] Re-anchor proof-only exemptions after merging main --- .../lake-manifest-json-d7675a65-baa97c4e.json | 6 ++++++ .../lakefile-lean-8226e990-006ad89b.json | 6 ++++++ 2 files changed, 12 insertions(+) create mode 100644 scripts/bench/proof_only_runtime_exemptions/lake-manifest-json-d7675a65-baa97c4e.json create mode 100644 scripts/bench/proof_only_runtime_exemptions/lakefile-lean-8226e990-006ad89b.json diff --git a/scripts/bench/proof_only_runtime_exemptions/lake-manifest-json-d7675a65-baa97c4e.json b/scripts/bench/proof_only_runtime_exemptions/lake-manifest-json-d7675a65-baa97c4e.json new file mode 100644 index 000000000..c78089a28 --- /dev/null +++ b/scripts/bench/proof_only_runtime_exemptions/lake-manifest-json-d7675a65-baa97c4e.json @@ -0,0 +1,6 @@ +{ + "path": "lake-manifest.json", + "baseline_blob": "d7675a65d5bec03396cb8f75c81bff62479b64e9", + "current_blob": "baa97c4e3953de6e3a7eea9bdea72e493d1c1534", + "reason": "Updates only the pinned lean-readme documentation checker revision; every factorization dependency remains unchanged." +} diff --git a/scripts/bench/proof_only_runtime_exemptions/lakefile-lean-8226e990-006ad89b.json b/scripts/bench/proof_only_runtime_exemptions/lakefile-lean-8226e990-006ad89b.json new file mode 100644 index 000000000..1291943f1 --- /dev/null +++ b/scripts/bench/proof_only_runtime_exemptions/lakefile-lean-8226e990-006ad89b.json @@ -0,0 +1,6 @@ +{ + "path": "lakefile.lean", + "baseline_blob": "8226e99030e7d5fa79f36b5652119b97ab8e0110", + "current_blob": "006ad89b94bb3c7621075d0d275f984a4193d0dc", + "reason": "Registers the upstream sparse-poly, modular, interval runtime, and polynomial-gcd conformance targets together with the pinned lean-readme documentation checker; the factorization service target, executable dependency graph, definitions, and build flags are unchanged." +} From 33ee060f35d18c6864c32bfda250236ffb2a3bf9 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 31 Aug 2026 10:26:12 +1000 Subject: [PATCH 16/16] ci: re-anchor the lakefile proof-only exemption after merging main The merge changed the lakefile blob, so the previous exemption no longer matched and the factorization sweep was reported stale. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_01WGQ4cXuC9bBbZQ3psYLZUA --- .../lakefile-lean-e82c6493-cf58f84d.json | 6 ++++++ 1 file changed, 6 insertions(+) create mode 100644 scripts/bench/proof_only_runtime_exemptions/lakefile-lean-e82c6493-cf58f84d.json diff --git a/scripts/bench/proof_only_runtime_exemptions/lakefile-lean-e82c6493-cf58f84d.json b/scripts/bench/proof_only_runtime_exemptions/lakefile-lean-e82c6493-cf58f84d.json new file mode 100644 index 000000000..a18dc677d --- /dev/null +++ b/scripts/bench/proof_only_runtime_exemptions/lakefile-lean-e82c6493-cf58f84d.json @@ -0,0 +1,6 @@ +{ + "path": "lakefile.lean", + "baseline_blob": "e82c649322c5dc6574071e576e92d644683eb00a", + "current_blob": "cf58f84d736d845c8f47cbf0054c19e88c1a9c5b", + "reason": "Adds the pinned lean-readme documentation checker as a dependency on top of main's inherited HexPolyFp precompileModules setting. The checker is required only by the README snippet targets, and precompilation changes build and link availability alone; hexbz_factor_service, its build flags, and every library it imports are unchanged." +}