feat(bz): word-sized Montgomery residue ring and CLD kernel#8697

Open

kim-em wants to merge 13 commits into

mainfrom

Commits on Jul 9, 2026

doc: progress note for issue #8691 measurement + re-scope session

Kim Morrison
and
claude
committed
feat(modarith): WordMod, a proven Montgomery residue ring over odd m < 2^64

Kim Morrison
and
claude
committed
feat(bz): word-sized Montgomery CLD kernel, byte-identical to cldQuotientMod

Kim Morrison
and
claude
committed
doc: progress note for issue #8691 Phases 1+1b (PR #8697)

Kim Morrison
and
claude
committed
feat(modarith-mathlib): WordMod-to-ZMod correspondence bridge

Kim Morrison
and
claude
committed
feat(modarith-mathlib): CommRing (WordMod) and RingHom to ZMod

Kim Morrison
and
claude
committed
doc: progress note for issue #8691 Phase-2 algebraic backbone

Kim Morrison
and
claude
committed
feat(bz-mathlib): Phase-2 transport infrastructure for the word CLD proof

Kim Morrison
and
claude
committed

Commits on Jul 10, 2026

feat(bz-mathlib): coefficient bridges for the word CLD correspondence

Kim Morrison
and
claude
committed
feat(bz-mathlib): powLtWord? correctness and degree-transport helpers

Kim Morrison
and
claude
committed
refactor(bz-mathlib): extract toWMap and coeff_toWMap for the CLD assembly

Kim Morrison
and
claude
committed
chore(bz): expose cldQuotientModWord? for the correspondence proof

Kim Morrison
and
claude
committed
doc: progress note — issue #8691 Phase-2 infrastructure complete

Kim Morrison
and
claude
committed