From ab9341183d710418a2e216ad4501495064ae13f3 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@lean-fro.org>
Date: Thu, 9 Jul 2026 04:11:08 +0000
Subject: [PATCH 01/13] doc: progress note for issue #8691 measurement +
 re-scope session

Measured the SD4 recovery modulus (11^13, ~45 bits, not near 2^64) and a
1.8x byte-identical native-Montgomery cldQuotientMod prototype; posted
findings + re-scope recommendation on the issue rather than landing a
proof-only WordPolyMod layer as dead code.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
---
 progress/2026-07-09T04-10-36Z.md | 53 ++++++++++++++++++++++++++++++++
 1 file changed, 53 insertions(+)
 create mode 100644 progress/2026-07-09T04-10-36Z.md

diff --git a/progress/2026-07-09T04-10-36Z.md b/progress/2026-07-09T04-10-36Z.md
new file mode 100644
index 000000000..4241dd699
--- /dev/null
+++ b/progress/2026-07-09T04-10-36Z.md
@@ -0,0 +1,53 @@
+# issue #8691: measured the premise, re-scoped rather than built dead code
+
+## Accomplished
+
+Investigated #8691 (word-sized Montgomery arithmetic for the BZ lattice
+tier's CLD/lift) as a directive hypothesis before committing to the large
+proof-only `WordPolyMod` layer. Key measurements:
+
+- Instrumented `factorLattice` on the `hex_lattice_spike` inputs: the SD4
+  recovery modulus is `11^13` (~45 bits), not "near 2^64" as the issue
+  framed it. #8395 early-termination stops the doubling schedule at
+  exponent 13, far short of the cap-precision exponent (398). SD5 lands at
+  `19^23` (~95 bits, already outside the word path).
+- Wrote an unproven native-word Montgomery prototype of `cldQuotientMod`
+  (Montgomery-form `Array UInt64`, `HexArith.MontCtx.mulMont`, monic long
+  division) and benchmarked vs the current `Int`/`DensePoly` path at
+  `m = 11^13`, SD4-shaped inputs: **byte-identical, 1.8x** (3022ms ->
+  1679ms / 20000 iters x8 factors). The win is real here (unlike the
+  #8642 packed-`UInt64` neutral result) because ~90-bit intermediate
+  products in the `Int` path heap-allocate as GMP; Montgomery keeps them
+  in words.
+- Got a Codex second opinion; it independently reached the same
+  conclusion (do not build deliverable 1 as dead code; report and
+  re-scope).
+
+Posted an evidence-backed findings comment on the issue with the corrected
+modulus regime, the 1.8x byte-identical benchmark, the #8642 distinction,
+the bounded end-to-end economics (~18% at SD4, ~0 at SD5/SD6 since LLL is
+57-92% and out of scope), the deliverable-2 proof-cost risk (no
+`DensePoly.map`/ring-hom transport exists; `CLDColumnBound.lean` depends on
+the current `cldQuotientMod` `rfl` shape), and three re-scope options.
+Attached the reproducible prototype. Unassigned to leave it claimable for a
+re-scoped version, per the "directives are hypotheses" doctrine.
+
+No tracked source changed; tree is clean.
+
+## Current frontier
+
+The optimization is validated but narrow (SD4-shaped, ~45-bit moduli). The
+open decision is scope: a proof-only foundational layer vs a
+feasibility-first transport-lemma PR vs folding into deliverable 4
+(crossover re-measurement, which is what actually moves the r=16 seam).
+
+## Next step
+
+Await a scope decision on the issue. If option 2 is chosen, the first code
+unit is a proven `DensePoly.map`-commutes-with-monic-`divMod` (and with
+`reduceModPow`) transport in the exact `cldQuotientMod` shape, which retires
+the deliverable-2 risk before any layer is built.
+
+## Blockers
+
+Scope re-confirmation needed (posted on the issue). No technical blocker.

From 50bee39de3774f59889dac9975b0018c15ce376d Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@lean-fro.org>
Date: Thu, 9 Jul 2026 04:51:13 +0000
Subject: [PATCH 02/13] feat(modarith): WordMod, a proven Montgomery residue
 ring over odd m < 2^64

Add `Hex.WordMod ctx`, residues modulo an odd `m < 2^64` stored in
Montgomery form on top of `HexArith.MontCtx`. Multiplication is a single
`mulMont` reduction; addition and subtraction are full-range modular
operations built from `UInt64.addCarry`/`subBorrow`, so the whole odd
`m < 2^64` range is supported (unlike `ZMod64`, capped at 2^31). Every
operation has a proven `toNat` characterisation modulo m; the additive specs
use `MontCtx.cancel_word_mod_of_lt`, now exposed from the Montgomery context.

This is the scalar layer (Phase 1) for the word-sized poly-mod-p^a arithmetic
of the Berlekamp-Zassenhaus lattice tier (#8691), measured byte-identical and
1.8x faster than the Int/bignum path at the SD4 recovery modulus.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
---
 HexArith/Montgomery/Context.lean |   6 +-
 HexModArith.lean                 |   1 +
 HexModArith/WordMod.lean         | 321 +++++++++++++++++++++++++++++++
 progress/2026-07-09T05-30-00Z.md |  40 ++++
 4 files changed, 367 insertions(+), 1 deletion(-)
 create mode 100644 HexModArith/WordMod.lean
 create mode 100644 progress/2026-07-09T05-30-00Z.md

diff --git a/HexArith/Montgomery/Context.lean b/HexArith/Montgomery/Context.lean
index 3a43d873d..9c033422c 100644
--- a/HexArith/Montgomery/Context.lean
+++ b/HexArith/Montgomery/Context.lean
@@ -327,8 +327,12 @@ Multiplication by `word` is injective on residues modulo `p`: since `p` is odd
 it is coprime to `word = 2 ^ 64`, so two reduced values `x, y < p` with
 `x * word ≡ y * word (mod p)` are equal. This is what lets the
 representative-mod-word characterisation pin down a unique `mulMont` value.
+
+Public because any word-modular residue layer built on this context (for
+example a Montgomery-form residue ring) needs the same cancellation to prove
+that its additive operations preserve the represented value.
 -/
-private theorem cancel_word_mod_of_lt (ctx : MontCtx p) {x y : Nat}
+theorem cancel_word_mod_of_lt (ctx : MontCtx p) {x y : Nat}
     (hx : x < p.toNat) (hy : y < p.toNat)
     (h : x * UInt64.word % p.toNat = y * UInt64.word % p.toNat) :
     x = y := by
diff --git a/HexModArith.lean b/HexModArith.lean
index f72e6fc7d..5e5f877fa 100644
--- a/HexModArith.lean
+++ b/HexModArith.lean
@@ -10,6 +10,7 @@ public import HexModArith.Basic
 public import HexModArith.HotLoop
 public import HexModArith.Prime
 public import HexModArith.Ring
+public import HexModArith.WordMod
 
 public section
 
diff --git a/HexModArith/WordMod.lean b/HexModArith/WordMod.lean
new file mode 100644
index 000000000..101486c2e
--- /dev/null
+++ b/HexModArith/WordMod.lean
@@ -0,0 +1,321 @@
+/-
+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
+
+public import HexArith.Montgomery.Context
+public import HexArith.UInt64.Wide
+
+public section
+set_option backward.proofsInPublic true
+
+/-!
+`WordMod ctx`: residues modulo an odd `m < 2^64`, stored in Montgomery form on
+top of `HexArith.MontCtx`. Multiplication is a single Montgomery reduction
+(`mulMont`); addition and subtraction are full-range modular operations built
+from `UInt64.addCarry`/`subBorrow`, so the whole odd-`m < 2^64` range is
+supported (unlike `ZMod64`, which caps at `2^31`). The represented residue of
+an element is `ctx.fromMont a.val`, and every operation is proven to compute the
+right residue modulo `m` via that map.
+
+This is the scalar layer for the word-sized poly-mod-`p^a` arithmetic of the
+Berlekamp-Zassenhaus lattice tier (issue #8691): an odd prime power `p^a < 2^64`
+is a valid modulus here.
+-/
+
+namespace Hex
+
+/-- Full-range modular addition of two residues below `m`. -/
+@[inline] def addModWord (m a b : UInt64) : UInt64 :=
+  if (UInt64.addCarry a b false).2 || m ≤ (UInt64.addCarry a b false).1 then
+    (UInt64.subBorrow (UInt64.addCarry a b false).1 m false).1
+  else
+    (UInt64.addCarry a b false).1
+
+/-- Full-range modular subtraction of two residues below `m`. -/
+@[inline] def subModWord (m a b : UInt64) : UInt64 :=
+  if (UInt64.subBorrow a b false).2 then
+    (UInt64.addCarry (UInt64.subBorrow a b false).1 m false).1
+  else
+    (UInt64.subBorrow a b false).1
+
+/-- `addModWord` computes the modular sum. -/
+theorem toNat_addModWord (m a b : UInt64) (hm : m.toNat ≤ UInt64.word)
+    (ha : a.toNat < m.toNat) (hb : b.toNat < m.toNat) :
+    (addModWord m a b).toNat = (a.toNat + b.toNat) % m.toNat := by
+  have haw : a.toNat < UInt64.word := UInt64.toNat_lt_word a
+  have hbw : b.toNat < UInt64.word := UInt64.toNat_lt_word b
+  have hfst : (UInt64.addCarry a b false).1.toNat = (a.toNat + b.toNat) % UInt64.word := by
+    rw [UInt64.toNat_addCarry_fst]; simp
+  have hsnd : (UInt64.addCarry a b false).2 = decide (UInt64.word ≤ a.toNat + b.toNat) := by
+    rw [UInt64.addCarry_snd]; simp
+  unfold addModWord
+  by_cases hge : m.toNat ≤ a.toNat + b.toNat
+  · -- sum ≥ m, so the modular result is `a + b - m`
+    have hmod : (a.toNat + b.toNat) % m.toNat = a.toNat + b.toNat - m.toNat := by
+      rw [Nat.mod_eq_sub_mod hge, Nat.mod_eq_of_lt (by omega)]
+    have hcond : ((UInt64.addCarry a b false).2 || m ≤ (UInt64.addCarry a b false).1) = true := by
+      rw [hsnd]
+      rcases Nat.lt_or_ge (a.toNat + b.toNat) UInt64.word with hlt | hle
+      · have hs : (UInt64.addCarry a b false).1.toNat = a.toNat + b.toNat := by
+          rw [hfst, Nat.mod_eq_of_lt hlt]
+        have : m ≤ (UInt64.addCarry a b false).1 := by
+          rw [UInt64.le_iff_toNat_le, hs]; exact hge
+        simp [this]
+      · simp [hle]
+    rw [if_pos hcond, UInt64.toNat_subBorrow_fst]
+    simp only [Bool.toNat_false, Nat.add_zero]
+    rw [hfst, hmod]
+    rcases Nat.lt_or_ge (a.toNat + b.toNat) UInt64.word with hlt | hle
+    · rw [Nat.mod_eq_of_lt hlt]
+      have he : UInt64.word + (a.toNat + b.toNat) - m.toNat
+          = UInt64.word + (a.toNat + b.toNat - m.toNat) := by omega
+      rw [he, Nat.add_mod_left, Nat.mod_eq_of_lt (by omega)]
+    · have hk : (a.toNat + b.toNat) % UInt64.word = a.toNat + b.toNat - UInt64.word := by
+        rw [Nat.mod_eq_sub_mod hle, Nat.mod_eq_of_lt (by omega)]
+      rw [hk]
+      have he : UInt64.word + (a.toNat + b.toNat - UInt64.word) - m.toNat
+          = a.toNat + b.toNat - m.toNat := by omega
+      rw [he, Nat.mod_eq_of_lt (by omega)]
+  · -- sum < m, no reduction needed
+    have hlt_word : a.toNat + b.toNat < UInt64.word := by omega
+    have hmod : (a.toNat + b.toNat) % m.toNat = a.toNat + b.toNat := Nat.mod_eq_of_lt (by omega)
+    have hs : (UInt64.addCarry a b false).1.toNat = a.toNat + b.toNat := by
+      rw [hfst, Nat.mod_eq_of_lt hlt_word]
+    have hcond : ((UInt64.addCarry a b false).2 || m ≤ (UInt64.addCarry a b false).1) = false := by
+      rw [hsnd]
+      have hc1 : ¬ UInt64.word ≤ a.toNat + b.toNat := by omega
+      have hc2 : ¬ m ≤ (UInt64.addCarry a b false).1 := by
+        rw [UInt64.le_iff_toNat_le, hs]; omega
+      simp [hc1, hc2]
+    rw [if_neg (by rw [hcond]; simp), hs, hmod]
+
+/-- `addModWord` stays below `m`. -/
+theorem addModWord_lt (m a b : UInt64) (hm : 0 < m.toNat) (hmw : m.toNat ≤ UInt64.word)
+    (ha : a.toNat < m.toNat) (hb : b.toNat < m.toNat) :
+    (addModWord m a b).toNat < m.toNat := by
+  rw [toNat_addModWord m a b hmw ha hb]
+  exact Nat.mod_lt _ hm
+
+/-- `subModWord` computes the modular difference. -/
+theorem toNat_subModWord (m a b : UInt64) (hm : m.toNat ≤ UInt64.word)
+    (ha : a.toNat < m.toNat) (hb : b.toNat < m.toNat) :
+    (subModWord m a b).toNat = (a.toNat + (m.toNat - b.toNat)) % m.toNat := by
+  have haw : a.toNat < UInt64.word := UInt64.toNat_lt_word a
+  have hbw : b.toNat < UInt64.word := UInt64.toNat_lt_word b
+  have hfst : (UInt64.subBorrow a b false).1.toNat
+      = (UInt64.word + a.toNat - b.toNat) % UInt64.word := by
+    rw [UInt64.toNat_subBorrow_fst]; simp
+  have hsnd : (UInt64.subBorrow a b false).2 = decide (a.toNat < b.toNat) := by
+    rw [UInt64.subBorrow_snd]; simp
+  unfold subModWord
+  by_cases hlt : a.toNat < b.toNat
+  · -- borrow: result wraps up by `m`
+    have hcond : (UInt64.subBorrow a b false).2 = true := by rw [hsnd]; simp [hlt]
+    rw [if_pos hcond, UInt64.toNat_addCarry_fst]
+    simp only [Bool.toNat_false, Nat.add_zero]
+    rw [hfst]
+    have hs : (UInt64.word + a.toNat - b.toNat) % UInt64.word
+        = UInt64.word + a.toNat - b.toNat := Nat.mod_eq_of_lt (by omega)
+    rw [hs]
+    have hrhs : (a.toNat + (m.toNat - b.toNat)) % m.toNat = a.toNat + (m.toNat - b.toNat) :=
+      Nat.mod_eq_of_lt (by omega)
+    rw [hrhs]
+    have he : UInt64.word + a.toNat - b.toNat + m.toNat
+        = UInt64.word + (a.toNat + (m.toNat - b.toNat)) := by omega
+    rw [he, Nat.add_mod_left, Nat.mod_eq_of_lt (by omega)]
+  · -- no borrow: plain difference
+    have hcond : (UInt64.subBorrow a b false).2 = false := by rw [hsnd]; simp [hlt]
+    rw [if_neg (by rw [hcond]; simp), hfst]
+    have hs : (UInt64.word + a.toNat - b.toNat) % UInt64.word = a.toNat - b.toNat := by
+      have he : UInt64.word + a.toNat - b.toNat = UInt64.word + (a.toNat - b.toNat) := by omega
+      rw [he, Nat.add_mod_left, Nat.mod_eq_of_lt (by omega)]
+    rw [hs]
+    have hrhs : (a.toNat + (m.toNat - b.toNat)) % m.toNat = a.toNat - b.toNat := by
+      have he : a.toNat + (m.toNat - b.toNat) = (a.toNat - b.toNat) + m.toNat := by omega
+      rw [he, Nat.add_mod_right, Nat.mod_eq_of_lt (by omega)]
+    rw [hrhs]
+
+theorem subModWord_lt (m a b : UInt64) (hm : 0 < m.toNat) (hmw : m.toNat ≤ UInt64.word)
+    (ha : a.toNat < m.toNat) (hb : b.toNat < m.toNat) :
+    (subModWord m a b).toNat < m.toNat := by
+  rw [toNat_subModWord m a b hmw ha hb]
+  exact Nat.mod_lt _ hm
+
+/-- `(x + y % M) % M = (x + y) % M`. -/
+private theorem add_mod_inner (x y M : Nat) : (x + y % M) % M = (x + y) % M := by
+  rw [Nat.add_mod, Nat.mod_mod, ← Nat.add_mod]
+
+/-- Modular negation commutes with multiplication by `w`: since `(M-X)*w` and
+`X*w` sum to `M*w ≡ 0`, they are additive inverses modulo `M`. -/
+private theorem sub_mul_word_mod (M w X : Nat) (hM : 0 < M) (hXM : X ≤ M) :
+    (M - X) * w % M = (M - (X * w % M)) % M := by
+  have hsum : (M - X) * w + X * w = M * w := by
+    rw [← Nat.add_mul, Nat.sub_add_cancel hXM]
+  have hmod0 : ((M - X) * w % M + X * w % M) % M = 0 := by
+    rw [← Nat.add_mod, hsum, Nat.mul_mod_right]
+  have hylt : (M - X) * w % M < M := Nat.mod_lt _ hM
+  have hbvlt : X * w % M < M := Nat.mod_lt _ hM
+  obtain ⟨k, hk⟩ := Nat.dvd_of_mod_eq_zero hmod0
+  have hk2 : k < 2 := by
+    rcases Nat.lt_or_ge k 2 with h | h
+    · exact h
+    · exfalso
+      have hle : M * 2 ≤ M * k := Nat.mul_le_mul (Nat.le_refl M) h
+      omega
+  have hkcases : k = 0 ∨ k = 1 := by omega
+  rcases hkcases with hk0 | hk1
+  · rw [hk0, Nat.mul_zero] at hk
+    have hA : (M - X) * w % M = 0 := by omega
+    have hB : X * w % M = 0 := by omega
+    rw [hA, hB, Nat.sub_zero, Nat.mod_self]
+  · rw [hk1, Nat.mul_one] at hk
+    have hAB : (M - X) * w % M = M - X * w % M := by omega
+    rw [hAB]
+    exact (Nat.mod_eq_of_lt (by rw [← hAB]; exact hylt)).symm
+
+/-- Residues modulo an odd `m < 2^64`, stored in Montgomery form. `val` is the
+Montgomery representative; the represented residue is `ctx.fromMont val`. -/
+structure WordMod {m : UInt64} (ctx : _root_.MontCtx m) where
+  /-- Montgomery-form representative. -/
+  val : UInt64
+  /-- The representative is reduced. -/
+  isLt : val < m
+
+namespace WordMod
+
+variable {m : UInt64} {ctx : _root_.MontCtx m}
+
+@[ext] theorem ext {a b : WordMod ctx} (h : a.val = b.val) : a = b := by
+  cases a; cases b; simp_all
+
+instance : DecidableEq (WordMod ctx) := fun a b =>
+  if h : a.val = b.val then isTrue (ext h)
+  else isFalse (fun hab => h (congrArg WordMod.val hab))
+
+/-- Represented residue as a `Nat` in `[0, m)`. -/
+@[inline] def toNat (a : WordMod ctx) : Nat := (ctx.fromMont a.val).toNat
+
+theorem val_toNat_lt (a : WordMod ctx) : a.val.toNat < m.toNat := by
+  rw [← UInt64.lt_iff_toNat_lt]; exact a.isLt
+
+theorem m_le_word (ctx : _root_.MontCtx m) : m.toNat ≤ UInt64.word :=
+  Nat.le_of_lt (_root_.MontCtx.p_lt_R ctx)
+
+theorem toNat_lt (a : WordMod ctx) : a.toNat < m.toNat :=
+  UInt64.lt_iff_toNat_lt.mp (ctx.fromMont_lt a.val a.isLt)
+
+/-- Multiplication by `word` recovers the Montgomery representative: the key
+input to the word-cancellation used by the additive specs. -/
+theorem toNat_mul_word (a : WordMod ctx) :
+    a.toNat * UInt64.word % m.toNat = a.val.toNat :=
+  ctx.fromMont_repr a.val a.isLt
+
+/-- Reduce a `Nat` into `WordMod ctx`. -/
+@[inline] def ofNat (n : Nat) : WordMod ctx :=
+  ⟨ctx.toMont (UInt64.ofNat (n % m.toNat)), by
+    apply ctx.toMont_lt
+    rw [UInt64.lt_iff_toNat_lt, UInt64.toNat_ofNat_mod_word]
+    have h1 : n % m.toNat < m.toNat := Nat.mod_lt _ ctx.p_pos
+    rw [Nat.mod_eq_of_lt (Nat.lt_of_lt_of_le h1 (m_le_word ctx))]
+    exact h1⟩
+
+@[simp] theorem toNat_ofNat (n : Nat) : (ofNat (ctx := ctx) n).toNat = n % m.toNat := by
+  have h1 : n % m.toNat < m.toNat := Nat.mod_lt _ ctx.p_pos
+  have hlt : UInt64.ofNat (n % m.toNat) < m := by
+    rw [UInt64.lt_iff_toNat_lt, UInt64.toNat_ofNat_mod_word,
+      Nat.mod_eq_of_lt (Nat.lt_of_lt_of_le h1 (m_le_word ctx))]
+    exact h1
+  show (ctx.fromMont (ctx.toMont (UInt64.ofNat (n % m.toNat)))).toNat = n % m.toNat
+  rw [ctx.fromMont_toMont _ hlt, UInt64.toNat_ofNat_mod_word,
+    Nat.mod_eq_of_lt (Nat.lt_of_lt_of_le h1 (m_le_word ctx))]
+
+instance : Zero (WordMod ctx) := ⟨ofNat 0⟩
+instance : One (WordMod ctx) := ⟨ofNat 1⟩
+
+@[simp] theorem toNat_zero : (0 : WordMod ctx).toNat = 0 := by
+  show (ofNat (ctx := ctx) 0).toNat = 0
+  rw [toNat_ofNat]; simp
+
+@[simp] theorem toNat_one : (1 : WordMod ctx).toNat = 1 % m.toNat := by
+  show (ofNat (ctx := ctx) 1).toNat = 1 % m.toNat
+  rw [toNat_ofNat]
+
+/-- Montgomery multiplication: one reduction. -/
+@[inline] def mul (a b : WordMod ctx) : WordMod ctx :=
+  ⟨ctx.mulMont a.val b.val, ctx.mulMont_lt a.val b.val a.isLt b.isLt⟩
+
+instance : Mul (WordMod ctx) := ⟨mul⟩
+
+@[simp] theorem toNat_mul (a b : WordMod ctx) :
+    (a * b).toNat = (a.toNat * b.toNat) % m.toNat :=
+  ctx.mulMont_repr a.val b.val a.isLt b.isLt
+
+/-- Full-range modular addition. -/
+@[inline] def add (a b : WordMod ctx) : WordMod ctx :=
+  ⟨addModWord m a.val b.val, by
+    rw [UInt64.lt_iff_toNat_lt]
+    exact addModWord_lt m a.val b.val ctx.p_pos (m_le_word ctx) (val_toNat_lt a) (val_toNat_lt b)⟩
+
+instance : Add (WordMod ctx) := ⟨add⟩
+
+/-- Full-range modular subtraction. -/
+@[inline] def sub (a b : WordMod ctx) : WordMod ctx :=
+  ⟨subModWord m a.val b.val, by
+    rw [UInt64.lt_iff_toNat_lt]
+    exact subModWord_lt m a.val b.val ctx.p_pos (m_le_word ctx) (val_toNat_lt a) (val_toNat_lt b)⟩
+
+instance : Sub (WordMod ctx) := ⟨sub⟩
+
+/-- Modular negation, as subtraction from zero. -/
+@[inline] def neg (a : WordMod ctx) : WordMod ctx := (0 : WordMod ctx) - a
+
+instance : Neg (WordMod ctx) := ⟨neg⟩
+
+@[simp] theorem toNat_add (a b : WordMod ctx) :
+    (a + b).toNat = (a.toNat + b.toNat) % m.toNat := by
+  have hs_lt : addModWord m a.val b.val < m := by
+    rw [UInt64.lt_iff_toNat_lt]
+    exact addModWord_lt m a.val b.val ctx.p_pos (m_le_word ctx) (val_toNat_lt a) (val_toNat_lt b)
+  apply ctx.cancel_word_mod_of_lt (toNat_lt _) (Nat.mod_lt _ ctx.p_pos)
+  calc (a + b).toNat * UInt64.word % m.toNat
+      = (addModWord m a.val b.val).toNat := by
+        show (ctx.fromMont (addModWord m a.val b.val)).toNat * UInt64.word % m.toNat = _
+        exact ctx.fromMont_repr _ hs_lt
+    _ = (a.val.toNat + b.val.toNat) % m.toNat :=
+        toNat_addModWord m a.val b.val (m_le_word ctx) (val_toNat_lt a) (val_toNat_lt b)
+    _ = ((a.toNat + b.toNat) % m.toNat) * UInt64.word % m.toNat := by
+        rw [Nat.mod_mul_mod, Nat.add_mul,
+          Nat.add_mod (a.toNat * UInt64.word) (b.toNat * UInt64.word) m.toNat,
+          toNat_mul_word a, toNat_mul_word b]
+
+@[simp] theorem toNat_sub (a b : WordMod ctx) :
+    (a - b).toNat = (a.toNat + (m.toNat - b.toNat)) % m.toNat := by
+  have hs_lt : subModWord m a.val b.val < m := by
+    rw [UInt64.lt_iff_toNat_lt]
+    exact subModWord_lt m a.val b.val ctx.p_pos (m_le_word ctx) (val_toNat_lt a) (val_toNat_lt b)
+  apply ctx.cancel_word_mod_of_lt (toNat_lt _) (Nat.mod_lt _ ctx.p_pos)
+  calc (a - b).toNat * UInt64.word % m.toNat
+      = (subModWord m a.val b.val).toNat := by
+        show (ctx.fromMont (subModWord m a.val b.val)).toNat * UInt64.word % m.toNat = _
+        exact ctx.fromMont_repr _ hs_lt
+    _ = (a.val.toNat + (m.toNat - b.val.toNat)) % m.toNat :=
+        toNat_subModWord m a.val b.val (m_le_word ctx) (val_toNat_lt a) (val_toNat_lt b)
+    _ = ((a.toNat + (m.toNat - b.toNat)) % m.toNat) * UInt64.word % m.toNat := by
+        rw [Nat.mod_mul_mod, Nat.add_mul,
+          Nat.add_mod (a.toNat * UInt64.word) ((m.toNat - b.toNat) * UInt64.word) m.toNat,
+          toNat_mul_word a,
+          sub_mul_word_mod m.toNat UInt64.word b.toNat ctx.p_pos (Nat.le_of_lt (toNat_lt b)),
+          toNat_mul_word b, add_mod_inner]
+
+@[simp] theorem toNat_neg (a : WordMod ctx) :
+    (-a).toNat = (m.toNat - a.toNat) % m.toNat := by
+  show (0 - a).toNat = (m.toNat - a.toNat) % m.toNat
+  rw [toNat_sub, toNat_zero, Nat.zero_add]
+
+end WordMod
+
+end Hex
diff --git a/progress/2026-07-09T05-30-00Z.md b/progress/2026-07-09T05-30-00Z.md
new file mode 100644
index 000000000..be32fd925
--- /dev/null
+++ b/progress/2026-07-09T05-30-00Z.md
@@ -0,0 +1,40 @@
+# issue #8691 Phase 1: WordMod scalar Montgomery ring landed
+
+## Accomplished
+
+After measuring the premise (SD4 recovery modulus is `11^13 ~ 2^45`, and a
+native-Montgomery `cldQuotientMod` prototype is byte-identical and 1.8x faster
+than the current `Int`/`DensePoly` path), committed to the full path via a
+`@[csimp]` architecture and built Phase 1:
+
+- `HexModArith/WordMod.lean`: `WordMod ctx`, residues modulo an odd `m < 2^64`
+  in Montgomery form over `HexArith.MontCtx`. `Zero`/`One`/`Add`/`Sub`/`Neg`/
+  `Mul`/`DecidableEq` instances; multiplication is a single `mulMont` reduction,
+  addition/subtraction are full-range modular ops built on
+  `UInt64.addCarry`/`subBorrow` (so the whole odd `m < 2^64` range is supported,
+  unlike `ZMod64`'s `2^31` cap).
+- Proven `toNat` characterisation of every operation
+  (`toNat_mul` from `MontCtx.mulMont_repr`; `toNat_add`/`toNat_sub`/`toNat_neg`
+  via the word-cancellation `MontCtx.cancel_word_mod_of_lt`, which this PR
+  exposes from `HexArith/Montgomery/Context.lean`, plus the full-range
+  `toNat_addModWord`/`toNat_subModWord`). No `sorry`, no `axiom`.
+- Whole `HexModArith` library green.
+
+## Current frontier
+
+Phase 1 (proven scalar ring) is done and is the first landable unit. The
+`@[csimp]` plan: add `cldQuotientModWord` over `DensePoly (WordMod ctx)`
+(Phase 1b), prove `cldQuotientMod = cldQuotientModWord` under the guard in the
+`*Mathlib` layer via `DensePoly.map` transport + monic-division uniqueness over
+`ZMod (p^a)` (Phase 2), then wire with `@[csimp]` + a safe `p^a < 2^64` guard
+and re-measure (Phase 3). Phase 2 is the dominant remaining cost/risk.
+
+## Next step
+
+Phase 1b: `WordMod` needs a `Div` (division by the monic leading `1`) so
+`DensePoly (WordMod ctx)` has `divMod`; then `cldQuotientModWord` = reduce(f*g')
+/ monic g over it, with a conformance cross-check against `cldQuotientMod`.
+
+## Blockers
+
+None.

From 35d1f9465928de165ff6e2fa0480de0637c2e1c3 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@lean-fro.org>
Date: Thu, 9 Jul 2026 05:15:31 +0000
Subject: [PATCH 03/13] feat(bz): word-sized Montgomery CLD kernel,
 byte-identical to cldQuotientMod
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Add `Hex.cldQuotientModWord?`, the CLD quotient `(f · g') / g mod p^a` for a
monic `g`, computed over `WordMod` (single-reduction Montgomery poly
arithmetic) whenever the guard `Odd (p^a) ∧ p^a < 2^64` holds and declining
otherwise. `powLtWord?` checks `p^a < 2^64` with early exit so a huge exponent
never materialises a bignum. Give `WordMod` the `NatCast` and (monic-only)
`Div` instances the dense-poly `derivative`/`divMod` need.

Conformance `#guard`s in HexBerlekampZassenhaus.Conformance pin the kernel
byte-identical to the bignum `cldQuotientMod` (SD3/√2+√3 cores, moduli 7^5,
11^13, 5^9) and confirm the guard declines on 11^400. The correspondence proof
and `@[csimp]` wiring are the next phases (#8691).

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
---
 HexBerlekampZassenhaus.lean                   |  1 +
 HexBerlekampZassenhaus/WordCld.lean           | 59 +++++++++++++++++++
 HexModArith/WordMod.lean                      | 10 ++++
 .../HexBerlekampZassenhaus/Conformance.lean   | 14 +++++
 4 files changed, 84 insertions(+)
 create mode 100644 HexBerlekampZassenhaus/WordCld.lean

diff --git a/HexBerlekampZassenhaus.lean b/HexBerlekampZassenhaus.lean
index c84f19411..dd0f871df 100644
--- a/HexBerlekampZassenhaus.lean
+++ b/HexBerlekampZassenhaus.lean
@@ -23,6 +23,7 @@ public import HexBerlekampZassenhaus.QuadraticRootProofs
 public import HexBerlekampZassenhaus.PrimitivityProofs
 public import HexBerlekampZassenhaus.ProductProofs
 public import HexBerlekampZassenhaus.SmallModSingleton
+public import HexBerlekampZassenhaus.WordCld
 
 public section
 
diff --git a/HexBerlekampZassenhaus/WordCld.lean b/HexBerlekampZassenhaus/WordCld.lean
new file mode 100644
index 000000000..2826465df
--- /dev/null
+++ b/HexBerlekampZassenhaus/WordCld.lean
@@ -0,0 +1,59 @@
+/-
+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
+
+public import HexModArith
+public import HexHensel.Basic
+public import HexPoly
+
+public section
+
+/-!
+Word-sized (Montgomery) computation of the CLD quotient for the
+Berlekamp-Zassenhaus lattice tier (issue #8691, Phase 1b).
+
+`cldQuotientModWord?` mirrors `Hex.cldQuotientMod` but runs all mod-`p^a`
+polynomial arithmetic over `Hex.WordMod` (residue arrays with single-reduction
+Montgomery multiplication) instead of `Int`/bignum, whenever `p^a` fits an odd
+machine word. It is byte-identical to `cldQuotientMod` on a monic divisor `g`;
+the correspondence proof is Phase 2, after which it is wired via `@[csimp]`.
+-/
+
+namespace Hex
+
+/-- `true` and the value `p^a` if `p^a < 2^64`, computed with early exit so a
+huge exponent never materialises a bignum. -/
+def powLtWord? (p a : Nat) : Option Nat :=
+  go a 1
+where
+  go : Nat → Nat → Option Nat
+    | 0, acc => some acc
+    | n + 1, acc =>
+        let next := acc * p
+        if next < UInt64.word then go n next else none
+
+/--
+Word-sized CLD quotient `(f · g') / g mod p^a` for monic `g`, computed over
+`WordMod` when the guard `Odd (p^a) ∧ p^a < 2^64` holds (`p` odd prime ⇒ `p^a`
+odd). Returns `none` when the guard fails, so the caller keeps the bignum path.
+-/
+def cldQuotientModWord? (f g : ZPoly) (p a : Nat) : Option ZPoly :=
+  match powLtWord? p a with
+  | none => none
+  | some m =>
+      let mU : UInt64 := UInt64.ofNat m
+      if h : mU % 2 = 1 then
+        let ctx := _root_.MontCtx.mk mU h
+        let toW : Int → WordMod ctx := fun c => WordMod.ofNat (ZPoly.intModNat c m)
+        let fW : DensePoly (WordMod ctx) := DensePoly.ofCoeffs (f.toArray.map toW)
+        let gW : DensePoly (WordMod ctx) := DensePoly.ofCoeffs (g.toArray.map toW)
+        let qW := (DensePoly.divMod (fW * DensePoly.derivative gW) gW).1
+        some (DensePoly.ofCoeffs (qW.toArray.map (fun w => Int.ofNat w.toNat)))
+      else
+        none
+
+end Hex
diff --git a/HexModArith/WordMod.lean b/HexModArith/WordMod.lean
index 101486c2e..eb04383b8 100644
--- a/HexModArith/WordMod.lean
+++ b/HexModArith/WordMod.lean
@@ -235,6 +235,16 @@ theorem toNat_mul_word (a : WordMod ctx) :
 
 instance : Zero (WordMod ctx) := ⟨ofNat 0⟩
 instance : One (WordMod ctx) := ⟨ofNat 1⟩
+instance : NatCast (WordMod ctx) := ⟨ofNat⟩
+
+/-- Division, defined only where it is used: by the leading coefficient of a
+monic divisor, which is `1`. Dividing by `1` is the identity (`div_one`);
+other divisors return `0` and are never exercised by monic `divMod`. -/
+@[inline] def div (a b : WordMod ctx) : WordMod ctx := if b = 1 then a else 0
+
+instance : Div (WordMod ctx) := ⟨div⟩
+
+@[simp] theorem div_one (a : WordMod ctx) : a / 1 = a := if_pos rfl
 
 @[simp] theorem toNat_zero : (0 : WordMod ctx).toNat = 0 := by
   show (ofNat (ctx := ctx) 0).toNat = 0
diff --git a/conformance/HexBerlekampZassenhaus/Conformance.lean b/conformance/HexBerlekampZassenhaus/Conformance.lean
index 7f6ee447c..3996613c9 100644
--- a/conformance/HexBerlekampZassenhaus/Conformance.lean
+++ b/conformance/HexBerlekampZassenhaus/Conformance.lean
@@ -728,5 +728,19 @@ private def zCertRoundTripsLinear (f : ZPoly) : Bool :=
 #guard (certifyIrreducible? swinnertonDyerSD3).isNone
 #guard (certifyIrreducible? phi15).isNone
 
+-- Issue #8691: the word-sized Montgomery CLD kernel `cldQuotientModWord?` is
+-- byte-identical to the bignum `cldQuotientMod` whenever its guard
+-- (`Odd (p^a) ∧ p^a < 2^64`) holds, and declines (returns `none`) otherwise.
+-- `g` is monic (leading coefficient `1`), as the lifted local factors are.
+private def cldTestDivisor : ZPoly := DensePoly.ofCoeffs #[3, 1]
+#guard cldQuotientModWord? swinnertonDyerSD3 cldTestDivisor 7 5
+        = some (cldQuotientMod swinnertonDyerSD3 cldTestDivisor 7 5)
+#guard cldQuotientModWord? swinnertonDyerSD3 cldTestDivisor 11 13
+        = some (cldQuotientMod swinnertonDyerSD3 cldTestDivisor 11 13)
+#guard cldQuotientModWord? quadSqrt2Sqrt3 cldTestDivisor 5 9
+        = some (cldQuotientMod quadSqrt2Sqrt3 cldTestDivisor 5 9)
+-- Guard declines when `p^a` overflows the word.
+#guard (cldQuotientModWord? swinnertonDyerSD3 cldTestDivisor 11 400).isNone
+
 end BZConformance
 end Hex

From 0485e1b3cb10e27780d47daaa054f39091e548ba Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@lean-fro.org>
Date: Thu, 9 Jul 2026 05:18:26 +0000
Subject: [PATCH 04/13] doc: progress note for issue #8691 Phases 1+1b (PR
 #8697)

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
---
 progress/2026-07-09T06-40-00Z.md | 50 ++++++++++++++++++++++++++++++++
 1 file changed, 50 insertions(+)
 create mode 100644 progress/2026-07-09T06-40-00Z.md

diff --git a/progress/2026-07-09T06-40-00Z.md b/progress/2026-07-09T06-40-00Z.md
new file mode 100644
index 000000000..1c3c62aba
--- /dev/null
+++ b/progress/2026-07-09T06-40-00Z.md
@@ -0,0 +1,50 @@
+# issue #8691 Phases 1+1b landed (PR #8697); Phase 2 mapped
+
+## Accomplished
+
+PR https://github.com/kim-em/hex-dev/pull/8697 now carries two proven, tested
+steps toward word-sized lattice-tier arithmetic:
+
+- **Phase 1** `HexModArith/WordMod.lean`: `WordMod ctx`, an odd-`m < 2^64`
+  Montgomery residue ring (single-reduction `mulMont`, full-range
+  `addModWord`/`subModWord` on `addCarry`/`subBorrow`), every op proven correct
+  via a `toNat` characterisation mod `m`. Exposes `MontCtx.cancel_word_mod_of_lt`.
+  Also `NatCast`/`Div` (monic-only) instances so dense-poly `derivative`/`divMod`
+  work over it. CI-green (whole graph incl. the merge-gating `*Mathlib` layer).
+- **Phase 1b** `HexBerlekampZassenhaus/WordCld.lean`: `cldQuotientModWord?`
+  (guarded `Odd (p^a) ∧ p^a < 2^64`, `powLtWord?` overflow-safe) plus
+  conformance `#guard`s proving it byte-identical to `cldQuotientMod` on the SD3
+  and √2+√3 cores at moduli 7^5, 11^13, 5^9, and declining on 11^400. Kernel is
+  its own module so Phase-3 `@[csimp]` in `Lattice.lean` imports it, no cycle.
+
+No `sorry`, no `axiom`.
+
+## Current frontier
+
+Phase 2 (the byte-identical *proof*, CI-gated `*Mathlib`) is mapped and is the
+dominant remaining work:
+- `HexModArithMathlib/WordMod.lean`: `WordMod.toZMod a := (a.toNat : ZMod m)`,
+  the `toZMod_zero/one/add/mul/neg/sub` lemmas (mirror the `ZMod64.toZMod`
+  template in `HexModArithMathlib/Basic.lean`) + injectivity, then a Mathlib
+  `CommRing (WordMod ctx)` via `Function.Injective.commRing` (needs
+  `SMul ℕ/ℤ`, `Pow ℕ`, `IntCast` instances + preservation args) and
+  `WordMod ctx ≃+* ZMod m`.
+- Transport `cldQuotientMod` and `cldQuotientModWord?` into `Polynomial (ZMod m)`
+  via `DensePoly.toPolynomial` (the ring-equiv in `HexPolyMathlib/Basic.lean`,
+  with `toPolynomial_add/sub/mul/derivative`) + `Polynomial.map`, and prove the
+  one novel lemma: dense monic `divMod` corresponds to `Polynomial.divByMonic`
+  (monic-division uniqueness). Conclude `cldQuotientMod = cldQuotientModWord?`
+  under the guard.
+
+Then Phase 3: `cldQuotientModFast := if guard then word else bignum`,
+`@[csimp] cldQuotientMod = cldQuotientModFast`, re-measure `hex_lattice_spike`
+SD4. Phase 4: lift (`quadraticHenselStep`).
+
+## Next step
+
+Build `HexModArithMathlib/WordMod.lean` (the `toZMod` bridge + `CommRing` +
+`equiv`). It is the Phase-2 prerequisite and a self-contained landable milestone.
+
+## Blockers
+
+None technical. Phase 2 is large and CI-gated; land it as its own PR.

From 075548fe43b126f82e7d6d1404972ef7df01f9ad Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@lean-fro.org>
Date: Thu, 9 Jul 2026 05:25:19 +0000
Subject: [PATCH 05/13] feat(modarith-mathlib): WordMod-to-ZMod correspondence
 bridge
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Add `HexModArithMathlib.WordMod.toZMod : Hex.WordMod ctx → ZMod m.toNat` with
its injectivity and the homomorphism laws (`toZMod_zero/one/add/mul/neg/sub`),
mirroring the existing `ZMod64` bridge. This is the Phase-2 foundation for the
byte-identical CLD correspondence (#8691): the next steps bundle a Mathlib
`CommRing (WordMod ctx)` and `≃+* ZMod` through this map, then transport the
word-sized and bignum CLD quotients into `Polynomial (ZMod (p^a))` to prove them
equal under the guard.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
---
 HexModArithMathlib.lean         |   1 +
 HexModArithMathlib/WordMod.lean | 103 ++++++++++++++++++++++++++++++++
 2 files changed, 104 insertions(+)
 create mode 100644 HexModArithMathlib/WordMod.lean

diff --git a/HexModArithMathlib.lean b/HexModArithMathlib.lean
index a33aa02e8..b16c82cf6 100644
--- a/HexModArithMathlib.lean
+++ b/HexModArithMathlib.lean
@@ -7,6 +7,7 @@ Authors: Kim Morrison
 module
 
 public import HexModArithMathlib.Basic
+public import HexModArithMathlib.WordMod
 
 public section
 
diff --git a/HexModArithMathlib/WordMod.lean b/HexModArithMathlib/WordMod.lean
new file mode 100644
index 000000000..14fb7cbcd
--- /dev/null
+++ b/HexModArithMathlib/WordMod.lean
@@ -0,0 +1,103 @@
+/-
+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
+
+public import Mathlib.Data.ZMod.Basic
+public import HexModArith
+
+public section
+
+/-!
+Correspondence between the executable `Hex.WordMod` residue ring and Mathlib's
+`ZMod`. `toZMod` sends a Montgomery-form residue to its class in `ZMod m.toNat`;
+the transport lemmas below (mirroring `HexModArithMathlib.ZMod64`) are the
+homomorphism laws used to lift the executable word arithmetic to Mathlib and,
+downstream, to prove the word-sized CLD kernel byte-identical to the bignum path
+(issue #8691, Phase 2).
+
+`m.toNat` is positive (`ctx.p_pos`) but that fact needs `ctx`, which `m.toNat`
+does not mention, so `NeZero m.toNat` cannot be a free instance; each proof
+introduces it locally.
+-/
+
+namespace HexModArithMathlib
+
+open Hex
+
+namespace WordMod
+
+variable {m : UInt64} {ctx : _root_.MontCtx m}
+
+/-- Interpret an executable `WordMod` residue as a Mathlib `ZMod` class. -/
+@[expose]
+def toZMod (a : Hex.WordMod ctx) : ZMod m.toNat := (a.toNat : ZMod m.toNat)
+
+/-- The canonical representative of a transferred class is the residue's value. -/
+@[simp] theorem val_toZMod (a : Hex.WordMod ctx) : (toZMod a).val = a.toNat := by
+  haveI : NeZero m.toNat := ⟨Nat.ne_of_gt ctx.p_pos⟩
+  rw [toZMod, ZMod.val_natCast, Nat.mod_eq_of_lt a.toNat_lt]
+
+/-- `toZMod` is injective: its `ZMod` value is the residue, which pins the word. -/
+theorem toZMod_injective : Function.Injective (toZMod (ctx := ctx)) := by
+  intro a b h
+  have hval : a.toNat = b.toNat := by
+    have := congrArg ZMod.val h
+    rwa [val_toZMod, val_toZMod] at this
+  apply Hex.WordMod.ext
+  apply UInt64.toNat_inj.mp
+  calc a.val.toNat
+      = a.toNat * UInt64.word % m.toNat := (Hex.WordMod.toNat_mul_word a).symm
+    _ = b.toNat * UInt64.word % m.toNat := by rw [hval]
+    _ = b.val.toNat := Hex.WordMod.toNat_mul_word b
+
+@[simp] theorem toZMod_zero : toZMod (0 : Hex.WordMod ctx) = 0 := by
+  haveI : NeZero m.toNat := ⟨Nat.ne_of_gt ctx.p_pos⟩
+  apply ZMod.val_injective
+  rw [val_toZMod, ZMod.val_zero, Hex.WordMod.toNat_zero]
+
+@[simp] theorem toZMod_add (a b : Hex.WordMod ctx) :
+    toZMod (a + b) = toZMod a + toZMod b := by
+  haveI : NeZero m.toNat := ⟨Nat.ne_of_gt ctx.p_pos⟩
+  apply ZMod.val_injective
+  rw [ZMod.val_add, val_toZMod, val_toZMod, val_toZMod, Hex.WordMod.toNat_add]
+
+@[simp] theorem toZMod_mul (a b : Hex.WordMod ctx) :
+    toZMod (a * b) = toZMod a * toZMod b := by
+  haveI : NeZero m.toNat := ⟨Nat.ne_of_gt ctx.p_pos⟩
+  apply ZMod.val_injective
+  rw [ZMod.val_mul, val_toZMod, val_toZMod, val_toZMod, Hex.WordMod.toNat_mul]
+
+@[simp] theorem toZMod_one : toZMod (1 : Hex.WordMod ctx) = 1 := by
+  haveI : NeZero m.toNat := ⟨Nat.ne_of_gt ctx.p_pos⟩
+  apply ZMod.val_injective
+  rw [val_toZMod, Hex.WordMod.toNat_one, ZMod.val_one_eq_one_mod]
+
+@[simp] theorem toZMod_neg (a : Hex.WordMod ctx) : toZMod (-a) = -toZMod a := by
+  have hle : a.toNat ≤ m.toNat := Nat.le_of_lt a.toNat_lt
+  rw [toZMod, Hex.WordMod.toNat_neg]
+  calc (((m.toNat - a.toNat) % m.toNat : Nat) : ZMod m.toNat)
+      = ((m.toNat - a.toNat : Nat) : ZMod m.toNat) := by
+        rw [ZMod.natCast_mod]
+    _ = ((m.toNat : Nat) : ZMod m.toNat) - ((a.toNat : Nat) : ZMod m.toNat) := by
+        rw [Nat.cast_sub hle]
+    _ = -toZMod a := by rw [ZMod.natCast_self]; simp [toZMod]
+
+@[simp] theorem toZMod_sub (a b : Hex.WordMod ctx) :
+    toZMod (a - b) = toZMod a - toZMod b := by
+  have hle : b.toNat ≤ m.toNat := Nat.le_of_lt b.toNat_lt
+  rw [toZMod, Hex.WordMod.toNat_sub]
+  calc (((a.toNat + (m.toNat - b.toNat)) % m.toNat : Nat) : ZMod m.toNat)
+      = ((a.toNat + (m.toNat - b.toNat) : Nat) : ZMod m.toNat) := by
+        rw [ZMod.natCast_mod]
+    _ = ((a.toNat : Nat) : ZMod m.toNat)
+          + (((m.toNat : Nat) : ZMod m.toNat) - ((b.toNat : Nat) : ZMod m.toNat)) := by
+        rw [Nat.cast_add, Nat.cast_sub hle]
+    _ = toZMod a - toZMod b := by rw [ZMod.natCast_self]; simp [toZMod, sub_eq_add_neg]
+
+end WordMod
+
+end HexModArithMathlib

From 2bd7f7c67c95631af63d0be46daffbcc6a55dd5f Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@lean-fro.org>
Date: Thu, 9 Jul 2026 06:01:24 +0000
Subject: [PATCH 06/13] feat(modarith-mathlib): CommRing (WordMod) and RingHom
 to ZMod
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Give the executable `WordMod ctx` a Mathlib `CommRing` structure, pulled back
along the injective `toZMod` via `Function.Injective.commRing` (adding the
`SMul ℕ/ℤ`, `Pow ℕ`, `IntCast` data with immediate transport proofs), and
package `toZMod` as `toZModRingHom : WordMod ctx →+* ZMod m.toNat`. This is the
algebraic backbone for the Phase-2 CLD correspondence (#8691): the remaining
step transports both quotients through `DensePoly.toPolynomial` + `Polynomial.map`
into `Polynomial (ZMod (p^a))` and proves them equal via monic-division
uniqueness.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
---
 HexModArithMathlib/WordMod.lean | 67 +++++++++++++++++++++++++++++++++
 1 file changed, 67 insertions(+)

diff --git a/HexModArithMathlib/WordMod.lean b/HexModArithMathlib/WordMod.lean
index 14fb7cbcd..91032e6b0 100644
--- a/HexModArithMathlib/WordMod.lean
+++ b/HexModArithMathlib/WordMod.lean
@@ -98,6 +98,73 @@ theorem toZMod_injective : Function.Injective (toZMod (ctx := ctx)) := by
         rw [Nat.cast_add, Nat.cast_sub hle]
     _ = toZMod a - toZMod b := by rw [ZMod.natCast_self]; simp [toZMod, sub_eq_add_neg]
 
+/-! ### Mathlib `CommRing` structure, transferred along `toZMod`.
+
+`WordMod` already carries `Zero/One/Add/Mul/Neg/Sub/NatCast`; the remaining data
+a `CommRing` needs (`SMul ℕ`, `SMul ℤ`, `Pow ℕ`, `IntCast`) is defined here so
+that each transports to `ZMod` immediately, then `Function.Injective.commRing`
+pulls the ring structure back through the injective `toZMod`. -/
+
+instance : SMul ℕ (Hex.WordMod ctx) := ⟨fun n a => (n : Hex.WordMod ctx) * a⟩
+
+instance : IntCast (Hex.WordMod ctx) :=
+  ⟨fun z => match z with
+    | Int.ofNat n => (n : Hex.WordMod ctx)
+    | Int.negSucc n => -((n + 1 : Nat) : Hex.WordMod ctx)⟩
+
+instance : SMul ℤ (Hex.WordMod ctx) := ⟨fun z a => (z : Hex.WordMod ctx) * a⟩
+
+instance : Pow (Hex.WordMod ctx) ℕ := ⟨fun a n => npowRec n a⟩
+
+@[simp] theorem toZMod_natCast (n : Nat) :
+    toZMod ((n : Hex.WordMod ctx)) = (n : ZMod m.toNat) := by
+  haveI : NeZero m.toNat := ⟨Nat.ne_of_gt ctx.p_pos⟩
+  show toZMod (Hex.WordMod.ofNat n) = _
+  rw [toZMod, Hex.WordMod.toNat_ofNat, ZMod.natCast_mod]
+
+@[simp] theorem toZMod_intCast (z : Int) :
+    toZMod ((z : Hex.WordMod ctx)) = (z : ZMod m.toNat) := by
+  cases z with
+  | ofNat n =>
+      show toZMod ((n : Hex.WordMod ctx)) = _
+      rw [toZMod_natCast]; simp
+  | negSucc n =>
+      show toZMod (-((n + 1 : Nat) : Hex.WordMod ctx)) = _
+      rw [toZMod_neg, toZMod_natCast]
+      exact (Int.cast_negSucc n).symm
+
+theorem toZMod_npowRec (a : Hex.WordMod ctx) (n : Nat) :
+    toZMod (npowRec n a) = toZMod a ^ n := by
+  induction n with
+  | zero => simp [npowRec, toZMod_one]
+  | succ k ih => rw [npowRec, toZMod_mul, ih, pow_succ]
+
+/-- The executable `WordMod` residue ring is a Mathlib `CommRing`, pulled back
+along the injective `toZMod`. -/
+instance : CommRing (Hex.WordMod ctx) :=
+  Function.Injective.commRing toZMod toZMod_injective
+    toZMod_zero toZMod_one toZMod_add toZMod_mul toZMod_neg toZMod_sub
+    (fun n x => by
+      show toZMod ((n : Hex.WordMod ctx) * x) = n • toZMod x
+      rw [toZMod_mul, toZMod_natCast, nsmul_eq_mul])
+    (fun z x => by
+      show toZMod ((z : Hex.WordMod ctx) * x) = z • toZMod x
+      rw [toZMod_mul, toZMod_intCast, zsmul_eq_mul])
+    (fun x n => toZMod_npowRec x n)
+    toZMod_natCast toZMod_intCast
+
+/-- `toZMod` packaged as a ring homomorphism. -/
+def toZModRingHom : Hex.WordMod ctx →+* ZMod m.toNat where
+  toFun := toZMod
+  map_one' := toZMod_one
+  map_mul' := toZMod_mul
+  map_zero' := toZMod_zero
+  map_add' := toZMod_add
+
+@[simp] theorem toZModRingHom_apply (a : Hex.WordMod ctx) :
+    toZModRingHom a = toZMod a := by
+  simp only [toZModRingHom, RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk]
+
 end WordMod
 
 end HexModArithMathlib

From 8afaa605e47a6c1fb630ed5e1fa95fec25b7d901 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@lean-fro.org>
Date: Thu, 9 Jul 2026 06:03:07 +0000
Subject: [PATCH 07/13] doc: progress note for issue #8691 Phase-2 algebraic
 backbone

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
---
 progress/2026-07-09T07-40-00Z.md | 54 ++++++++++++++++++++++++++++++++
 1 file changed, 54 insertions(+)
 create mode 100644 progress/2026-07-09T07-40-00Z.md

diff --git a/progress/2026-07-09T07-40-00Z.md b/progress/2026-07-09T07-40-00Z.md
new file mode 100644
index 000000000..a3c55c08c
--- /dev/null
+++ b/progress/2026-07-09T07-40-00Z.md
@@ -0,0 +1,54 @@
+# issue #8691 Phase-2 algebraic backbone landed; poly transport scoped
+
+## Accomplished
+
+On PR https://github.com/kim-em/hex-dev/pull/8697 (branch `issue-8691`), all
+green, no `sorry`/`axiom`:
+
+- Phase 1 `WordMod` proven Montgomery ring; Phase 1b `cldQuotientModWord?`
+  kernel + conformance `#guard`s byte-identical to `cldQuotientMod`.
+- **Phase-2 algebraic backbone** `HexModArithMathlib/WordMod.lean`:
+  `WordMod.toZMod : WordMod ctx → ZMod m.toNat` with injectivity and the full
+  homomorphism suite (`zero/one/add/mul/neg/sub/natCast/intCast`), a Mathlib
+  `CommRing (WordMod ctx)` pulled back via `Function.Injective.commRing`, and
+  `toZModRingHom : WordMod ctx →+* ZMod m.toNat`. Whole `HexModArithMathlib`
+  green.
+
+## Current frontier
+
+Only the poly-level transport of Phase 2 remains — `cldQuotientMod f g p a =
+some⁻¹ (cldQuotientModWord? f g p a)` under the guard. The shape is now fully
+determined; the needed infrastructure exists:
+
+- `HexPoly/Euclid/Reconstruction.lean`: `divMod_reconstruction` (generic
+  `(divMod a g).1 * g + (divMod a g).2 = a`), `divModArray_reconstruction`.
+- `HexPoly/Euclid/DivGcd.lean`: `DensePoly.Monic`, `divModMonic`, `modByMonic`,
+  `modByMonic_eq_divModMonic`, the remainder-degree lemmas.
+- `HexPolyMathlib/Basic.lean`: `DensePoly.toPolynomial` (`≃+*`) with
+  `toPolynomial_add/sub/mul/derivative/monomial`, `natDegree_toPolynomial`,
+  `leadingCoeff_toPolynomial`.
+- `HexModArithMathlib/WordMod.lean`: `toZModRingHom` (this PR).
+
+Proof plan: both `cldQuotientModWord?` (over `WordMod`) and `cldQuotientMod`
+(over `Int`, reduced) satisfy `q·g + r = numerator`, `deg r < deg g`, `g` monic.
+Map each reconstruction identity into `ZMod (p^a)[X]` (word side via
+`toZModRingHom`/`toPolynomial` + `Polynomial.map`; Int side via
+`Int.castRingHom (ZMod (p^a))`). Both numerators map to `f·g' mod p^a` and both
+`g`s to the same monic image, so by monic-division uniqueness in `ZMod (p^a)[X]`
+the two quotient images agree; since both executable outputs are the canonical
+`[0, p^a)` residue representation of that image, the `ZPoly`s are equal.
+
+Then Phase 3: `cldQuotientModFast := if guard then word else bignum`,
+`@[csimp] cldQuotientMod = cldQuotientModFast`, re-measure `hex_lattice_spike`
+SD4. Phase 4: the Hensel lift.
+
+## Next step
+
+Write `HexBerlekampZassenhausMathlib/WordCld.lean`: the monic-division
+uniqueness transport and the `cldQuotientMod = cldQuotientModWord?` equality.
+This is the last proof before the runtime win can be wired.
+
+## Blockers
+
+None technical; the remaining equality is a large but well-scoped proof, and is
+CI-gated (`HexBerlekampZassenhausMathlib`), so land it as its own PR.

From c25cfb34049e7c9bd8daf760d91755913faf4355 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@lean-fro.org>
Date: Thu, 9 Jul 2026 06:59:51 +0000
Subject: [PATCH 08/13] feat(bz-mathlib): Phase-2 transport infrastructure for
 the word CLD proof

Add the coefficient casts `cZ`/`cW` from executable integer / `WordMod`
polynomials into `ZMod (p^a)[X]` with their homomorphism laws, the
canonical-representative uniqueness lemma `eq_of_cZ_eq`, and the central
`map_divMod_monic`: monic dense-polynomial division commutes with any
coefficient ring hom (via `Polynomial.div_modByMonic_unique`). These are the
reusable pieces the byte-identical `cldQuotientMod = cldQuotientModWord?`
equality (#8691, Phase 2) assembles from.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
---
 HexBerlekampZassenhausMathlib.lean         |   1 +
 HexBerlekampZassenhausMathlib/WordCld.lean | 124 +++++++++++++++++++++
 2 files changed, 125 insertions(+)
 create mode 100644 HexBerlekampZassenhausMathlib/WordCld.lean

diff --git a/HexBerlekampZassenhausMathlib.lean b/HexBerlekampZassenhausMathlib.lean
index 6924a0d8a..5e9b5c643 100644
--- a/HexBerlekampZassenhausMathlib.lean
+++ b/HexBerlekampZassenhausMathlib.lean
@@ -34,6 +34,7 @@ public import HexBerlekampZassenhausMathlib.UFDPartition
 public import HexBerlekampZassenhausMathlib.IntReductionMod
 public import HexBerlekampZassenhausMathlib.FactorSoundness
 public import HexBerlekampZassenhausMathlib.LatticeTier
+public import HexBerlekampZassenhausMathlib.WordCld
 
 public section
 
diff --git a/HexBerlekampZassenhausMathlib/WordCld.lean b/HexBerlekampZassenhausMathlib/WordCld.lean
new file mode 100644
index 000000000..a457e5ec4
--- /dev/null
+++ b/HexBerlekampZassenhausMathlib/WordCld.lean
@@ -0,0 +1,124 @@
+/-
+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
+
+public import HexBerlekampZassenhaus.WordCld
+public import HexModArithMathlib.WordMod
+public import HexPolyMathlib.Basic
+public import Mathlib.Algebra.Polynomial.Div
+
+public section
+
+/-!
+Byte-identical correspondence for the word-sized CLD kernel (issue #8691,
+Phase 2): `cldQuotientModWord? f g p a = some (cldQuotientMod f g p a)` for a
+monic `g` whenever the guard `Odd (p^a) ∧ p^a < 2^64` holds.
+
+The proof transports both quotients' Euclidean reconstructions
+(`q · g + r = numerator`, `deg r < deg g`, `g` monic) into `ZMod (p^a)[X]` and
+concludes by monic-division uniqueness (`Polynomial.div_modByMonic_unique`).
+-/
+
+namespace HexBerlekampZassenhausMathlib
+
+open Hex Polynomial
+
+/-- Coefficient cast of an executable integer polynomial into `ZMod m.toNat[X]`. -/
+noncomputable def cZ (m : UInt64) (f : Hex.ZPoly) : Polynomial (ZMod m.toNat) :=
+  Polynomial.map (Int.castRingHom (ZMod m.toNat)) (HexPolyMathlib.toPolynomial f)
+
+/-- Coefficient cast of an executable `WordMod` polynomial into `ZMod m.toNat[X]`. -/
+noncomputable def cW {m : UInt64} (ctx : _root_.MontCtx m)
+    (a : Hex.DensePoly (Hex.WordMod ctx)) : Polynomial (ZMod m.toNat) :=
+  Polynomial.map (HexModArithMathlib.WordMod.toZModRingHom (ctx := ctx))
+    (HexPolyMathlib.toPolynomial a)
+
+@[simp] theorem cZ_coeff (m : UInt64) (f : Hex.ZPoly) (j : Nat) :
+    (cZ m f).coeff j = ((f.coeff j : Int) : ZMod m.toNat) := by
+  rw [cZ, Polynomial.coeff_map, HexPolyMathlib.coeff_toPolynomial]; simp
+
+@[simp] theorem cW_coeff {m : UInt64} (ctx : _root_.MontCtx m)
+    (a : Hex.DensePoly (Hex.WordMod ctx)) (j : Nat) :
+    (cW ctx a).coeff j = HexModArithMathlib.WordMod.toZMod (a.coeff j) := by
+  rw [cW, Polynomial.coeff_map, HexPolyMathlib.coeff_toPolynomial,
+    HexModArithMathlib.WordMod.toZModRingHom_apply]
+
+theorem cZ_mul (m : UInt64) (f g : Hex.ZPoly) : cZ m (f * g) = cZ m f * cZ m g := by
+  rw [cZ, cZ, cZ, HexPolyMathlib.toPolynomial_mul, Polynomial.map_mul]
+
+theorem cZ_add (m : UInt64) (f g : Hex.ZPoly) : cZ m (f + g) = cZ m f + cZ m g := by
+  rw [cZ, cZ, cZ, HexPolyMathlib.toPolynomial_add, Polynomial.map_add]
+
+theorem cW_mul {m : UInt64} (ctx : _root_.MontCtx m)
+    (a b : Hex.DensePoly (Hex.WordMod ctx)) : cW ctx (a * b) = cW ctx a * cW ctx b := by
+  rw [cW, cW, cW, HexPolyMathlib.toPolynomial_mul, Polynomial.map_mul]
+
+theorem cW_add {m : UInt64} (ctx : _root_.MontCtx m)
+    (a b : Hex.DensePoly (Hex.WordMod ctx)) : cW ctx (a + b) = cW ctx a + cW ctx b := by
+  rw [cW, cW, cW, HexPolyMathlib.toPolynomial_add, Polynomial.map_add]
+
+/-- Canonical-representative uniqueness: two integer polynomials with all
+coefficients in `[0, m)` that are congruent mod `m` coefficientwise are equal. -/
+theorem eq_of_cZ_eq {m : UInt64}
+    (x y : Hex.ZPoly)
+    (hx : ∀ i, 0 ≤ x.coeff i ∧ x.coeff i < (m.toNat : Int))
+    (hy : ∀ i, 0 ≤ y.coeff i ∧ y.coeff i < (m.toNat : Int))
+    (h : cZ m x = cZ m y) : x = y := by
+  apply Hex.DensePoly.ext_coeff
+  intro i
+  have hi : ((x.coeff i : Int) : ZMod m.toNat) = ((y.coeff i : Int) : ZMod m.toNat) := by
+    have := congrArg (fun q => Polynomial.coeff q i) h
+    simpa [cZ_coeff] using this
+  have hcong : x.coeff i ≡ y.coeff i [ZMOD (m.toNat : Int)] :=
+    (ZMod.intCast_eq_intCast_iff _ _ _).mp hi
+  have hc : x.coeff i % (m.toNat : Int) = y.coeff i % (m.toNat : Int) := hcong
+  rwa [Int.emod_eq_of_lt (hx i).1 (hx i).2, Int.emod_eq_of_lt (hy i).1 (hy i).2] at hc
+
+open HexPolyMathlib in
+/-- Monic division commutes with a coefficient ring hom, in the target `T[X]`:
+the mapped executable quotient is the Mathlib monic-division quotient of the
+mapped inputs. Uniqueness (`div_modByMonic_unique`) does the work; the caller
+supplies the transported monic/degree facts. -/
+theorem map_divMod_monic {S : Type*} [CommRing S] [DecidableEq S] [Div S]
+    {T : Type*} [CommRing T] (φ : S →+* T)
+    (num g : Hex.DensePoly S)
+    (hcancel : ∀ a : S, a - a / g.leadingCoeff * g.leadingCoeff = (0 : S))
+    (hgmonic : (Polynomial.map φ (toPolynomial g)).Monic)
+    (hdegmap : (Polynomial.map φ (toPolynomial g)).degree = (toPolynomial g).degree)
+    (hdeg : (toPolynomial (Hex.DensePoly.divMod num g).2).degree < (toPolynomial g).degree) :
+    Polynomial.map φ (toPolynomial (Hex.DensePoly.divMod num g).1)
+      = Polynomial.map φ (toPolynomial num) /ₘ Polynomial.map φ (toPolynomial g) := by
+  have hrec : (Hex.DensePoly.divMod num g).1 * g + (Hex.DensePoly.divMod num g).2 = num :=
+    Hex.DensePoly.divMod_reconstruction num g hcancel
+  have hrec2 :
+      Polynomial.map φ (toPolynomial (Hex.DensePoly.divMod num g).1)
+          * Polynomial.map φ (toPolynomial g)
+        + Polynomial.map φ (toPolynomial (Hex.DensePoly.divMod num g).2)
+        = Polynomial.map φ (toPolynomial num) := by
+    have h := congrArg (Polynomial.map φ) (congrArg toPolynomial hrec)
+    simp only [toPolynomial_add, toPolynomial_mul, Polynomial.map_add, Polynomial.map_mul] at h
+    exact h
+  have hrec3 :
+      Polynomial.map φ (toPolynomial (Hex.DensePoly.divMod num g).2)
+        + Polynomial.map φ (toPolynomial g)
+            * Polynomial.map φ (toPolynomial (Hex.DensePoly.divMod num g).1)
+        = Polynomial.map φ (toPolynomial num) := by
+    rw [mul_comm, add_comm]; exact hrec2
+  have hrdeg :
+      (Polynomial.map φ (toPolynomial (Hex.DensePoly.divMod num g).2)).degree
+        < (Polynomial.map φ (toPolynomial g)).degree := by
+    calc (Polynomial.map φ (toPolynomial (Hex.DensePoly.divMod num g).2)).degree
+        ≤ (toPolynomial (Hex.DensePoly.divMod num g).2).degree := Polynomial.degree_map_le
+      _ < (toPolynomial g).degree := hdeg
+      _ = (Polynomial.map φ (toPolynomial g)).degree := hdegmap.symm
+  have huniq := Polynomial.div_modByMonic_unique
+    (Polynomial.map φ (toPolynomial (Hex.DensePoly.divMod num g).1))
+    (Polynomial.map φ (toPolynomial (Hex.DensePoly.divMod num g).2))
+    hgmonic ⟨hrec3, hrdeg⟩
+  exact huniq.1.symm
+
+end HexBerlekampZassenhausMathlib

From 4e9182edc7d282a51211ed47e5f54385d6ff8bf2 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@lean-fro.org>
Date: Fri, 10 Jul 2026 09:59:14 +0000
Subject: [PATCH 09/13] feat(bz-mathlib): coefficient bridges for the word CLD
 correspondence

Add the intCast-of-intModNat cast lemma, the cW-of-toW-mapped = cZ bridge, the
reduceModPow-vanishing lemma, and derivative-commute for both casts. With the
transport lemma these reduce the byte-identical CLD equality (#8691) to
numerator/divisor agreement in ZMod (p^a)[X] plus monic-division uniqueness.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
---
 HexBerlekampZassenhausMathlib/WordCld.lean | 63 ++++++++++++++++++++++
 1 file changed, 63 insertions(+)

diff --git a/HexBerlekampZassenhausMathlib/WordCld.lean b/HexBerlekampZassenhausMathlib/WordCld.lean
index a457e5ec4..264db1b2e 100644
--- a/HexBerlekampZassenhausMathlib/WordCld.lean
+++ b/HexBerlekampZassenhausMathlib/WordCld.lean
@@ -121,4 +121,67 @@ theorem map_divMod_monic {S : Type*} [CommRing S] [DecidableEq S] [Div S]
     hgmonic ⟨hrec3, hrdeg⟩
   exact huniq.1.symm
 
+/-! ### Coefficient bridges -/
+
+theorem intCast_intModNat (c : Int) (M : Nat) (hM : 0 < M) :
+    ((ZPoly.intModNat c M : Nat) : ZMod M) = (c : ZMod M) := by
+  have hM0 : (M : Int) ≠ 0 := by exact_mod_cast hM.ne'
+  have hnn : 0 ≤ c % (M : Int) := Int.emod_nonneg c hM0
+  have h1 : ((ZPoly.intModNat c M : Nat) : Int) = c % (M : Int) := by
+    rw [ZPoly.intModNat]
+    simp [Int.toNat_of_nonneg hnn]
+  calc ((ZPoly.intModNat c M : Nat) : ZMod M)
+      = (((ZPoly.intModNat c M : Nat) : Int) : ZMod M) := by rw [Int.cast_natCast]
+    _ = ((c % (M : Int) : Int) : ZMod M) := by rw [h1]
+    _ = (c : ZMod M) :=
+        (ZMod.intCast_eq_intCast_iff _ _ _).mpr (Int.emod_emod_of_dvd c (dvd_refl _))
+
+/-- `cW` of the `toW`-mapped image of an integer polynomial equals `cZ` of the
+original. -/
+theorem cW_toW_eq_cZ {m : UInt64} (ctx : _root_.MontCtx m) (x : Hex.ZPoly) :
+    cW ctx (Hex.DensePoly.ofCoeffs
+        (x.toArray.map (fun c => Hex.WordMod.ofNat (ZPoly.intModNat c m.toNat))))
+      = cZ m x := by
+  apply Polynomial.ext
+  intro j
+  rw [cW_coeff, cZ_coeff]
+  have htoW0 : Hex.WordMod.ofNat (ctx := ctx) (ZPoly.intModNat 0 m.toNat) = 0 := by
+    have : ZPoly.intModNat 0 m.toNat = 0 := by simp [ZPoly.intModNat]
+    rw [this]; rfl
+  have hcoeff : (Hex.DensePoly.ofCoeffs
+      (x.toArray.map (fun c => Hex.WordMod.ofNat (ctx := ctx) (ZPoly.intModNat c m.toNat)))).coeff j
+      = Hex.WordMod.ofNat (ctx := ctx) (ZPoly.intModNat (x.coeff j) m.toNat) := by
+    rw [Hex.DensePoly.coeff_ofCoeffs]
+    show (x.toArray.map (fun c => Hex.WordMod.ofNat (ctx := ctx) (ZPoly.intModNat c m.toNat))).getD j 0
+      = Hex.WordMod.ofNat (ctx := ctx) (ZPoly.intModNat (x.coeff j) m.toNat)
+    rw [show x.coeff j = x.toArray.getD j 0 from rfl]
+    simp only [Array.getD_eq_getD_getElem?, Array.getElem?_map]
+    cases x.toArray[j]? with
+    | none => simpa using htoW0.symm
+    | some v => simp
+  rw [hcoeff]
+  rw [show HexModArithMathlib.WordMod.toZMod
+        (Hex.WordMod.ofNat (ctx := ctx) (ZPoly.intModNat (x.coeff j) m.toNat))
+      = ((ZPoly.intModNat (x.coeff j) m.toNat : Nat) : ZMod m.toNat) from
+    HexModArithMathlib.WordMod.toZMod_natCast _]
+  exact intCast_intModNat (x.coeff j) m.toNat ctx.p_pos
+
+/-- Reduction mod `p^a` vanishes under the `ZMod (p^a)` cast. -/
+theorem cZ_reduceModPow {m : UInt64} {p a : Nat} (hpos : 0 < m.toNat) (hm : m.toNat = p ^ a)
+    (x : Hex.ZPoly) : cZ m (ZPoly.reduceModPow x p a) = cZ m x := by
+  apply Polynomial.ext
+  intro j
+  rw [cZ_coeff, cZ_coeff, ZPoly.coeff_reduceModPow, Int.ofNat_eq_natCast, Int.cast_natCast, ← hm]
+  exact intCast_intModNat (x.coeff j) m.toNat hpos
+
+/-- The `ZMod` cast commutes with the executable derivative. -/
+theorem cZ_derivative (m : UInt64) (x : Hex.ZPoly) :
+    cZ m (Hex.DensePoly.derivative x) = Polynomial.derivative (cZ m x) := by
+  simp only [cZ, HexPolyMathlib.toPolynomial_derivative, Polynomial.derivative_map]
+
+theorem cW_derivative {m : UInt64} (ctx : _root_.MontCtx m)
+    (a : Hex.DensePoly (Hex.WordMod ctx)) :
+    cW ctx (Hex.DensePoly.derivative a) = Polynomial.derivative (cW ctx a) := by
+  simp only [cW, HexPolyMathlib.toPolynomial_derivative, Polynomial.derivative_map]
+
 end HexBerlekampZassenhausMathlib

From 914812bb4dfc14972e1bbab36752870778b69bc1 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@lean-fro.org>
Date: Fri, 10 Jul 2026 10:02:43 +0000
Subject: [PATCH 10/13] feat(bz-mathlib): powLtWord? correctness and
 degree-transport helpers

Refactor powLtWord?'s inner loop into a named @[expose] powLtWordAux, prove it
computes p^a and stays below 2^64 (powLtWord?_eq), and add toPoly_degree_lt
transporting the dense remainder-degree bound into Polynomial.degree. These are
the last supporting lemmas before assembling the cldQuotientMod equality (#8691).

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
---
 HexBerlekampZassenhaus/WordCld.lean        | 22 +++++----
 HexBerlekampZassenhausMathlib/WordCld.lean | 55 ++++++++++++++++++++++
 2 files changed, 68 insertions(+), 9 deletions(-)

diff --git a/HexBerlekampZassenhaus/WordCld.lean b/HexBerlekampZassenhaus/WordCld.lean
index 2826465df..b9be3f73c 100644
--- a/HexBerlekampZassenhaus/WordCld.lean
+++ b/HexBerlekampZassenhaus/WordCld.lean
@@ -25,16 +25,20 @@ the correspondence proof is Phase 2, after which it is wired via `@[csimp]`.
 
 namespace Hex
 
-/-- `true` and the value `p^a` if `p^a < 2^64`, computed with early exit so a
-huge exponent never materialises a bignum. -/
+/-- Accumulating helper for `powLtWord?`: multiply `acc` by `p`, `n` times, with
+early exit if any partial product reaches `2^64`. -/
+@[expose]
+def powLtWordAux (p : Nat) : Nat → Nat → Option Nat
+  | 0, acc => some acc
+  | n + 1, acc =>
+      let next := acc * p
+      if next < UInt64.word then powLtWordAux p n next else none
+
+/-- `some (p^a)` if `p^a < 2^64`, computed with early exit so a huge exponent
+never materialises a bignum. -/
+@[expose]
 def powLtWord? (p a : Nat) : Option Nat :=
-  go a 1
-where
-  go : Nat → Nat → Option Nat
-    | 0, acc => some acc
-    | n + 1, acc =>
-        let next := acc * p
-        if next < UInt64.word then go n next else none
+  powLtWordAux p a 1
 
 /--
 Word-sized CLD quotient `(f · g') / g mod p^a` for monic `g`, computed over
diff --git a/HexBerlekampZassenhausMathlib/WordCld.lean b/HexBerlekampZassenhausMathlib/WordCld.lean
index 264db1b2e..b3e791ea0 100644
--- a/HexBerlekampZassenhausMathlib/WordCld.lean
+++ b/HexBerlekampZassenhausMathlib/WordCld.lean
@@ -184,4 +184,59 @@ theorem cW_derivative {m : UInt64} (ctx : _root_.MontCtx m)
     cW ctx (Hex.DensePoly.derivative a) = Polynomial.derivative (cW ctx a) := by
   simp only [cW, HexPolyMathlib.toPolynomial_derivative, Polynomial.derivative_map]
 
+/-! ### Guard correctness -/
+
+theorem powLtWord?_go_eq (p : Nat) : ∀ (n acc r : Nat),
+    Hex.powLtWordAux p n acc = some r → r = acc * p ^ n := by
+  intro n
+  induction n with
+  | zero =>
+      intro acc r h
+      simp only [Hex.powLtWordAux, Option.some.injEq] at h
+      subst h; simp
+  | succ k ih =>
+      intro acc r h
+      simp only [Hex.powLtWordAux] at h
+      by_cases hlt : acc * p < UInt64.word
+      · rw [if_pos hlt] at h
+        have := ih (acc * p) r h
+        rw [this]; ring
+      · rw [if_neg hlt] at h; exact absurd h (by simp)
+
+theorem powLtWord?_go_lt (p : Nat) : ∀ (n acc r : Nat),
+    acc < UInt64.word → Hex.powLtWordAux p n acc = some r → r < UInt64.word := by
+  intro n
+  induction n with
+  | zero =>
+      intro acc r hacc h
+      simp only [Hex.powLtWordAux, Option.some.injEq] at h
+      omega
+  | succ k ih =>
+      intro acc r _ h
+      simp only [Hex.powLtWordAux] at h
+      by_cases hlt : acc * p < UInt64.word
+      · rw [if_pos hlt] at h; exact ih (acc * p) r hlt h
+      · rw [if_neg hlt] at h; exact absurd h (by simp)
+
+theorem powLtWord?_eq {p a mval : Nat} (h : Hex.powLtWord? p a = some mval) :
+    mval = p ^ a ∧ mval < UInt64.word := by
+  have hgo : Hex.powLtWordAux p a 1 = some mval := h
+  refine ⟨?_, powLtWord?_go_lt p a 1 mval (by simp [UInt64.word]) hgo⟩
+  have := powLtWord?_go_eq p a 1 mval hgo
+  simpa using this
+
+/-! ### Degree transport -/
+
+open HexPolyMathlib in
+theorem toPoly_degree_lt {S : Type*} [CommRing S] [DecidableEq S] {r g : Hex.DensePoly S}
+    (hg0 : toPolynomial g ≠ 0)
+    (hlt : r.degree?.getD 0 < g.degree?.getD 0) :
+    (toPolynomial r).degree < (toPolynomial g).degree := by
+  by_cases hr : toPolynomial r = 0
+  · rw [hr, Polynomial.degree_zero]
+    exact bot_lt_iff_ne_bot.mpr (fun hb => hg0 (Polynomial.degree_eq_bot.mp hb))
+  · rw [Polynomial.degree_eq_natDegree hr, Polynomial.degree_eq_natDegree hg0,
+      natDegree_toPolynomial, natDegree_toPolynomial]
+    exact_mod_cast hlt
+
 end HexBerlekampZassenhausMathlib

From 9053f56b89199f816c233db2d434d87392059d65 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@lean-fro.org>
Date: Fri, 10 Jul 2026 10:06:17 +0000
Subject: [PATCH 11/13] refactor(bz-mathlib): extract toWMap and coeff_toWMap
 for the CLD assembly

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
---
 HexBerlekampZassenhausMathlib/WordCld.lean | 44 +++++++++++-----------
 1 file changed, 23 insertions(+), 21 deletions(-)

diff --git a/HexBerlekampZassenhausMathlib/WordCld.lean b/HexBerlekampZassenhausMathlib/WordCld.lean
index b3e791ea0..00f65a1c6 100644
--- a/HexBerlekampZassenhausMathlib/WordCld.lean
+++ b/HexBerlekampZassenhausMathlib/WordCld.lean
@@ -136,31 +136,33 @@ theorem intCast_intModNat (c : Int) (M : Nat) (hM : 0 < M) :
     _ = (c : ZMod M) :=
         (ZMod.intCast_eq_intCast_iff _ _ _).mpr (Int.emod_emod_of_dvd c (dvd_refl _))
 
+/-- The word-mapped executable image `toW = ofNat ∘ intModNat`. -/
+def toWMap {m : UInt64} (ctx : _root_.MontCtx m) (x : Hex.ZPoly) :
+    Hex.DensePoly (Hex.WordMod ctx) :=
+  Hex.DensePoly.ofCoeffs (x.toArray.map (fun c => Hex.WordMod.ofNat (ZPoly.intModNat c m.toNat)))
+
+theorem coeff_toWMap {m : UInt64} (ctx : _root_.MontCtx m) (x : Hex.ZPoly) (j : Nat) :
+    (toWMap ctx x).coeff j = Hex.WordMod.ofNat (ctx := ctx) (ZPoly.intModNat (x.coeff j) m.toNat) := by
+  have htoW0 : Hex.WordMod.ofNat (ctx := ctx) (ZPoly.intModNat 0 m.toNat) = 0 := by
+    have : ZPoly.intModNat 0 m.toNat = 0 := by simp [ZPoly.intModNat]
+    rw [this]; rfl
+  rw [toWMap, Hex.DensePoly.coeff_ofCoeffs]
+  show (x.toArray.map (fun c => Hex.WordMod.ofNat (ctx := ctx) (ZPoly.intModNat c m.toNat))).getD j 0
+    = Hex.WordMod.ofNat (ctx := ctx) (ZPoly.intModNat (x.coeff j) m.toNat)
+  rw [show x.coeff j = x.toArray.getD j 0 from rfl]
+  simp only [Array.getD_eq_getD_getElem?, Array.getElem?_map]
+  cases x.toArray[j]? with
+  | none => simpa using htoW0.symm
+  | some v => simp
+
 /-- `cW` of the `toW`-mapped image of an integer polynomial equals `cZ` of the
 original. -/
-theorem cW_toW_eq_cZ {m : UInt64} (ctx : _root_.MontCtx m) (x : Hex.ZPoly) :
-    cW ctx (Hex.DensePoly.ofCoeffs
-        (x.toArray.map (fun c => Hex.WordMod.ofNat (ZPoly.intModNat c m.toNat))))
-      = cZ m x := by
+theorem cW_toWMap_eq_cZ {m : UInt64} (ctx : _root_.MontCtx m) (x : Hex.ZPoly) :
+    cW ctx (toWMap ctx x) = cZ m x := by
   apply Polynomial.ext
   intro j
-  rw [cW_coeff, cZ_coeff]
-  have htoW0 : Hex.WordMod.ofNat (ctx := ctx) (ZPoly.intModNat 0 m.toNat) = 0 := by
-    have : ZPoly.intModNat 0 m.toNat = 0 := by simp [ZPoly.intModNat]
-    rw [this]; rfl
-  have hcoeff : (Hex.DensePoly.ofCoeffs
-      (x.toArray.map (fun c => Hex.WordMod.ofNat (ctx := ctx) (ZPoly.intModNat c m.toNat)))).coeff j
-      = Hex.WordMod.ofNat (ctx := ctx) (ZPoly.intModNat (x.coeff j) m.toNat) := by
-    rw [Hex.DensePoly.coeff_ofCoeffs]
-    show (x.toArray.map (fun c => Hex.WordMod.ofNat (ctx := ctx) (ZPoly.intModNat c m.toNat))).getD j 0
-      = Hex.WordMod.ofNat (ctx := ctx) (ZPoly.intModNat (x.coeff j) m.toNat)
-    rw [show x.coeff j = x.toArray.getD j 0 from rfl]
-    simp only [Array.getD_eq_getD_getElem?, Array.getElem?_map]
-    cases x.toArray[j]? with
-    | none => simpa using htoW0.symm
-    | some v => simp
-  rw [hcoeff]
-  rw [show HexModArithMathlib.WordMod.toZMod
+  rw [cW_coeff, cZ_coeff, coeff_toWMap,
+    show HexModArithMathlib.WordMod.toZMod
         (Hex.WordMod.ofNat (ctx := ctx) (ZPoly.intModNat (x.coeff j) m.toNat))
       = ((ZPoly.intModNat (x.coeff j) m.toNat : Nat) : ZMod m.toNat) from
     HexModArithMathlib.WordMod.toZMod_natCast _]

From 130cc76f2ccddfee52f9d1266200bf84db127d13 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@lean-fro.org>
Date: Fri, 10 Jul 2026 10:08:32 +0000
Subject: [PATCH 12/13] chore(bz): expose cldQuotientModWord? for the
 correspondence proof

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
---
 HexBerlekampZassenhaus/WordCld.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/HexBerlekampZassenhaus/WordCld.lean b/HexBerlekampZassenhaus/WordCld.lean
index b9be3f73c..322997d8c 100644
--- a/HexBerlekampZassenhaus/WordCld.lean
+++ b/HexBerlekampZassenhaus/WordCld.lean
@@ -45,6 +45,7 @@ Word-sized CLD quotient `(f · g') / g mod p^a` for monic `g`, computed over
 `WordMod` when the guard `Odd (p^a) ∧ p^a < 2^64` holds (`p` odd prime ⇒ `p^a`
 odd). Returns `none` when the guard fails, so the caller keeps the bignum path.
 -/
+@[expose]
 def cldQuotientModWord? (f g : ZPoly) (p a : Nat) : Option ZPoly :=
   match powLtWord? p a with
   | none => none

From a10075d67a4076c35f606ebee3ed267d884a6122 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@lean-fro.org>
Date: Fri, 10 Jul 2026 10:09:08 +0000
Subject: [PATCH 13/13] =?UTF-8?q?doc:=20progress=20note=20=E2=80=94=20issu?=
 =?UTF-8?q?e=20#8691=20Phase-2=20infrastructure=20complete?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
---
 progress/2026-07-10T00-00-00Z.md | 60 ++++++++++++++++++++++++++++++++
 1 file changed, 60 insertions(+)
 create mode 100644 progress/2026-07-10T00-00-00Z.md

diff --git a/progress/2026-07-10T00-00-00Z.md b/progress/2026-07-10T00-00-00Z.md
new file mode 100644
index 000000000..1d6f02c74
--- /dev/null
+++ b/progress/2026-07-10T00-00-00Z.md
@@ -0,0 +1,60 @@
+# issue #8691: Phase-2 infrastructure complete; main equality + Phase 3 remain
+
+## Accomplished
+
+PR https://github.com/kim-em/hex-dev/pull/8697 (branch `issue-8691`), all green,
+no `sorry`/`axiom`, CI-verified through commit c25cfb34:
+
+- Phase 1 `WordMod` proven Montgomery ring; Phase 1b `cldQuotientModWord?`
+  kernel + conformance `#guard`s byte-identical to `cldQuotientMod`.
+- Phase-2 algebraic backbone: `CommRing (WordMod)` + `toZModRingHom`.
+- **Phase-2 proof infrastructure** in `HexBerlekampZassenhausMathlib/WordCld.lean`:
+  - `cZ`/`cW` coefficient casts into `ZMod (p^a)[X]` + homomorphism laws.
+  - `eq_of_cZ_eq`: canonical-`[0,m)` uniqueness.
+  - `map_divMod_monic`: **the crux** — monic dense `divMod` commutes with any
+    coefficient ring hom (via `Polynomial.div_modByMonic_unique`).
+  - `intCast_intModNat`, `toWMap`/`coeff_toWMap`, `cW_toWMap_eq_cZ`,
+    `cZ_reduceModPow`, `cZ_derivative`/`cW_derivative`.
+  - `powLtWord?_eq` (guard computes `p^a`, `< 2^64`), `toPoly_degree_lt`.
+- `cldQuotientModWord?` and `powLtWordAux` are `@[expose]` for the proof.
+
+## Current frontier
+
+Only the main equality `cldQuotientModWord?_eq` and Phase 3 remain. Everything
+it needs is proven; it is assembly:
+
+`theorem cldQuotientModWord?_eq (f g) (p a) (hg : Monic g) (hgdeg) (hpow :
+powLtWord? p a = some mval) (hodd) (hm1 : 1 < mval) : cldQuotientModWord? f g p a
+= some (cldQuotientMod f g p a)`.
+
+Proof plan (each `have` uses a proven lemma):
+1. `powLtWord?_eq hpow` ⇒ `mval = p^a ∧ mval < 2^64`; `(ofNat mval).toNat = mval`.
+2. `rw [cldQuotientModWord?, hpow]; simp only [dif_pos hodd]; refine congrArg some ?_`.
+3. `eq_of_cZ_eq` reduces to (a) both outputs' coeffs in `[0, mval)` — from
+   `coeff_reduceModPow`/`WordMod.toNat_lt` — and (b) `cZ (word_output) = cZ (cldQuotientMod)`.
+4. For (b): `cZ word_output = cW qW` (a `coeff_toWMap`-style lemma for the
+   `toNat` map); `cW qW = cW numW /ₘ cW gW` via `map_divMod_monic` (word side);
+   `cZ (cldQuotientMod) = cZ numI /ₘ cZ g` via `cZ_reduceModPow` +
+   `map_divMod_monic` (Int side); `cZ numI = cW numW` and `cZ g = cW gW` via
+   `cW_toWMap_eq_cZ` + `cZ_mul`/`cZ_derivative`/`cW_mul`/`cW_derivative`.
+   The `map_divMod_monic` discharges need: `hcancel` (monic ⇒ leadingCoeff 1),
+   `hgmonic`/`hdegmap` (`leadingCoeff_toPolynomial` + `Monic.map` +
+   `degree_map_eq_of_leadingCoeff_ne_zero`, needs `Nontrivial (ZMod mval)` from
+   `hm1`), `hdeg` (`divMod_remainder_degree_lt_of_pos_degree_core` +
+   `toPoly_degree_lt`). Word side also needs `gW` monic + pos-degree, from
+   `coeff_toWMap` + `g` monic (`toW 1 = 1`).
+
+Then Phase 3: `cldQuotientModFast := if <odd ∧ 1<p^a ∧ Monic g ∧ 0<deg g> then
+(cldQuotientModWord? …).getD (cldQuotientMod …) else cldQuotientMod …`;
+`@[csimp] cldQuotientMod = cldQuotientModFast` (word branch via the equality
+theorem); re-measure `hex_lattice_spike` SD4.
+
+## Next step
+
+Write `cldQuotientModWord?_eq` per the plan (the fiddly parts are the modulus
+bookkeeping `mval = (ofNat mval).toNat = p^a` inside the kernel `let`s, and the
+`gW` monic/degree facts), then the `@[csimp]` wiring.
+
+## Blockers
+
+None technical; remaining is a large assembly proof, CI-gated.