diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 5c29e4be4..70d4aaac0 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -168,7 +168,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 HexTruncatedSeries HexTruncatedSeriesMathlib HexArith HexPoly HexPolyFast HexMvPoly HexModArith HexGF2 HexPolyZ HexRoots HexResultant HexInterval HexIntervalExperiment HexIntervalMathlib HexIntervalMathlibExperiment HexIntervalReplayProbe HexIntervalMathlibReplayProbe HexRealRootsMathlibReplayProbe HexRCFProofProbe HexPolyFp HexGFqRing HexGFqField HexBerlekamp HexHensel HexConway HexGFq HexPrimality HexIntFactor HexPrimalityKernelProbe HexPrimalityElabProbe HexIntFactorKernelProbe HexMvGcdKernelProbe HexBerlekampZassenhaus HexRealRoots HexMatrix HexRowReduce HexDeterminant HexBareiss HexHermite HexSmith HexCharPoly HexMinPoly HexPolySmith HexGramSchmidt HexLLL HexMatrixMathlib HexHermiteMathlib HexSmithMathlib HexSmithTests HexCharPolyMathlib HexMinPolyMathlib HexPolySmithMathlib HexGramSchmidtMathlib HexLLLMathlib HexBerlekampZassenhausMathlib HexBerlekampZassenhausMathlibProofProbe HexBerlekampMathlibProofProbe HexPrimalityMathlib HexIntFactorMathlib 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 HexTruncatedSeries HexTruncatedSeriesMathlib HexArith HexPoly HexPolyFast HexMvPoly HexModArith HexGF2 HexPolyZ HexRoots HexResultant HexInterval HexIntervalExperiment HexIntervalMathlib HexIntervalMathlibExperiment HexIntervalReplayProbe HexIntervalMathlibReplayProbe HexRealRootsMathlibReplayProbe HexRCFProofProbe HexPolyFp HexGFqRing HexGFqField HexBerlekamp HexHensel HexConway HexGFq HexPrimality HexIntFactor HexPrimalityKernelProbe HexPrimalityElabProbe HexIntFactorKernelProbe HexMvGcdKernelProbe HexBerlekampZassenhaus HexRealRoots HexMatrix HexRowReduce HexDeterminant HexBareiss HexHermite HexSmith HexCharPoly HexMinPoly HexPolySmith HexGramSchmidt HexLLL HexMatrixMathlib HexHermiteMathlib HexSmithMathlib HexSmithTests HexCharPolyMathlib HexMinPolyMathlib HexPolySmithMathlib HexGramSchmidtMathlib HexLLLMathlib HexBerlekampZassenhausMathlib HexBerlekampZassenhausMathlibProofProbe HexBerlekampMathlibProofProbe HexPrimalityMathlib HexIntFactorMathlib HexPolyFpMathlib HexFactorizationModules HexRealRootsMathlib HexGF2Mathlib HexGFqMathlib HexMvPolyMathlib HexMvPolyMathlibProofProbe HexRCF HexRCFTests HexRootsMathlib HexResultantMathlib HexNumberField HexNumberFieldMathlib HexNumberFieldTower HexNumberFieldTowerMathlib HexReleaseTests HexReleaseExamples HexAggregateCheck" >> "$GITHUB_ENV"
           echo "HEX_EXE_TARGETS=hextruncatedseries_bench hexarith_bench hexpoly_bench hexpolyfast_bench hexpolysmith_bench hexmvpoly_bench hexmvgcd_bench hexsparsepoly_bench hexpolyz_bench hexpolyfp_bench hexmodarith_bench hexmodular_bench hexgf2_bench hexgfqring_bench hexgfqfield_bench hexgfq_bench hexhensel_bench hexprimality_bench hexprimality_policy_probe hexprimality_fuel_probe hexintfactor_bench hexberlekamp_bench hexbz_bench hexconway_bench hexmatrix_bench hexstrassen_compare hexdeterminant_bench hexbareiss_bench hexcharpoly_bench hexminpoly_bench hexgramschmidt_bench hexhermite_bench hexsmith_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
@@ -212,6 +212,20 @@ jobs:
             hexnumberfieldtower_emit_fixtures
       - name: Build HexManual
         run: lake build HexManual
+      - name: Check README Lean snippets
+        run: |
+          for readme in Hex*/README.md; do
+            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
       # --- Parallel verification tails (single job, in-job parallel steps) ---
       # Both tails only read the already-built .lake/build; they write to
       # disjoint outputs, so they are safe to run concurrently. Each touches a
diff --git a/.lean-readme/Aggregate.lean b/.lean-readme/Aggregate.lean
new file mode 100644
index 000000000..5ec8c5176
--- /dev/null
+++ b/.lean-readme/Aggregate.lean
@@ -0,0 +1,23 @@
+/-
+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 HexLLL
+
+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/.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 a0a153c76..6bf244ca1 100644
--- a/HexBareiss/README.md
+++ b/HexBareiss/README.md
@@ -74,7 +74,7 @@ Mathlib bridge proves quotient exactness implies agreement with the determinant.
 
 The public determinant agrees with the encoded data, `bareiss_eq_bareissData_det`:
 
-```lean
+```lean recall Hex.Matrix.bareiss_eq_bareissData_det
 theorem bareiss_eq_bareissData_det (M : Matrix Int n n) :
     bareiss M = (bareissData M).det
 ```
@@ -82,7 +82,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 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 78f78e93e..a7c91e44c 100644
--- a/HexBareissMathlib/README.md
+++ b/HexBareissMathlib/README.md
@@ -72,14 +72,14 @@ the preferred compatibility surface and hold outright.
 The executable Bareiss determinant equals the Leibniz determinant,
 `bareiss_eq_det`:
 
-```lean
+```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
+```lean recall HexMatrixMathlib.bareissDet_eq_det
 theorem bareissDet_eq_det (M : Hex.Matrix Int n n) :
     Hex.Matrix.bareiss M = Matrix.det (matrixEquiv M)
 ```
@@ -87,7 +87,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 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 630620b22..b4dc30805 100644
--- a/HexConway/README.md
+++ b/HexConway/README.md
@@ -77,7 +77,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 recall Hex.Conway.conwayPoly_irreducible
 theorem conwayPoly_irreducible
     (p n : Nat) [ZMod64.Bounds p] (h : SupportedEntry p n) :
     FpPoly.Irreducible (conwayPoly p n h)
@@ -89,7 +89,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 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 f24370671..aa7a22811 100644
--- a/HexDeterminant/README.md
+++ b/HexDeterminant/README.md
@@ -59,16 +59,19 @@ The headline theorem for each of the remaining results (with
 
 Column linearity, `det_setCol_add`:
 
-```lean
-theorem det_setCol_add (M : Matrix R n n) (dst : Fin n) (v w : Fin n → R) :
+```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)) =
       det (setCol M dst v) + det (setCol M dst w)
 ```
 
 Laplace cofactor expansion along a row, `det_eq_finFoldl_laplace_row`:
 
-```lean
-theorem det_eq_finFoldl_laplace_row (M : Matrix R (n + 1) (n + 1)) (row : Fin (n + 1)) :
+```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)) :
     det M =
       Fin.foldl (n + 1)
         (fun acc col => acc + M[row][col] * cofactor M row col) 0
@@ -86,8 +89,9 @@ 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 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)
     (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 c0c8937ba..a682bf40e 100644
--- a/HexDeterminantMathlib/README.md
+++ b/HexDeterminantMathlib/README.md
@@ -70,7 +70,7 @@ Desnanot-Jacobi.
 The determinant correspondence is fully proven over a `CommRing`. The
 headline theorem identifies the two determinants:
 
-```lean
+```lean recall HexMatrixMathlib.det_eq
 theorem det_eq [CommRing R] (M : Hex.Matrix R n n) :
     Hex.Matrix.det M = Matrix.det (matrixEquiv M)
 ```
@@ -79,7 +79,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 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))
@@ -92,7 +92,7 @@ theorem det_plucker_three_term
 
 The Desnanot-Jacobi identity over Mathlib matrices:
 
-```lean
+```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 7feb61483..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
+```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,10 +87,9 @@ 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
-def fieldOfDegreePos (hdeg : 0 < f.degree) : Lean.Grind.Field (GF2nPoly f hirr)
-
-theorem isCharPOfDegreePos (hdeg : 0 < f.degree) :
+```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 e8e7aa613..b2925d2a6 100644
--- a/HexGF2Mathlib/README.md
+++ b/HexGF2Mathlib/README.md
@@ -75,6 +75,10 @@ The equivalences are the content. The packed polynomial representation
 corresponds to the generic one, and composing reaches Mathlib:
 
 ```lean
+import HexGF2Mathlib
+
+open Hex
+
 def equiv : Hex.GF2Poly ≃+* Hex.FpPoly 2
 
 noncomputable def equivPolynomial : Hex.GF2Poly ≃+* Polynomial (ZMod 2)
@@ -92,20 +96,16 @@ recursive Bezout theorem with the executable packed gcd.
 
 The single-word wrapper, in namespace `HexGF2Mathlib.GF2n`:
 
-```lean
-def equiv : Hex.GF2n n irr hn hn64 hirr ≃+*
-    GenericFiniteField (n := n) (irr := irr) (hn := hn) (hn64 := hn64) (hirr := hirr)
-
-theorem fintype_card :
+```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
 ```
 
 The arbitrary-degree wrapper, in namespace `HexGF2Mathlib.GF2nPoly`:
 
-```lean
-def equiv : Hex.GF2nPoly f hirr ≃+* GenericFiniteField (f := f) (hirr := hirr) (hdeg := hdeg)
-
-theorem fintype_card :
+```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/HexGFq/README.md b/HexGFq/README.md
index 7e28c65f6..790de68ec 100644
--- a/HexGFq/README.md
+++ b/HexGFq/README.md
@@ -73,6 +73,10 @@ The field type is built directly from the Conway table's proofs, so a `GFq`
 that elaborates is a field:
 
 ```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)
@@ -92,6 +96,10 @@ 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
+import HexGFq
+
+open Hex Hex.GFq Hex.Conway
+
 class PackedGF2Entry (n : Nat) where
   entry : SupportedEntry 2 n
   lower : UInt64
diff --git a/HexGFqField/README.md b/HexGFqField/README.md
index 415ab27a2..2970894c2 100644
--- a/HexGFqField/README.md
+++ b/HexGFqField/README.md
@@ -71,8 +71,9 @@ example : frob α = α ^ 5 := frob_eq_pow α
 The field laws are proved, not asserted. Inverse cancellation is the result the
 rest rests on:
 
-```lean
+```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}
     {x : FiniteField f hf hp hirr} (hx : x ≠ 0) :
     x * x⁻¹ = 1
@@ -85,6 +86,10 @@ already carries both the irreducibility proof and the positive-degree
 hypothesis:
 
 ```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 db4249fe0..725480462 100644
--- a/HexGFqMathlib/README.md
+++ b/HexGFqMathlib/README.md
@@ -70,11 +70,9 @@ 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
-noncomputable instance field :
-    Field (Hex.GFqField.FiniteField f hf hp hirr)
-
-theorem fintype_card_eq_pow (h : Hex.Conway.SupportedEntry p n) :
+```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
 ```
 
@@ -88,7 +86,12 @@ that the two counts agree, so it needs `Fact p.Prime` and `n ≠ 0` as
 hypotheses, neither of which the executable side carries:
 
 ```lean
-noncomputable def equivGaloisField [Fact p.Prime]
+import HexGFqMathlib
+
+open Hex
+
+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)
 ```
@@ -98,6 +101,10 @@ built on hex-gf2-mathlib's `GF2n.equiv` and computable, the second inheriting
 the choice `ringEquivOfCardEq` makes:
 
 ```lean
+import HexGFqMathlib
+
+open Hex
+
 def equivGFq : RingEquiv (GF2q n) (GFq 2 n h.entry)
 
 noncomputable def equivGaloisField : RingEquiv (GF2q n) (GaloisField 2 n)
@@ -107,6 +114,10 @@ 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
+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 83909da32..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
+```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
+```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 ce8aebd23..a212893ef 100644
--- a/HexGramSchmidtMathlib/README.md
+++ b/HexGramSchmidtMathlib/README.md
@@ -62,7 +62,7 @@ The proof-facing API splits into three parts.
 The rowwise correspondence with Mathlib's orthogonalization is fully
 proven. Over the rationals:
 
-```lean
+```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
@@ -70,7 +70,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 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
@@ -79,7 +79,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 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 =
@@ -89,7 +89,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 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 3fc72b996..2ab4b7c07 100644
--- a/HexMatrixMathlib/README.md
+++ b/HexMatrixMathlib/README.md
@@ -69,10 +69,14 @@ The headline equivalence sends each matrix to the Mathlib matrix with the
 same entries:
 
 ```lean
+import HexMatrixMathlib
+
+open Hex HexMatrixMathlib
+
 def matrixEquiv : Hex.Matrix R n m ≃ Matrix (Fin n) (Fin m) R
 ```
 
-```lean
+```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]
 ```
@@ -80,22 +84,24 @@ 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
-theorem matrixEquiv_rowSwap (M : Hex.Matrix R n m) (i j : Fin n) :
+```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
 ```
 
 A row addition is left multiplication by `Matrix.transvection`:
 
-```lean
-theorem matrixEquiv_rowAdd (M : Hex.Matrix R n m) (src dst : Fin n) (c : R) :
+```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) =
       Matrix.transvection dst src c * matrixEquiv M
 ```
 
 The matrix-vector product transports to Mathlib's `Matrix.mulVec`:
 
-```lean
+```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 9842e7bb0..9ed6fba8f 100644
--- a/HexMvPoly/README.md
+++ b/HexMvPoly/README.md
@@ -64,8 +64,10 @@ recursive-view laws.
 
 A product coefficient is the convolution over every monomial split:
 
-```lean
-theorem coeff_mul [Lean.Grind.Semiring R] [DecidableEq R]
+```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]
     (m : Mono n) (p q : MvPoly n R cmp) :
     coeff m (p * q) =
       (Mono.splits m).foldl
@@ -74,8 +76,9 @@ theorem coeff_mul [Lean.Grind.Semiring R] [DecidableEq R]
 
 Sparse Horner evaluation agrees with direct evaluation:
 
-```lean
-theorem evalHorner_eq [Lean.Grind.CommSemiring R]
+```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) :
     evalHorner x p = eval x p
 ```
diff --git a/HexMvPolyMathlib/README.md b/HexMvPolyMathlib/README.md
index 92ad256ce..54da50029 100644
--- a/HexMvPolyMathlib/README.md
+++ b/HexMvPolyMathlib/README.md
@@ -58,14 +58,23 @@ example (p q : P) :
 The correspondence is fully proven in both directions:
 
 ```lean
-def equiv [CommSemiring R] [DecidableEq R] :
+import HexMvPolyMathlib
+
+open Hex Hex.MvPoly HexMvPolyMathlib
+open scoped HexMvPolyMathlib
+
+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
-theorem coeff_toMvPolynomial [CommSemiring R] [DecidableEq R]
+```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]
     (m : Mono n) (p : MvPoly n R cmp) :
     MvPolynomial.coeff (monoEquiv m) (toMvPolynomial p) =
       coeff m p
@@ -73,8 +82,11 @@ theorem coeff_toMvPolynomial [CommSemiring R] [DecidableEq R]
 
 Executable evaluation is Mathlib algebra evaluation after conversion:
 
-```lean
-theorem aeval_apply [CommSemiring R] [DecidableEq R]
+```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]
+    [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 31126228a..70cb16ccd 100644
--- a/HexPolyFpMathlib/README.md
+++ b/HexPolyFpMathlib/README.md
@@ -53,7 +53,10 @@ polynomials and Mathlib's:
 The headline result is the ring equivalence:
 
 ```lean
-def fpPolyEquiv : Hex.FpPoly p ≃+* Polynomial (ZMod p)
+import HexPolyFpMathlib
+
+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/HexRealRootsMathlib/README.md b/HexRealRootsMathlib/README.md
index d95edb14d..848a0ea0a 100644
--- a/HexRealRootsMathlib/README.md
+++ b/HexRealRootsMathlib/README.md
@@ -44,6 +44,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/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..a3276c94f 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.
 
@@ -58,27 +58,36 @@ 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
-theorem rowReduce_isRowReduced (M : Matrix R n m) : IsRowReduced M (rowReduce M)
+```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)
 ```
 
 The row-span wrappers are sound, with `spanCoeffs_sound`:
 
-```lean
-theorem spanCoeffs_sound [Lean.Grind.Field R] [DecidableEq R]
+```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) :
-    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
-theorem nullspace_sound [Lean.Grind.Field R] [DecidableEq R] (M : Matrix R n m)
+```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
+```
 
-theorem nullspace_complete [Lean.Grind.Field R] [DecidableEq R] (M : Matrix R n m)
+```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)
     (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 f84038c70..bb93e5d08 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 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
+```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
+```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/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
 ```
 
diff --git a/SPEC/readme.md b/SPEC/readme.md
index c52c26c4e..852536c65 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,22 @@ 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 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.
+
+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
@@ -59,6 +74,9 @@ Use these five level-1 headings, in this order.
 `<Lib>/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 d7675a65d..baa97c4e3 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -21,6 +21,16 @@
    "inputRev": "master",
    "inherited": false,
    "configFile": "lakefile.toml"},
+  {"url": "https://github.com/kim-em/lean-readme.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "2a286f42701c22dffafc9d2ff3222f8d3ac4994a",
+   "name": "«lean-readme»",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "2a286f42701c22dffafc9d2ff3222f8d3ac4994a",
+   "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 5324f2a8c..cf58f84d7 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.34.0-rc2"
 
+require «lean-readme» from git
+  "https://github.com/kim-em/lean-readme.git" @
+    "2a286f42701c22dffafc9d2ff3222f8d3ac4994a"
+
 require «lean-bench» from git
   "https://github.com/kim-em/lean-bench.git" @ "master"
 
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."
+}
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."
+}