diff --git a/research/cyclic-schur-lean/AXIOMS.txt b/research/cyclic-schur-lean/AXIOMS.txt
new file mode 100644
index 0000000000..3809670745
--- /dev/null
+++ b/research/cyclic-schur-lean/AXIOMS.txt
@@ -0,0 +1,105 @@
+Lean (version 4.21.0, arm64-apple-darwin23.6.0, commit 6741444a63ee, Release)
+AXIOMS CyclicSchur.Controls.data8.eq_1: []
+AXIOMS CyclicSchur.Controls.data8.eq_2: []
+AXIOMS CyclicSchur.Controls.data8.eq_3: []
+AXIOMS CyclicSchur.Controls.data8.eq_4: []
+AXIOMS CyclicSchur.Controls.data8.eq_5: []
+AXIOMS CyclicSchur.Controls.data8.eq_6: []
+AXIOMS CyclicSchur.Controls.data8.eq_7: []
+AXIOMS CyclicSchur.Controls.data8.eq_8: []
+AXIOMS CyclicSchur.Controls.ends8.eq_1: []
+AXIOMS CyclicSchur.Controls.missing_start_factor_rejected: [propext, Quot.sound]
+AXIOMS CyclicSchur.Controls.reference_closure: [propext, Quot.sound]
+AXIOMS CyclicSchur.Controls.reference_closure._proof_1_3: [propext, Quot.sound]
+AXIOMS CyclicSchur.Controls.reference_solution: [propext]
+AXIOMS CyclicSchur.Controls.solution8.eq_1: []
+AXIOMS CyclicSchur.Controls.stale_predecessor_rejected: [propext, Quot.sound]
+AXIOMS CyclicSchur.Controls.two.eq_1: []
+AXIOMS CyclicSchur.Controls.wrong_child_sign_rejected: [propext, Quot.sound]
+AXIOMS CyclicSchur.Controls.wrong_tail_rejected: [propext, Quot.sound]
+AXIOMS CyclicSchur.IsSolution.eq_1: []
+AXIOMS CyclicSchur.chain._unary._proof_1: []
+AXIOMS CyclicSchur.chain._unary._proof_2: [propext, Quot.sound]
+AXIOMS CyclicSchur.chain._unary.eq_def: [propext, Quot.sound]
+AXIOMS CyclicSchur.chain.eq_1: [propext, Quot.sound]
+AXIOMS CyclicSchur.chain.eq_def: [propext, Quot.sound]
+AXIOMS CyclicSchur.chainProduct._proof_1: []
+AXIOMS CyclicSchur.chainProduct._proof_2: [propext, Quot.sound]
+AXIOMS CyclicSchur.chainProduct.eq_1: [propext, Quot.sound]
+AXIOMS CyclicSchur.chainProduct.eq_def: [propext, Quot.sound]
+AXIOMS CyclicSchur.chain_affine: [propext, Quot.sound]
+AXIOMS CyclicSchur.chain_affine._proof_1_5: [propext, Quot.sound]
+AXIOMS CyclicSchur.childCoefficient.eq_1: [propext, Quot.sound]
+AXIOMS CyclicSchur.childData.eq_1: [propext, Quot.sound]
+AXIOMS CyclicSchur.childStride.eq_1: []
+AXIOMS CyclicSchur.childStride_lt: [propext]
+AXIOMS CyclicSchur.child_predecessor: [propext, Quot.sound]
+AXIOMS CyclicSchur.child_predecessor._proof_1_2: [propext, Quot.sound]
+AXIOMS CyclicSchur.child_predecessor._proof_1_3: [propext, Quot.sound]
+AXIOMS CyclicSchur.closure_is_child_system: [propext, Quot.sound]
+AXIOMS CyclicSchur.closure_reconstruct: [propext, Quot.sound]
+AXIOMS CyclicSchur.closure_reconstruct_tail: [propext, Quot.sound]
+AXIOMS CyclicSchur.endpoint.eq_1: []
+AXIOMS CyclicSchur.endpoint_lt: [propext, Quot.sound]
+AXIOMS CyclicSchur.endpoint_lt._proof_1_1: [propext, Quot.sound]
+AXIOMS CyclicSchur.endpoint_mod: [propext, Quot.sound]
+AXIOMS CyclicSchur.endpoint_mod._proof_1_1: [propext, Quot.sound]
+AXIOMS CyclicSchur.forward._proof_1: []
+AXIOMS CyclicSchur.forward._proof_2: [propext, Quot.sound]
+AXIOMS CyclicSchur.forward.eq_1: [propext, Quot.sound]
+AXIOMS CyclicSchur.forward.eq_def: [propext, Quot.sound]
+AXIOMS CyclicSchur.forward_affine: [propext, Quot.sound]
+AXIOMS CyclicSchur.forward_eq_chain: [propext, Quot.sound]
+AXIOMS CyclicSchur.forward_eq_chain._proof_1_3: [propext, Quot.sound]
+AXIOMS CyclicSchur.forward_eq_chain._proof_1_4: [propext, Quot.sound]
+AXIOMS CyclicSchur.forward_pair: [propext, Quot.sound]
+AXIOMS CyclicSchur.forward_pair._proof_1_5: [propext, Quot.sound]
+AXIOMS CyclicSchur.pairStep.eq_1: []
+AXIOMS CyclicSchur.passA.eq_1: [Quot.sound, propext]
+AXIOMS CyclicSchur.passA_correct: [Quot.sound, propext, Classical.choice]
+AXIOMS CyclicSchur.passA_tail_correct: [Quot.sound, propext, Classical.choice]
+AXIOMS CyclicSchur.passC.eq_1: []
+AXIOMS CyclicSchur.passC_correct: [propext, Quot.sound, Classical.choice]
+AXIOMS CyclicSchur.passC_solves_parent: [propext, Quot.sound, Classical.choice]
+AXIOMS CyclicSchur.passC_solves_parent._proof_1_1: [propext, Quot.sound]
+AXIOMS CyclicSchur.predecessor.eq_1: []
+AXIOMS CyclicSchur.predecessor_lt: [propext, Quot.sound]
+AXIOMS CyclicSchur.predecessor_lt._proof_1_2: [propext, Quot.sound]
+AXIOMS CyclicSchur.predecessor_lt._proof_1_3: [propext, Quot.sound]
+AXIOMS CyclicSchur.predecessor_mod: [propext, Quot.sound]
+AXIOMS CyclicSchur.predecessor_mod._proof_1_2: [propext, Quot.sound]
+AXIOMS CyclicSchur.predecessor_mod._proof_1_3: [propext, Quot.sound]
+AXIOMS CyclicSchur.predecessor_mod._proof_1_4: [propext, Quot.sound]
+AXIOMS CyclicSchur.predecessor_mod._proof_1_5: [propext, Quot.sound]
+AXIOMS CyclicSchur.reconstruct.eq_1: [propext, Quot.sound]
+AXIOMS CyclicSchur.scalarStep.eq_1: []
+AXIOMS CyclicSchur.scalar_closure: [propext, Quot.sound]
+AXIOMS CyclicSchur.scalar_exists_iff: [propext, Quot.sound]
+AXIOMS CyclicSchur.scalar_is_solution: [propext, Quot.sound]
+AXIOMS CyclicSchur.scalar_reconstruct: [propext, Quot.sound]
+AXIOMS CyclicSchur.scalar_reconstruct_tail: [propext, Quot.sound]
+AXIOMS CyclicSchur.scalar_schur_iff: [propext, Quot.sound]
+AXIOMS CyclicSchur.scanPass.eq_1: []
+AXIOMS CyclicSchur.scanPass.eq_2: []
+AXIOMS CyclicSchur.scanPass_prefix: [propext, Quot.sound, Classical.choice]
+AXIOMS CyclicSchur.scanPass_prefix._proof_1_1: [propext, Quot.sound]
+AXIOMS CyclicSchur.scanPass_prefix._proof_1_6: [propext, Quot.sound]
+AXIOMS CyclicSchur.scanPass_prefix._proof_1_7: [propext, Quot.sound]
+AXIOMS CyclicSchur.scanPass_suffix: [propext, Quot.sound]
+AXIOMS CyclicSchur.scanPass_suffix._proof_1_1: [propext, Quot.sound]
+AXIOMS CyclicSchur.scanPass_suffix._proof_1_5: [propext, Quot.sound]
+AXIOMS CyclicSchur.schur_iff: [propext, Quot.sound]
+AXIOMS CyclicSchur.solution_reconstruct: [propext, Quot.sound]
+AXIOMS CyclicSchur.solution_reconstruct._proof_1_5: [propext, Quot.sound]
+AXIOMS CyclicSchur.solution_reconstruct._proof_1_6: [propext, Quot.sound]
+AXIOMS CyclicSchur.solution_restrict: [propext, Quot.sound]
+AXIOMS CyclicSchur.solutions_eq_iff_tails: [propext, Quot.sound]
+AXIOMS CyclicSchur.sub_stride_mod: [propext, Quot.sound]
+AXIOMS CyclicSchur.sub_stride_mod._proof_1_1: [propext, Quot.sound]
+AXIOMS CyclicSchur.tail.eq_1: []
+AXIOMS CyclicSchur.zeroSeed._proof_1: []
+AXIOMS CyclicSchur.zeroSeed._proof_2: [propext, Quot.sound]
+AXIOMS CyclicSchur.zeroSeed.eq_1: [propext, Quot.sound]
+AXIOMS CyclicSchur.zeroSeed.eq_def: [propext, Quot.sound]
+PASS_CYCLIC_SCHUR: 102 theorems; standard axioms only
+PASS_AUDIT_GUARDS: incomplete proof and package axiom rejected
diff --git a/research/cyclic-schur-lean/Audit.lean b/research/cyclic-schur-lean/Audit.lean
new file mode 100644
index 0000000000..8158ecfe82
--- /dev/null
+++ b/research/cyclic-schur-lean/Audit.lean
@@ -0,0 +1,28 @@
+import Lean
+import CyclicSchur
+import Counterexamples
+
+open Lean Elab Command
+
+/- Check every theorem in the package namespace, including equation lemmas. -/
+def CyclicSchurAudit.check : CommandElabM Unit := do
+  let env ← getEnv
+  let mut names : Array Name := #[]
+  for (name, _) in env.constants do
+    if (`CyclicSchur).isPrefixOf name then
+      if getOriginalConstKind? env name == some .axiom then
+        throwError "Package declares an axiom: {name}"
+      if getOriginalConstKind? env name == some .thm then
+        names := names.push name
+  if names.isEmpty then
+    throwError "No package theorems were found"
+  let allowed := #[`propext, `Classical.choice, `Quot.sound]
+  for name in names.qsort (fun a b => a.toString < b.toString) do
+    let axioms ← collectAxioms name
+    for axiomName in axioms do
+      unless allowed.contains axiomName do
+        throwError "Disallowed axiom in {name}: {axiomName}"
+    logInfo m!"AXIOMS {name}: {axioms.toList}"
+  logInfo m!"PASS_CYCLIC_SCHUR: {names.size} theorems; standard axioms only"
+
+run_cmd CyclicSchurAudit.check
diff --git a/research/cyclic-schur-lean/Counterexamples.lean b/research/cyclic-schur-lean/Counterexamples.lean
new file mode 100644
index 0000000000..68cf634de9
--- /dev/null
+++ b/research/cyclic-schur-lean/Counterexamples.lean
@@ -0,0 +1,71 @@
+import CyclicSchur
+import Init.Grind.CommRing.Int
+
+/- The examples below reject index and coefficient errors in the exact reduction. -/
+namespace CyclicSchur.Controls
+
+def data8 (i : Nat) : Int :=
+  match i with
+  | 0 => -11
+  | 1 => -12
+  | 2 => -13
+  | 3 => 2
+  | 4 => 1
+  | 5 => 0
+  | 6 => -1
+  | _ => -2
+
+def two (_ : Nat) : Int := 2
+def solution8 (i : Nat) : Int := i + 1
+def ends8 (k : Nat) : Int := k + 6
+
+theorem reference_solution : ScalarSolution 8 3 data8 two solution8 := by
+  have h : ∀ i : Fin 8, solution8 i = data8 i + two i * solution8 ((i + 8 - 3) % 8) :=
+    by decide
+  intro i hi
+  exact h ⟨i, hi⟩
+
+theorem reference_closure :
+    ScalarSolution 3 (childStride 8 3) (childData 8 3 (by decide) data8 two)
+      (childCoefficient 8 3 (by decide) two) ends8 := by
+  have h := ((scalar_schur_iff (by decide : 0 < 3) (by decide : 3 ≤ 8)
+    data8 two solution8).mp reference_solution).1
+  have he : tail 8 3 solution8 = ends8 := by
+    funext k
+    simp only [tail, endpoint, solution8, ends8]
+    omega
+  rw [he] at h
+  exact h
+
+/- The positive remainder gives stride two. The correct child stride is one. -/
+theorem wrong_child_sign_rejected :
+    ¬ ScalarSolution 3 (8 % 3) (childData 8 3 (by decide) data8 two)
+      (childCoefficient 8 3 (by decide) two) ends8 := by
+  intro h
+  have bad := h 0 (by decide)
+  simp [ends8, childData, childCoefficient, zeroSeed, chainProduct, endpoint, data8, two] at bad
+
+/- Starting the tail one entry early changes the closure right-hand side. -/
+theorem wrong_tail_rejected :
+    ¬ ScalarSolution 3 (childStride 8 3)
+      (fun k => zeroSeed 3 (by decide) data8 two (8 - 3 - 1 + k))
+      (fun k => chainProduct 3 (by decide) two (8 - 3 - 1 + k)) ends8 := by
+  intro h
+  have bad := h 0 (by decide)
+  simp [ends8, childStride, zeroSeed, chainProduct, data8, two] at bad
+
+/- A chain product includes the coefficient at the chain start. -/
+theorem missing_start_factor_rejected :
+    ¬ ScalarSolution 3 (childStride 8 3) (childData 8 3 (by decide) data8 two)
+      (fun k => chainProduct 3 (by decide) two (endpoint 8 3 k) / 2) ends8 := by
+  intro h
+  have bad := h 0 (by decide)
+  simp [ends8, childStride, childData, childCoefficient, zeroSeed, chainProduct,
+    endpoint, data8, two] at bad
+
+/- A source pass must read the updated predecessor. -/
+theorem stale_predecessor_rejected :
+    data8 6 + two 6 * data8 (6 - 3) ≠ zeroSeed 3 (by decide) data8 two 6 := by
+  simp [data8, two, zeroSeed]
+
+end CyclicSchur.Controls
diff --git a/research/cyclic-schur-lean/CyclicSchur.lean b/research/cyclic-schur-lean/CyclicSchur.lean
new file mode 100644
index 0000000000..d34fc8dfa5
--- /dev/null
+++ b/research/cyclic-schur-lean/CyclicSchur.lean
@@ -0,0 +1,365 @@
+import Std
+import Init.Grind.CommRing.Basic
+
+set_option autoImplicit false
+
+/-!
+The exact chain and closure steps in PR846 and PR985.
+The indices are natural numbers. Only entries below the stated length are used.
+-/
+
+namespace CyclicSchur
+
+universe u
+variable {α : Type u}
+
+def predecessor (n w i : Nat) : Nat :=
+  if i < w then n - w + i else i - w
+
+def endpoint (n w k : Nat) : Nat := n - w + k
+
+def tail (n w : Nat) (y : Nat → α) : Nat → α :=
+  fun k => y (endpoint n w k)
+
+def chain (w : Nat) (hw : 0 < w) (f : Nat → α → α) (i : Nat) (t : α) : α :=
+  if i < w then f i t else f i (chain w hw f (i - w) t)
+termination_by i
+decreasing_by omega
+
+def forward (w : Nat) (hw : 0 < w) (f : Nat → α → α)
+    (seed : Nat → α) (i : Nat) : α :=
+  if i < w then f i (seed i) else f i (forward w hw f seed (i - w))
+termination_by i
+decreasing_by omega
+
+def IsSolution (n w : Nat) (f : Nat → α → α) (y : Nat → α) : Prop :=
+  ∀ i, i < n → y i = f i (y (predecessor n w i))
+
+def IsClosure (n w : Nat) (hw : 0 < w) (f : Nat → α → α)
+    (Y : Nat → α) : Prop :=
+  ∀ k, k < w → Y k = chain w hw f (endpoint n w k) (Y ((k + n) % w))
+
+theorem predecessor_lt {n w i : Nat} (hw : w ≤ n) (hi : i < n) :
+    predecessor n w i < n := by
+  simp only [predecessor]
+  split <;> omega
+
+theorem predecessor_mod {n w i : Nat} (hw : w ≤ n) (hi : i < n) :
+    predecessor n w i = (i + n - w) % n := by
+  by_cases h : i < w
+  · rw [predecessor, if_pos h, Nat.mod_eq_of_lt (by omega)]
+    omega
+  · have he : i + n - w = n + (i - w) := by omega
+    rw [predecessor, if_neg h, he, Nat.add_mod_left,
+      Nat.mod_eq_of_lt (by omega)]
+
+theorem endpoint_lt {n w k : Nat} (hw : w ≤ n) (hk : k < w) :
+    endpoint n w k < n := by
+  unfold endpoint
+  omega
+
+theorem endpoint_mod {n w k : Nat} (hw : w ≤ n) :
+    endpoint n w k % w = (k + n) % w := by
+  have he : k + n = endpoint n w k + w := by unfold endpoint; omega
+  rw [he, Nat.add_mod_right]
+
+theorem sub_stride_mod {w i : Nat} (h : w ≤ i) :
+    (i - w) % w = i % w := by
+  have he : i = (i - w) + w := by omega
+  conv => rhs; rw [he, Nat.add_mod_right]
+
+theorem forward_eq_chain (w : Nat) (hw : 0 < w) (f : Nat → α → α)
+    (seed : Nat → α) (i : Nat) :
+    forward w hw f seed i = chain w hw f i (seed (i % w)) := by
+  induction i using Nat.strongRecOn with
+  | ind i ih =>
+    rw [forward, chain]
+    by_cases hi : i < w
+    · simp only [if_pos hi, Nat.mod_eq_of_lt hi]
+    · simp only [if_neg hi]
+      rw [ih (i - w) (by omega), sub_stride_mod (by omega)]
+
+theorem solution_reconstruct {n w : Nat} (hw : 0 < w)
+    {f : Nat → α → α} {y : Nat → α} (hy : IsSolution n w f y)
+    (i : Nat) (hi : i < n) :
+    y i = forward w hw f (tail n w y) i := by
+  induction i using Nat.strongRecOn with
+  | ind i ih =>
+    rw [hy i hi, forward]
+    by_cases hs : i < w
+    · simp only [if_pos hs, predecessor, tail, endpoint]
+    · simp only [if_neg hs, predecessor]
+      rw [ih (i - w) (by omega) (by omega)]
+
+theorem solution_restrict {n w : Nat} (hw : 0 < w) (hwn : w ≤ n)
+    {f : Nat → α → α} {y : Nat → α} (hy : IsSolution n w f y) :
+    IsClosure n w hw f (tail n w y) := by
+  intro k hk
+  change y (endpoint n w k) = _
+  rw [solution_reconstruct hw hy _ (endpoint_lt hwn hk),
+    forward_eq_chain, endpoint_mod hwn]
+
+theorem closure_reconstruct_tail {n w : Nat} (hw : 0 < w) (hwn : w ≤ n)
+    {f : Nat → α → α} {Y : Nat → α} (hY : IsClosure n w hw f Y)
+    (k : Nat) (hk : k < w) :
+    tail n w (forward w hw f Y) k = Y k := by
+  unfold tail
+  rw [forward_eq_chain, endpoint_mod hwn]
+  exact (hY k hk).symm
+
+theorem closure_reconstruct {n w : Nat} (hw : 0 < w) (hwn : w ≤ n)
+    {f : Nat → α → α} {Y : Nat → α} (hY : IsClosure n w hw f Y) :
+    IsSolution n w f (forward w hw f Y) := by
+  intro i hi
+  rw [forward]
+  by_cases hs : i < w
+  · simp only [if_pos hs, predecessor]
+    exact congrArg (f i) (closure_reconstruct_tail hw hwn hY i hs).symm
+  · simp only [if_neg hs, predecessor]
+
+theorem schur_iff {n w : Nat} (hw : 0 < w) (hwn : w ≤ n)
+    (f : Nat → α → α) (y : Nat → α) :
+    IsSolution n w f y ↔
+      IsClosure n w hw f (tail n w y) ∧
+      ∀ i, i < n → y i = forward w hw f (tail n w y) i := by
+  constructor
+  · intro hy
+    exact ⟨solution_restrict hw hwn hy, solution_reconstruct hw hy⟩
+  · rintro ⟨hY, hr⟩
+    have hs := closure_reconstruct hw hwn hY
+    intro i hi
+    rw [hr i hi, hs i hi, ← hr _ (predecessor_lt hwn hi)]
+
+/- The normalized child stride is the natural-number form of (-n) mod w. -/
+def childStride (n w : Nat) : Nat := (w - n % w) % w
+
+theorem childStride_lt {n w : Nat} (hw : 0 < w) : childStride n w < w :=
+  Nat.mod_lt _ hw
+
+theorem child_predecessor {n w k : Nat} (hw : 0 < w) (hk : k < w) :
+    predecessor w (childStride n w) k = (k + n) % w := by
+  rw [predecessor_mod (Nat.le_of_lt (childStride_lt hw)) hk]
+  have hr : n % w < w := Nat.mod_lt n hw
+  by_cases hz : n % w = 0
+  · simp only [childStride, hz, Nat.sub_zero, Nat.mod_self, Nat.sub_zero,
+      Nat.add_mod_right]
+    rw [Nat.add_mod, hz, Nat.add_zero, Nat.mod_mod]
+  · have hc : w - n % w < w := by omega
+    simp only [childStride, Nat.mod_eq_of_lt hc]
+    have he : k + w - (w - n % w) = k + n % w := by omega
+    rw [he, Nat.add_mod k n w, Nat.mod_eq_of_lt hk]
+
+theorem closure_is_child_system {n w : Nat} (hw : 0 < w)
+    (f : Nat → α → α) (Y : Nat → α) :
+    IsClosure n w hw f Y ↔
+      IsSolution w (childStride n w) (fun k => chain w hw f (endpoint n w k)) Y := by
+  constructor <;> intro h k hk
+  · simpa only [child_predecessor hw hk] using h k hk
+  · simpa only [child_predecessor hw hk] using h k hk
+
+/- Each step writes one entry. The lagged read uses the current array. -/
+def scanPass (w : Nat) (f : Nat → α → α) (seed initial : Nat → α) :
+    Nat → Nat → α
+  | 0 => initial
+  | count + 1 => fun i =>
+      if i = count then
+        f count (if count < w then seed count
+          else scanPass w f seed initial count (count - w))
+      else scanPass w f seed initial count i
+
+theorem scanPass_prefix {w : Nat} (hw : 0 < w) (f : Nat → α → α)
+    (seed initial : Nat → α) (count i : Nat) (hi : i < count) :
+    scanPass w f seed initial count i = forward w hw f seed i := by
+  induction count generalizing i with
+  | zero => omega
+  | succ count ih =>
+    by_cases he : i = count
+    · subst i
+      simp only [scanPass, if_pos rfl, ite_true]
+      rw [forward]
+      by_cases hs : count < w
+      · simp only [if_pos hs]
+      · simp only [if_neg hs]
+        rw [ih (count - w) (by omega)]
+    · simp only [scanPass, if_neg he]
+      exact ih i (by omega)
+
+theorem scanPass_suffix (w : Nat) (f : Nat → α → α)
+    (seed initial : Nat → α) (count i : Nat) (hi : count ≤ i) :
+    scanPass w f seed initial count i = initial i := by
+  induction count with
+  | zero => rfl
+  | succ count ih =>
+    have he : i ≠ count := by omega
+    simp only [scanPass, if_neg he]
+    exact ih (by omega)
+
+section Scalar
+
+open Lean.Grind
+
+variable {R : Type u} [Semiring R]
+
+def scalarStep (x b : Nat → R) (i : Nat) (t : R) : R := x i + b i * t
+
+def zeroSeed (w : Nat) (hw : 0 < w) (x b : Nat → R) (i : Nat) : R :=
+  if i < w then x i else x i + b i * zeroSeed w hw x b (i - w)
+termination_by i
+decreasing_by omega
+
+def chainProduct (w : Nat) (hw : 0 < w) (b : Nat → R) (i : Nat) : R :=
+  if i < w then b i else b i * chainProduct w hw b (i - w)
+termination_by i
+decreasing_by omega
+
+theorem chain_affine (w : Nat) (hw : 0 < w) (x b : Nat → R) (i : Nat) (t : R) :
+    chain w hw (scalarStep x b) i t =
+      zeroSeed w hw x b i + chainProduct w hw b i * t := by
+  induction i using Nat.strongRecOn with
+  | ind i ih =>
+    rw [chain, zeroSeed, chainProduct]
+    by_cases hi : i < w
+    · simp only [if_pos hi, scalarStep]
+    · simp only [if_neg hi, scalarStep]
+      rw [ih (i - w) (by omega), Semiring.left_distrib,
+        ← Semiring.mul_assoc, Semiring.add_assoc]
+
+theorem forward_affine (w : Nat) (hw : 0 < w) (x b seed : Nat → R) (i : Nat) :
+    forward w hw (scalarStep x b) seed i =
+      zeroSeed w hw x b i + chainProduct w hw b i * seed (i % w) := by
+  rw [forward_eq_chain, chain_affine]
+
+def pairStep (x b : Nat → R) (i : Nat) (v : R × R) : R × R :=
+  (x i + b i * v.1, b i * v.2)
+
+theorem forward_pair (w : Nat) (hw : 0 < w) (x b : Nat → R) (i : Nat) :
+    forward w hw (pairStep x b) (fun _ => (0, 1)) i =
+      (zeroSeed w hw x b i, chainProduct w hw b i) := by
+  induction i using Nat.strongRecOn with
+  | ind i ih =>
+    rw [forward, zeroSeed, chainProduct]
+    by_cases hi : i < w
+    · simp only [if_pos hi, pairStep, Semiring.mul_zero,
+        Semiring.add_zero, Semiring.mul_one]
+    · simp only [if_neg hi]
+      rw [ih (i - w) (by omega)]
+      rfl
+
+/- These are the exact scalar operations in the two source loops. -/
+def passA (n w : Nat) (x b : Nat → R) (initial : Nat → R × R) : Nat → R × R :=
+  scanPass w (pairStep x b) (fun _ => (0, 1)) initial n
+
+def passC (n w : Nat) (x b Y initial : Nat → R) : Nat → R :=
+  scanPass w (scalarStep x b) Y initial n
+
+theorem passA_correct {n w : Nat} (hw : 0 < w) (x b : Nat → R)
+    (initial : Nat → R × R) (i : Nat) (hi : i < n) :
+    passA n w x b initial i = (zeroSeed w hw x b i, chainProduct w hw b i) := by
+  rw [passA, scanPass_prefix hw _ _ _ _ _ hi, forward_pair]
+
+theorem passC_correct {n w : Nat} (hw : 0 < w) (x b Y initial : Nat → R)
+    (i : Nat) (hi : i < n) :
+    passC n w x b Y initial i =
+      zeroSeed w hw x b i + chainProduct w hw b i * Y (i % w) := by
+  rw [passC, scanPass_prefix hw _ _ _ _ _ hi, forward_affine]
+
+def ScalarSolution (n w : Nat) (x b y : Nat → R) : Prop :=
+  ∀ i, i < n → y i = x i + b i * y ((i + n - w) % n)
+
+def childData (n w : Nat) (hw : 0 < w) (x b : Nat → R) : Nat → R :=
+  fun k => zeroSeed w hw x b (endpoint n w k)
+
+def childCoefficient (n w : Nat) (hw : 0 < w) (b : Nat → R) : Nat → R :=
+  fun k => chainProduct w hw b (endpoint n w k)
+
+def reconstruct (w : Nat) (hw : 0 < w) (x b Y : Nat → R) (i : Nat) : R :=
+  zeroSeed w hw x b i + chainProduct w hw b i * Y (i % w)
+
+theorem scalar_is_solution {n w : Nat} (hwn : w ≤ n) (x b y : Nat → R) :
+    ScalarSolution n w x b y ↔ IsSolution n w (scalarStep x b) y := by
+  constructor <;> intro h i hi
+  · simpa only [scalarStep, predecessor_mod hwn hi] using h i hi
+  · simpa only [scalarStep, predecessor_mod hwn hi] using h i hi
+
+theorem scalar_closure {n w : Nat} (hw : 0 < w) (x b Y : Nat → R) :
+    IsClosure n w hw (scalarStep x b) Y ↔
+      ScalarSolution w (childStride n w) (childData n w hw x b)
+        (childCoefficient n w hw b) Y := by
+  rw [scalar_is_solution (Nat.le_of_lt (childStride_lt hw))]
+  constructor <;> intro h k hk
+  · simpa only [chain_affine, scalarStep, childData, childCoefficient,
+      child_predecessor hw hk] using h k hk
+  · simpa only [chain_affine, scalarStep, childData, childCoefficient,
+      child_predecessor hw hk] using h k hk
+
+/- This is the exact Schur identity with the indices used by solve. -/
+theorem scalar_schur_iff {n w : Nat} (hw : 0 < w) (hwn : w ≤ n)
+    (x b y : Nat → R) :
+    ScalarSolution n w x b y ↔
+      ScalarSolution w (childStride n w) (childData n w hw x b)
+        (childCoefficient n w hw b) (tail n w y) ∧
+      ∀ i, i < n → y i = reconstruct w hw x b (tail n w y) i := by
+  rw [scalar_is_solution hwn, schur_iff hw hwn, scalar_closure hw]
+  simp only [forward_affine, reconstruct]
+
+theorem scalar_reconstruct {n w : Nat} (hw : 0 < w) (hwn : w ≤ n)
+    {x b Y : Nat → R}
+    (hY : ScalarSolution w (childStride n w) (childData n w hw x b)
+      (childCoefficient n w hw b) Y) :
+    ScalarSolution n w x b (reconstruct w hw x b Y) := by
+  apply (scalar_is_solution hwn _ _ _).mpr
+  have hc := closure_reconstruct hw hwn ((scalar_closure hw x b Y).mpr hY)
+  simpa only [IsSolution, forward_affine, reconstruct] using hc
+
+theorem scalar_reconstruct_tail {n w : Nat} (hw : 0 < w) (hwn : w ≤ n)
+    {x b Y : Nat → R}
+    (hY : ScalarSolution w (childStride n w) (childData n w hw x b)
+      (childCoefficient n w hw b) Y) (k : Nat) (hk : k < w) :
+    tail n w (reconstruct w hw x b Y) k = Y k := by
+  have hc := closure_reconstruct_tail hw hwn ((scalar_closure hw x b Y).mpr hY) k hk
+  simpa only [tail, forward_affine, reconstruct] using hc
+
+theorem passC_solves_parent {n w : Nat} (hw : 0 < w) (hwn : w ≤ n)
+    {x b Y : Nat → R}
+    (hY : ScalarSolution w (childStride n w) (childData n w hw x b)
+      (childCoefficient n w hw b) Y) (initial : Nat → R) :
+    ScalarSolution n w x b (passC n w x b Y initial) := by
+  intro i hi
+  have hp : (i + n - w) % n < n := Nat.mod_lt _ (by omega)
+  rw [passC_correct hw _ _ _ _ _ hi, passC_correct hw _ _ _ _ _ hp]
+  exact scalar_reconstruct hw hwn hY i hi
+
+theorem passA_tail_correct {n w : Nat} (hw : 0 < w) (hwn : w ≤ n)
+    (x b : Nat → R) (initial : Nat → R × R) (k : Nat) (hk : k < w) :
+    passA n w x b initial (endpoint n w k) =
+      (childData n w hw x b k, childCoefficient n w hw b k) :=
+  passA_correct hw x b initial _ (endpoint_lt hwn hk)
+
+theorem scalar_exists_iff {n w : Nat} (hw : 0 < w) (hwn : w ≤ n)
+    (x b : Nat → R) :
+    (∃ y, ScalarSolution n w x b y) ↔
+      ∃ Y, ScalarSolution w (childStride n w) (childData n w hw x b)
+        (childCoefficient n w hw b) Y := by
+  constructor
+  · rintro ⟨y, hy⟩
+    exact ⟨tail n w y, ((scalar_schur_iff hw hwn x b y).mp hy).1⟩
+  · rintro ⟨Y, hY⟩
+    exact ⟨reconstruct w hw x b Y, scalar_reconstruct hw hwn hY⟩
+
+theorem solutions_eq_iff_tails {n w : Nat} (hw : 0 < w) (hwn : w ≤ n)
+    {x b y₁ y₂ : Nat → R} (h₁ : ScalarSolution n w x b y₁)
+    (h₂ : ScalarSolution n w x b y₂) :
+    (∀ i, i < n → y₁ i = y₂ i) ↔
+      ∀ k, k < w → tail n w y₁ k = tail n w y₂ k := by
+  constructor
+  · intro h k hk
+    exact h _ (endpoint_lt hwn hk)
+  · intro h i hi
+    rw [((scalar_schur_iff hw hwn x b y₁).mp h₁).2 i hi,
+      ((scalar_schur_iff hw hwn x b y₂).mp h₂).2 i hi]
+    unfold reconstruct
+    rw [h _ (Nat.mod_lt _ hw)]
+
+end Scalar
+
+end CyclicSchur
diff --git a/research/cyclic-schur-lean/FOLLOWUP-REVIEW.md b/research/cyclic-schur-lean/FOLLOWUP-REVIEW.md
new file mode 100644
index 0000000000..eb89b29974
--- /dev/null
+++ b/research/cyclic-schur-lean/FOLLOWUP-REVIEW.md
@@ -0,0 +1,74 @@
+# Exact statement and source-interface follow-up
+
+This review addresses the [PR #1026 triage request](https://github.com/CrocSwap/integer-mult-bounds/pull/1026#issuecomment-6161280106).
+The complete Lean source, its four mathematical controls and the axiom guard
+were reviewed. A fresh build passed on 2026-10-14. No proof correction was
+needed. This is a formalization of the exact reduction, with no new kappa.
+
+## Pins and fresh build
+
+Reviewed head: `c4be063c0afb634db7aa02bc1876ff29640bec65`.
+Refreshed main: `418e40eb2572d930b58c1cf9b82b41c0fc7ee08d`.
+Original base and source subjects remain those in `SOURCES.json`; no pin was
+changed to follow a moving PR head.
+
+```sh
+sh research/cyclic-schur-lean/verify.sh /path/to/lean-4.21.0/bin/lean
+```
+
+This command exited 0 with the official compiler commit
+`6741444a63eec253a7eae7a83f1beb3de015023d`. It used one Lean worker and a
+fresh temporary build. The theorem report matched `AXIOMS.txt` byte for byte.
+The final lines were:
+
+```text
+PASS_CYCLIC_SCHUR: 102 theorems; standard axioms only
+PASS_AUDIT_GUARDS: incomplete proof and package axiom rejected
+```
+
+The complete build-log SHA-256 was
+`47f3cb9bb50be35e0881d9361b2e2cc5f3c4cc78353b5d3529138dc474ace624`.
+No toolchain installation, dependency upgrade or shared cache change was
+needed. No root-wide or selected-supplier replay was run.
+
+## What the checked statement covers
+
+| Obligation | Checked statement | Boundary |
+| --- | --- | --- |
+| Parent index | `predecessor_mod` | Requires `w <= n` and an active index. |
+| Closure tail and stride | `endpoint_mod`, `child_predecessor` | Uses `n-w+k` and `(-n) mod w`, including zero child stride. |
+| Ordered coefficient products | `chain_affine` | Multiplication order is preserved over `Lean.Grind.Semiring`; commutativity and inverses are not assumed. |
+| Actual model reads | `scanPass_prefix`, `scanPass_suffix` | A written entry uses the current predecessor; unwritten entries retain arbitrary initial values. |
+| Two scalar passes | `passA_tail_correct`, `passC_solves_parent` | The exact child equations are a premise of reconstruction, not a proved numerical solver guarantee. |
+| Solution correspondence | `scalar_schur_iff`, `scalar_exists_iff`, `solutions_eq_iff_tails` | Covers singular systems and equality on active indices. It does not assert unique solvability. |
+
+The proof is parametric. The four fixed examples detect index/coefficient
+errors; they are not the basis for its all-length claim. The audit checks all
+package theorems, including generated lemmas. It accepts only `propext`,
+`Quot.sound` and `Classical.choice`; the two invalid-proof probes fail for
+the specified axiom violations.
+
+## Source correspondence and remaining obligations
+
+All four source files in `SOURCES.json` were recovered from their pinned Git
+objects and their SHA-256 digests were checked. The [PR #846](https://github.com/CrocSwap/integer-mult-bounds/pull/846) files are still
+byte-identical at its refreshed head. Its `bits=None` Pass A, tail slice and
+Pass C correspond to the operations and indices above.
+
+[PR #985](https://github.com/CrocSwap/integer-mult-bounds/pull/985) now has head `da1cdf8ed4ac9b1b8378dfec73f77ff4e81a4f70`.
+Its proof is unchanged from the pinned `9df42a99dd8497b6e7d46cd2507bb89071372640`.
+Its solver file has two changes: each input-validation loop binds one
+`data[i]` read to `value` before its grid comparison. The chain, child stride
+and closure implementation are unchanged. The historical source pin is
+therefore retained, with this later source comparison stated separately.
+
+This comparison is a code review, not a formal Python translation theorem.
+The Lean proof does not establish FIFO or block-swap routing, fresh-power
+return times, rounded coefficient accuracy, dirty restoration, recursive
+termination, physical cost or the multiplication theorem. Those remain the
+separate [PR #846](https://github.com/CrocSwap/integer-mult-bounds/pull/846) / [PR #985](https://github.com/CrocSwap/integer-mult-bounds/pull/985) family review. The exact algebraic result can be
+assessed on its stated scope without treating those interfaces as proved.
+
+Prepared by Ali Romman with substantial OpenAI Codex assistance. Apache-2.0.
+This is an author-side follow-up, not independent human review or a merge
+approval.
diff --git a/research/cyclic-schur-lean/NOTICE.md b/research/cyclic-schur-lean/NOTICE.md
new file mode 100644
index 0000000000..cfa93c2d58
--- /dev/null
+++ b/research/cyclic-schur-lean/NOTICE.md
@@ -0,0 +1,21 @@
+# Attribution and license
+
+New material is prepared for Ali Romman (@aliromman), with substantial
+OpenAI Codex assistance in the proof, code, verification, and text.
+The new material uses the repository's Apache-2.0 license.
+
+Rohan Guliani (@Rohansguliani), PR846, supplies the exact Euclidean
+chain/closure construction. Ali Romman, PR985, uses this identity in the
+dirty source-reuse solver. Chafik Boukhalfa (@chafreaky), PR628, and
+Charles Bethin (@cbethin), PR764, supply predecessor cyclic-inverse and
+scan work. Their mathematical contributions are not claimed as new here.
+
+Gareth Davidson (@bitplane), PR896, proves a separate generic nonlinear
+dirty-commutator result. Its proof source is not imported or modified.
+All inspected subject pins are recorded in `SOURCES.json`.
+
+Lean and its core/Std libraries retain their upstream licenses and
+authorship. They are not distributed in this package.
+
+No literature priority, new exponent, full multiplication proof,
+independent human review, or hosted CI result is claimed.
diff --git a/research/cyclic-schur-lean/README.md b/research/cyclic-schur-lean/README.md
new file mode 100644
index 0000000000..d7e96b901a
--- /dev/null
+++ b/research/cyclic-schur-lean/README.md
@@ -0,0 +1,165 @@
+# Exact cyclic Schur elimination in Lean
+
+This package proves the exact chain and closure reduction used by Rohan
+Guliani's PR846 and Ali Romman's PR985. The proof applies to every length
+`n` and stride `w` with `0 < w ≤ n`. It uses Lean 4.21.0 and its core/Std
+libraries. It needs no Mathlib package or external proof dependency.
+
+The result is a formal proof of one exact elimination step and its two
+sequential passes. It does not change the selected construction or kappa.
+
+## Statement
+
+Let the scalar type be any `Lean.Grind.Semiring`. Coefficients need not
+commute. Let `x_i` and `b_i` be arbitrary data and coefficients. The parent
+system is
+
+```text
+y_i = x_i + b_i y_((i+n-w) mod n),      0 ≤ i < n.
+```
+
+Pass A computes the following entries in increasing index order:
+
+```text
+z_i  = x_i,                          i < w
+pi_i = b_i,                          i < w
+z_i  = x_i + b_i z_(i-w),             i ≥ w
+pi_i = b_i pi_(i-w),                  i ≥ w.
+```
+
+Set `e(k) = n-w+k`, `c_k = z_e(k)`, and `a_k = pi_e(k)`. Lean proves that
+the exact closure system is
+
+```text
+Y_k = c_k + a_k Y_((k+n) mod w),      0 ≤ k < w.
+```
+
+Its stride is `(w - n mod w) mod w`, the natural-number form of
+`(-n) mod w`. The theorem `child_predecessor` proves the equality of the
+two index maps. It includes the case in which the child stride is zero.
+
+The reconstruction formula is
+
+```text
+y_i = z_i + pi_i Y_(i mod w).
+```
+
+`scalar_schur_iff` proves both directions: a parent solution restricts to
+a child solution and has this reconstruction formula; a reconstruction
+from a child solution satisfies every parent equation. The separate
+theorems `scalar_reconstruct` and `scalar_reconstruct_tail` prove the
+parent equations and exact return of every child entry.
+
+`scalar_exists_iff` proves that a parent solution exists if and only if a
+child solution exists. `solutions_eq_iff_tails` proves that two parent
+solutions agree if and only if their tails agree. These statements do not
+assume invertibility, unique solutions, a norm bound, or a division rule.
+They therefore also cover singular systems. Only entries in the active
+index ranges are compared; functions outside those ranges are irrelevant.
+
+## Connection to the source loops
+
+`scanPass` is an explicit left-to-right array-update evaluator. Step `i`
+writes entry `i`. It reads the seed if `i < w`; otherwise it reads entry
+`i-w` from the current array. The initial array can have arbitrary values.
+
+`scanPass_prefix` proves that every written entry is the recursive chain
+value. `scanPass_suffix` proves that every unwritten entry is unchanged.
+`passA_correct` specializes this evaluator to the pair update for `z` and
+`pi`. `passA_tail_correct` gives the exact data sent to the child.
+`passC_correct` specializes it to the seeded scalar update.
+`passC_solves_parent` proves that this executed Pass C solves the parent
+when its seed solves the child system.
+
+The source map below uses immutable Git commits. `SOURCES.json` also gives
+SHA-256 and Git blob identifiers for the inspected files.
+
+| Source operation | Lean definition or theorem |
+| --- | --- |
+| [PR846 Pass A](https://github.com/CrocSwap/integer-mult-bounds/blob/4bdb3e755ea7118170a7a34764df955880dec282/research/cyclic-inverse-stride-bridge/stride.py#L99) with `bits=None` | `pairStep`, `passA`, `passA_correct` |
+| [PR846 tail and child call](https://github.com/CrocSwap/integer-mult-bounds/blob/4bdb3e755ea7118170a7a34764df955880dec282/research/cyclic-inverse-stride-bridge/stride.py#L115) | `endpoint`, `childData`, `childCoefficient`, `child_predecessor` |
+| [PR846 Pass C](https://github.com/CrocSwap/integer-mult-bounds/blob/4bdb3e755ea7118170a7a34764df955880dec282/research/cyclic-inverse-stride-bridge/stride.py#L119) | `passC`, `passC_correct`, `passC_solves_parent` |
+| [PR985 source reuse identity](https://github.com/CrocSwap/integer-mult-bounds/blob/9df42a99dd8497b6e7d46cd2507bb89071372640/research/dirty-stride-source-reuse/PROOF.md#L85) | `chain_affine`, `scalar_schur_iff`, `scalar_reconstruct` |
+| [PR985 closure views](https://github.com/CrocSwap/integer-mult-bounds/blob/9df42a99dd8497b6e7d46cd2507bb89071372640/research/dirty-stride-source-reuse/dirty_stride.py#L226) | `endpoint n w k = n-w+k`, `childStride` |
+
+This is a proof of the displayed recurrence and the indexed array
+evaluator. It is not a formal semantics for Python, the two-stack FIFO,
+or the two-tape block-swap interpreter. The source correspondence above is
+an explicit code review, not a compiler-correctness theorem.
+
+For PR985, the theorem supplies the exact Schur identity. It does not prove
+that the freshly prepared child powers equal the exact chain products.
+The return-time formula and the rounding comparison remain separate.
+
+## Reproduce
+
+From the repository root, use an official Lean 4.21.0 compiler:
+
+```sh
+sh research/cyclic-schur-lean/verify.sh /path/to/lean-4.21.0/bin/lean
+```
+
+The script checks version `4.21.0` and compiler commit
+`6741444a63eec253a7eae7a83f1beb3de015023d`. It builds all three modules
+in a new temporary directory, with one Lean worker. It discards inherited
+Lean search paths and removes only its own temporary build on exit.
+It downloads nothing and does not write a package cache.
+
+The output lists the axiom dependencies of every theorem in the package
+namespace, including generated equation lemmas. It ends with:
+
+```text
+PASS_CYCLIC_SCHUR: 102 theorems; standard axioms only
+PASS_AUDIT_GUARDS: incomplete proof and package axiom rejected
+```
+
+The count includes compiler-generated helper theorems. The mathematical
+result is the parametric proof above, not that count. `AXIOMS.txt` records
+the checked dependency report. All dependencies are drawn from `propext`,
+`Quot.sound`, and `Classical.choice`. The central scalar Schur theorem
+uses only `propext` and `Quot.sound`. No theorem uses `sorryAx`, a custom
+axiom, or a native evaluation oracle.
+
+The script also compiles two separate invalid proof probes. The axiom
+guard must reject an incomplete proof through `sorryAx` and reject a
+declared package axiom. The script checks the exact rejection reason, so
+an unrelated compilation error cannot make these controls pass. Those
+invalid probes are temporary test inputs, not proof dependencies.
+
+`Counterexamples.lean` supplies four kernel-checked mathematical controls:
+the wrong child-stride sign, an early tail start, an omitted chain-start
+coefficient, and a stale predecessor read. An explicit eight-entry parent
+solution and its three-entry closure fix the first three examples. These
+examples support review; they are not the proof of the all-length result.
+
+## Scope and credit
+
+The tested base is `8bddbee377e2f3ce1f1247196c4b290d55767d20`.
+Only this new package changes. `upstream/`, the Python solvers, precision
+claims, phase contracts, and the selected certificates stay unchanged.
+
+Rohan Guliani's PR846 supplies the chain/closure algorithm. Ali Romman's
+PR985 uses its exact identity inside the dirty source-reuse construction.
+Chafik Boukhalfa's PR628 and Charles Bethin's PR764 supply predecessor
+cyclic-inverse and scan analysis. This package does not claim a new Schur
+algorithm or literature priority.
+
+Gareth Davidson's PR896 proves the generic nonlinear dirty commutator. It
+does not prove this indexed elimination identity. No PR896 proof source
+is imported here. The two results have separate contracts.
+
+This package leaves rounding, norm and precision estimates, original-cycle
+return times, reversal and normalization of arbitrary input strides,
+recursive solver termination, FIFO correctness, dirty restoration, tape
+costs, physical compilation, and the multiplication theorem open. It does
+not assert that a numerical child solve returns a solution; it proves what
+follows when the exact child equations hold.
+
+Prepared for Ali Romman (@aliromman), with substantial OpenAI Codex
+assistance. Apache-2.0. No independent human review or hosted CI success is
+claimed. `VALIDATION.md` gives the local checks and their limits.
+
+## Follow-up review
+
+The [2026-10-14 follow-up](FOLLOWUP-REVIEW.md) records the response to the
+maintainer triage, the fresh checks and the remaining proof boundaries.
diff --git a/research/cyclic-schur-lean/SOURCES.json b/research/cyclic-schur-lean/SOURCES.json
new file mode 100644
index 0000000000..5de46f0e19
--- /dev/null
+++ b/research/cyclic-schur-lean/SOURCES.json
@@ -0,0 +1,62 @@
+{
+  "schema": 1,
+  "base_commit": "8bddbee377e2f3ce1f1247196c4b290d55767d20",
+  "formal_dependencies": "Official Lean 4.21.0 core and Std only. The source subjects below are not imported by the proof.",
+  "toolchain": {
+    "file": "lean-toolchain",
+    "version": "4.21.0",
+    "git_commit": "6741444a63eec253a7eae7a83f1beb3de015023d",
+    "download_url": "https://github.com/leanprover/lean4/releases/download/v4.21.0/lean-4.21.0-darwin_aarch64.tar.zst",
+    "download_sha256": "e3d7d31dd0fdb7bfd1a4b953e13b32cefe84df04df96106ff8aada775386da8b"
+  },
+  "subjects": [
+    {
+      "pr": 846,
+      "author": "Rohan Guliani (@Rohansguliani)",
+      "files": [
+        {
+          "path": "research/cyclic-inverse-stride-bridge/stride.py",
+          "head": "4bdb3e755ea7118170a7a34764df955880dec282",
+          "sha256": "da56e45f414a633453e06e8d058bcec6c815c73950816fcf049d92c570f8928e",
+          "git_blob": "9229a4193b004d0dd939a502cfae75c27791dc76"
+        },
+        {
+          "path": "research/cyclic-inverse-stride-bridge/PROOF.md",
+          "head": "4bdb3e755ea7118170a7a34764df955880dec282",
+          "sha256": "3937696d2156e000519fb185a8a55fa7fd55dc12266fe0fe806dba42b2acf4e1",
+          "git_blob": "8987bfdfc4ba6635cc3e0e984ca24d91da429084"
+        }
+      ]
+    },
+    {
+      "pr": 985,
+      "author": "Ali Romman (@aliromman)",
+      "files": [
+        {
+          "path": "research/dirty-stride-source-reuse/dirty_stride.py",
+          "head": "9df42a99dd8497b6e7d46cd2507bb89071372640",
+          "sha256": "129b2bc8cf89159aae0a810fad4703caefefccf1c5f4805dd3c9b5e8d967354b",
+          "git_blob": "f469930b8b7d79cbc05a884dc2e224e32db7fc4a"
+        },
+        {
+          "path": "research/dirty-stride-source-reuse/PROOF.md",
+          "head": "9df42a99dd8497b6e7d46cd2507bb89071372640",
+          "sha256": "af6560b048b20649aebd31d68815948a104d2c87efcdf556c85a10f48bbc0489",
+          "git_blob": "01a3da73470dc773a33948ee5f8cfc8848798411"
+        }
+      ]
+    }
+  ],
+  "related_formal_work": {
+    "pr": 896,
+    "head": "4e34d42b64ff05a4f293b9748d71642e14ef273d",
+    "author": "Gareth Davidson (@bitplane)",
+    "scope": "Generic nonlinear dirty commutator. No source or theorem is imported."
+  },
+  "selected_context": {
+    "path": "certificates/selected-result.json",
+    "sha256": "1d35283cb0ce3f8db1f285683933517f9e87475d295e2b6316399ad9928c81c3",
+    "kappa": "1661960547713947/1000000000000000000",
+    "changed": false
+  }
+}
diff --git a/research/cyclic-schur-lean/VALIDATION.json b/research/cyclic-schur-lean/VALIDATION.json
new file mode 100644
index 0000000000..361e517717
--- /dev/null
+++ b/research/cyclic-schur-lean/VALIDATION.json
@@ -0,0 +1,54 @@
+{
+  "schema": 1,
+  "checked_at_utc": "2026-10-13T16:41:39.825331+00:00",
+  "base_commit": "8bddbee377e2f3ce1f1247196c4b290d55767d20",
+  "command": "sh research/cyclic-schur-lean/verify.sh /path/to/lean-4.21.0/bin/lean",
+  "exit_code": 0,
+  "compiler_version": "4.21.0",
+  "compiler_git_commit": "6741444a63eec253a7eae7a83f1beb3de015023d",
+  "platform": "macOS arm64",
+  "lean_workers": 1,
+  "source_sha256": {
+    "CyclicSchur.lean": "31775ea1accad2eaf79e57142ae034c4f08d16eac8d9c16a116e8e6b1bdb3df8",
+    "Counterexamples.lean": "d45bd6bc5c3c44487d8291f4ea1088db3e4109bcd344b1cfce7f5de79b44104c",
+    "Audit.lean": "8c21b111cccab46b1980d937090838e1a3d76e83f767fce8cc9793e9494af462",
+    "verify.sh": "34f50670d46d19cf6eaa0b12c387484fcc6a320f81fb3a2a7ec1e11ce3b3ba8b",
+    "lean-toolchain": "d24fed434d3b13adfaab57724a0a7f270ea8bf1c818b5ae5cf25cbce24dd685c",
+    "SOURCES.json": "02f348b792fe923d0c2c959ce070bb9b17927657287fdc19005fc1ec2c20d021"
+  },
+  "output_sha256": "a0cbd48a9e45107d4255bff12e10c8de37cdc79c3d0406d562ecc458b4e4fa4b",
+  "named_parametric_theorems": 30,
+  "named_reference_and_negative_theorems": 6,
+  "all_audited_theorem_declarations_including_generated": 102,
+  "allowed_axioms": [
+    "propext",
+    "Quot.sound",
+    "Classical.choice"
+  ],
+  "axiom_guard_controls": [
+    "incomplete theorem rejected for sorryAx",
+    "declared package axiom rejected"
+  ],
+  "mathematical_negative_controls": [
+    "wrong child-stride sign",
+    "tail begins one entry early",
+    "missing chain-start coefficient",
+    "stale predecessor read"
+  ],
+  "measured_run": {
+    "wall_seconds": 16.24,
+    "peak_resident_bytes": 901316608,
+    "exit_code": 0,
+    "note": "Same proof modules and guard tests. The final script has a separate signal-exit trap."
+  },
+  "not_checked": [
+    "global make verify",
+    "selected cold replay",
+    "hosted CI",
+    "Python runtime",
+    "FIFO implementation",
+    "physical tape interpreter",
+    "rounded solver",
+    "multiplication theorem"
+  ]
+}
diff --git a/research/cyclic-schur-lean/VALIDATION.md b/research/cyclic-schur-lean/VALIDATION.md
new file mode 100644
index 0000000000..8de9a96520
--- /dev/null
+++ b/research/cyclic-schur-lean/VALIDATION.md
@@ -0,0 +1,56 @@
+# Local validation
+
+The final package command exited with status 0 on 2026-10-13:
+
+```sh
+sh research/cyclic-schur-lean/verify.sh /path/to/lean-4.21.0/bin/lean
+```
+
+The machine was macOS on ARM64. The compiler reported Lean 4.21.0,
+commit `6741444a63eec253a7eae7a83f1beb3de015023d`. The downloaded
+official archive matched the release's published SHA-256 digest in
+`SOURCES.json`. The build used only the matching core and Std libraries.
+No shared Lean cache was changed.
+
+The check compiled `CyclicSchur.lean`, `Counterexamples.lean`, and
+`Audit.lean` from source in a fresh temporary directory. The final output
+is byte-identical to `AXIOMS.txt`. The guard checked 102 theorem
+declarations, including generated equation and tactic lemmas. A separate
+source inventory found all 30 named proof theorems and all six named
+example/control theorems in that report.
+
+The mathematical controls prove that four concrete incorrect reductions
+fail: positive instead of negative child stride, a tail that starts one
+entry early, omission of the chain-start coefficient, and a stale
+predecessor read. The build also verified both axiom-guard controls.
+The incomplete-proof input failed specifically on `sorryAx`. The custom
+axiom input failed specifically on the package-axiom check.
+
+A measured run of the same three proof modules and guard tests took
+16.24 seconds wall time. Peak resident memory was 901,316,608 bytes
+(859.5625 MiB). Each compiler call used `-j 1`. These are local build
+measurements, not solver performance results.
+
+The first resource wrapper could not read macOS `kern.clockrate` in the
+sandbox. It returned status 1 after the inner verification had printed
+both pass messages. That wrapper result is not counted as a successful
+run. A permitted resource-accounting run exited 0. The final plain
+verification command also exited 0 after the script's signal-cleanup
+change. The proof source did not change between those successful runs.
+
+The four inspected subject files have exact commit, Git blob, and SHA-256
+pins. The PR846 pins were checked against GitHub's immutable file API.
+The PR985 pins were checked against the local pinned Git objects. PR846,
+PR985, and PR896 still had the recorded heads at the overlap refresh.
+The recent open-PR inspection reached PR1012 and found no newer cyclic
+Schur formalization. This is a bounded overlap check, not a claim about
+all unpublished or external work.
+
+No global `make verify`, selected cold replay, hosted CI, Python runtime
+test, FIFO proof, or physical tape test was run. This package changes
+none of those implementations or certificates. The limits in `README.md`
+remain part of the claim. No independent human review is claimed.
+
+`VALIDATION.json` binds the checked source bytes and output digest. The
+full local logs and the compiler receipt are retained in the lane archive
+named in the coordinator handoff.
diff --git a/research/cyclic-schur-lean/lean-toolchain b/research/cyclic-schur-lean/lean-toolchain
new file mode 100644
index 0000000000..980709bbba
--- /dev/null
+++ b/research/cyclic-schur-lean/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.21.0
diff --git a/research/cyclic-schur-lean/verify.sh b/research/cyclic-schur-lean/verify.sh
new file mode 100644
index 0000000000..4e931a1505
--- /dev/null
+++ b/research/cyclic-schur-lean/verify.sh
@@ -0,0 +1,52 @@
+#!/bin/sh
+set -eu
+
+if [ "$#" -ne 1 ]; then
+  printf '%s\n' 'Usage: sh verify.sh /path/to/lean-4.21.0/bin/lean' >&2
+  exit 2
+fi
+
+compiler=$(cd "$(dirname "$1")" && pwd)/$(basename "$1")
+package=$(CDPATH= cd -- "$(dirname -- "$0")" && pwd)
+unset LEAN_PATH LEAN_SYSROOT
+
+if [ "$("$compiler" --short-version)" != '4.21.0' ] ||
+   [ "$("$compiler" --githash)" != '6741444a63eec253a7eae7a83f1beb3de015023d' ]; then
+  printf '%s\n' 'Expected the official Lean 4.21.0 compiler commit.' >&2
+  exit 1
+fi
+
+build=$(mktemp -d "${TMPDIR:-/tmp}/cyclic-schur.XXXXXXXX")
+trap 'rm -rf "$build"' EXIT
+trap 'exit 1' HUP INT TERM
+export LEAN_PATH="$build"
+cd "$package"
+
+"$compiler" --version
+"$compiler" -j 1 -o "$build/CyclicSchur.olean" CyclicSchur.lean
+"$compiler" -j 1 -o "$build/Counterexamples.olean" Counterexamples.lean
+"$compiler" -j 1 -o "$build/Audit.olean" Audit.lean
+
+# These probes must fail at the axiom guard, not at an unrelated build step.
+cat > "$build/RejectSorry.lean" <<'EOF'
+import Audit
+theorem CyclicSchur.auditProbe : False := by sorry
+run_cmd CyclicSchurAudit.check
+EOF
+if "$compiler" -j 1 "$build/RejectSorry.lean" > "$build/sorry.log" 2>&1; then
+  printf '%s\n' 'FAIL: the audit accepted an incomplete proof.' >&2
+  exit 1
+fi
+grep -F 'Disallowed axiom in CyclicSchur.auditProbe: sorryAx' "$build/sorry.log" > /dev/null
+
+cat > "$build/RejectAxiom.lean" <<'EOF'
+import Audit
+axiom CyclicSchur.auditProbe : False
+run_cmd CyclicSchurAudit.check
+EOF
+if "$compiler" -j 1 "$build/RejectAxiom.lean" > "$build/axiom.log" 2>&1; then
+  printf '%s\n' 'FAIL: the audit accepted a package axiom.' >&2
+  exit 1
+fi
+grep -F 'Package declares an axiom: CyclicSchur.auditProbe' "$build/axiom.log" > /dev/null
+printf '%s\n' 'PASS_AUDIT_GUARDS: incomplete proof and package axiom rejected'