Reversible modular multiplication — semantic target + shift-and-add multiplier cost (ECDLP Tranche 3, Stage A)

Category: 1-Mathlib (CSD-free; staged as a Mathlib-upstream candidate).

The multiplication layer of the reversible-circuit substrate (Circuit.lean / Cost.lean / ModAdd.lean, specs/ecdlp-resource-plan.md). The semantic target is Shor's modular-multiplication oracle mulOracle : |y⟩ ↦ |a·y⟩ on ZMod N (a permutation when a is a unit), which the corpus's Empirical/QM/Algorithms/ShorCore.lean carries with no gate-level content. This tranche builds the missing reversible circuit + derived cost.

What is proved here (Stage A)

• mulConst — the semantic target: the ZMod N map y ↦ a · y, with mulConst_bijective (a unit acts as a permutation — the reversibility that lets a circuit realise it).
• multiplier — the shift-and-add multiplier as the concatenation of a list of partial-product adder circuits, with derived cost multiplier_toffoli / _cnot (the total count is the list-sum of the block counts, composed through the Tranche-1 cost_comp_* lemmas — not annotated).
• rippleCirc_toffoli / _cnot — a ripple adder block costs 2 * n Toffolis / CNOTs (derived), so a multiplier built from m width-n adders costs 2 * n * m (multiplier_ripple_toffoli).
• The per-partial-product correctness is ModAdd.rippleCirc_correct (one shifted add); the building block is in hand.

Stage B.1 — the per-step accumulation correctness (landed below)

• regValRange_split — split a register readout at an offset (low + 2^i · window), the tool relating a windowed add to the full accumulator value with no division.
• rippleCirc_preserves_external — a ripple circuit preserves any wire disjoint from its layout (the frame lemma at circuit granularity).
• accStep — THE per-step heart: one full-remaining-width ripple add of the multiplicand (value Yv) into the accumulator window Acc[i, W) increases the full accumulator value by exactly 2^i · Yv (carry propagating through the whole upper accumulator; low i bits preserved; no overflow).

Stage B.2 — the fold to Acc = a · Y (landed below)

• MulLayout — the multi-register wire geometry (accumulator, multiplicand with high bits held zero, per-shift carry chains; bounded injectivity/disjointness, so it is inhabitable — see mulLayout1).
• mulCircuit — the shift-and-add multiplier: one partial-product ripple add per shift in shifts.
• mulCircuit_correct — THE headline: the multiplier leaves the accumulator holding Acc + (∑ sh ∈ shifts, 2^sh) · Y, by folding accStep over the shifts (an induction threading Y-preservation via stepLayout_preserves_Y and carry-freshness via stepLayout_preserves_carry; each step at its own width W - sh, applied individually so there is no dependent-width fold). With Acc initialised 0 and ∑ 2^sh = a (the set bits of the classical constant), this is Acc = a · Y.
• mulLayout1 + the closing example — a concrete Fin 6 witness, so the headline is non-vacuous.

Stage B.3 — the modular (ZMod N) capstone (landed below)

• mulCircuit_correct_zmod — connects the exact integer product to the semantic target: the output register, read in ZMod N, is mulConst N (∑ 2^sh) Y (Shor's mulOracle action y ↦ a·y mod N). The ZMod N cast performs the reduction (no N = 2^W assumption); the no-overflow hypothesis keeps the register exact. Honest residue: the register holds the exact integer a·Y — reducing it in place to a bitlen N-bit representative is a reversible conditional-subtract circuit (qubit optimisation), not built here.

Semantic target: the ZMod N multiplication oracle

def Reversible.mulConst (N : ℕ) (a : ZMod N) : ZMod N → ZMod N

The modular-multiplication oracle action: y ↦ a · y on ZMod N. This is the permutation Shor's mulOracle realises (for a a unit); the circuit below is its reversible implementation.

Equations

• Reversible.mulConst N a y = a * y

theorem Reversible.mulConst_bijective {N : ℕ} {a : ZMod N} (ha : IsUnit a) : Function.Bijective (mulConst N a)

For a unit a, mulConst is a bijection (the reversibility that admits a reversible circuit): its inverse is multiplication by a⁻¹.

The shift-and-add multiplier circuit and its derived cost

def Reversible.multiplier {m : ℕ} (adders : List (Circuit m)) : Circuit m

The shift-and-add multiplier: the concatenation of a list of partial-product adder circuits. Each entry is the circuit that adds one shifted copy of the multiplicand into the accumulator; the multiplier is their composition. (Which adders appear is fixed by the classical constant a — its set bits — so no quantum control is needed; the gate list, hence the cost, is determined.)

Equations

• Reversible.multiplier adders = List.flatMap id adders

@[simp]

theorem Reversible.multiplier_nil {m : ℕ} : multiplier [] = []

theorem Reversible.multiplier_toffoli {m : ℕ} (adders : List (Circuit m)) : (circuitCost (multiplier adders)).toffoli = (List.map (fun (c : Circuit m) => (circuitCost c).toffoli) adders).sum

Multiplier Toffoli count is the sum of the block counts (derived, composed through the Tranche-1 cost_comp_toffoli_count). Not annotated — read off the concatenated gate list.

theorem Reversible.multiplier_cnot {m : ℕ} (adders : List (Circuit m)) : (circuitCost (multiplier adders)).cnot = (List.map (fun (c : Circuit m) => (circuitCost c).cnot) adders).sum

Multiplier CNOT count is the sum of the block counts (derived).

theorem Reversible.ripplePrefix_toffoli {m n : ℕ} (L : RippleLayout m n) (k : ℕ) : (circuitCost (ripplePrefix L k)).toffoli = 2 * k

The first k slices of a ripple adder cost 2 * k Toffolis (derived, induction on k composing cost_comp_toffoli_count + fullAdder_toffoli).

theorem Reversible.rippleCirc_toffoli {m n : ℕ} (L : RippleLayout m n) : (circuitCost (rippleCirc L)).toffoli = 2 * n

A ripple adder block (n slices) costs 2 * n Toffolis (derived).

theorem Reversible.multiplier_ripple_toffoli {m n : ℕ} (Ls : List (RippleLayout m n)) : (circuitCost (multiplier (List.map rippleCirc Ls))).toffoli = 2 * n * Ls.length

A multiplier built from m' width-n ripple-adder blocks costs 2 * n * m' Toffolis (derived). The count is independent of whether the layouts are valid (disjoint-wire) — cost is syntactic, so this is a cost statement, not a correctness one; the multiplier's correctness is Stage B.

Stage B: multiplication correctness — arithmetic tools

theorem Reversible.regValRange_split {m : ℕ} (f : ℕ → Fin m) (s : State m) (i k : ℕ) (h : i ≤ k) : regValRange f s k = regValRange f s i + 2 ^ i * regValRange (fun (j : ℕ) => f (i + j)) s (k - i)

Split a register readout at an offset. The low-i value plus 2^i times the value of the window starting at i. The key tool relating a windowed add to the full accumulator value (no division).

theorem Reversible.rippleCirc_preserves_external {m w : ℕ} (L : RippleLayout m w) (s : State m) (x : Fin m) (hA : ∀ k < w, x ≠ L.A k) (hB : ∀ k < w, x ≠ L.B k) (hC : ∀ k < w + 1, x ≠ L.C k) : denote (rippleCirc L) s x = s x

A ripple circuit preserves any wire external to its layout (disjoint from all of A, B, C). The frame lemma at circuit granularity, lifting denote_apply_of_forall_not_mem: every gate of rippleCirc L has wires among L.A, L.B, L.C, so a wire avoiding all three is untouched.

theorem Reversible.accStep {m w : ℕ} (L : RippleLayout m w) (Acc : ℕ → Fin m) (s : State m) (i W : ℕ) (hw : w = W - i) (hiW : i ≤ W) (hB : ∀ (k : ℕ), L.B k = Acc (i + k)) (hAccinj : ∀ (j k : ℕ), j < W → k < W → Acc j = Acc k → j = k) (hAccA : ∀ j < i, ∀ (k : ℕ), Acc j ≠ L.A k) (hAccC : ∀ j < i, ∀ (k : ℕ), Acc j ≠ L.C k) (hcarry : ∀ (j : ℕ), s (L.C j) = false) (Yv : ℕ) (hYv : regValRange L.A s w = Yv) (hno : Yv + regValRange (fun (k : ℕ) => Acc (i + k)) s w < 2 ^ w) : regValRange Acc (denote (rippleCirc L) s) W = regValRange Acc s W + 2 ^ i * Yv

Single accumulation step. One full-remaining-width ripple add of the multiplicand (value Yv, read by L.A) into the accumulator window Acc[i, W) increases the full accumulator value by 2^i · Yv — provided the add does not overflow the window. The carry propagates through the whole upper accumulator (width w = W - i), so nothing is dropped; the low i bits are preserved.

Stage B.2: the fold to Acc = a · Y

A MulLayout lays out, on Fin M, the accumulator Acc (W wires), the multiplicand Y (a W-wire register whose high bits [n, W) are held zero, so no separate addend-pad wires are needed), and a per-shift carry chain Carry sh. The multiplier is the concatenation, over a list of shifts (the set bits of the classical constant a), of one full-window ripple add of Y into Acc[sh, W) per shift. Folding accStep over the shifts gives Acc ← Acc + (∑ 2^sh) · Y. Each step has its own width W - sh, but the steps are applied individually (the circuits are all Circuit M), so there is no dependent-width fold.

structure Reversible.MulLayout (M n W : ℕ) : Type

A multiplier layout on Fin M: accumulator Acc, multiplicand Y (high bits held zero), and a per-shift carry chain Carry. The fields are pure wire geometry (disjointness + injectivity).

• Acc : ℕ → Fin M

  Accumulator wires (indices [0, W)).

• Y : ℕ → Fin M

  Multiplicand wires (a W-wire register; values live in [0, n), high bits held zero).

• Carry : ℕ → ℕ → Fin M

  Carry chain for the partial-product add at shift sh.

• hYAcc (i j : ℕ) : self.Y i ≠ self.Acc j
• hYCarry (i sh j : ℕ) : self.Y i ≠ self.Carry sh j
• hAccCarry (i sh j : ℕ) : self.Acc i ≠ self.Carry sh j
• hCarryCross (sh sh' i j : ℕ) : sh ≤ W → sh' ≤ W → sh ≠ sh' → self.Carry sh i ≠ self.Carry sh' j
• hAccInj (i j : ℕ) : i < W → j < W → self.Acc i = self.Acc j → i = j
• hYInj (i j : ℕ) : i < W → j < W → self.Y i = self.Y j → i = j
• hCarryInj (sh i j : ℕ) : i ≤ W → j ≤ W → self.Carry sh i = self.Carry sh j → i = j

def Reversible.stepLayout {m n W : ℕ} (L : MulLayout m n W) (sh : ℕ) : RippleLayout m (W - sh)

The ripple-adder layout for the partial product at shift sh: add the multiplicand Y (the low window) into the accumulator window Acc[sh, W) (width W - sh), with carry chain Carry sh.

Equations

• Reversible.stepLayout L sh = { A := L.Y, B := fun (k : ℕ) => L.Acc (sh + k), C := L.Carry sh, hAB := ⋯, hAC := ⋯, hBC := ⋯, hAinj := ⋯, hBinj := ⋯, hCinj := ⋯ }

def Reversible.mulCircuit {m n W : ℕ} (L : MulLayout m n W) (shifts : List ℕ) : Circuit m

The shift-and-add multiplier circuit: one partial-product ripple add per shift in shifts.

Equations

• Reversible.mulCircuit L shifts = Reversible.multiplier (List.map (fun (sh : ℕ) => Reversible.rippleCirc (Reversible.stepLayout L sh)) shifts)

theorem Reversible.regValRange_eq_of_high_zero {m : ℕ} (f : ℕ → Fin m) (s : State m) (n k : ℕ) (hnk : n ≤ k) (hz : ∀ (j : ℕ), n ≤ j → j < k → s (f j) = false) : regValRange f s k = regValRange f s n

A register readout over [0, k) equals its readout over [0, n) when bits [n, k) are zero.

theorem Reversible.stepLayout_preserves_Y {m n W : ℕ} (L : MulLayout m n W) (sh : ℕ) (s : State m) (hcarry : ∀ (k : ℕ), s (L.Carry sh k) = false) (j : ℕ) (hj : j < W) : denote (rippleCirc (stepLayout L sh)) s (L.Y j) = s (L.Y j)

A partial-product step preserves the multiplicand Y (the addend wires are read-only; the wires beyond the window are external).

theorem Reversible.stepLayout_preserves_carry {m n W : ℕ} (L : MulLayout m n W) (sh sh' : ℕ) (hshW : sh ≤ W) (hsh'W : sh' ≤ W) (hne : sh' ≠ sh) (s : State m) (k : ℕ) : denote (rippleCirc (stepLayout L sh)) s (L.Carry sh' k) = s (L.Carry sh' k)

A partial-product step at shift sh preserves the carry chain of any other shift sh' ≠ sh.

theorem Reversible.mulCircuit_correct {m n W : ℕ} (L : MulLayout m n W) (shifts : List ℕ) : shifts.Nodup → (∀ sh ∈ shifts, sh + n ≤ W) → ∀ (s : State m) (Yv : ℕ), (∀ sh ∈ shifts, ∀ (k : ℕ), s (L.Carry sh k) = false) → (∀ (j : ℕ), n ≤ j → j < W → s (L.Y j) = false) → regValRange L.Y s n = Yv → regValRange L.Acc s W + (List.map (fun (x : ℕ) => 2 ^ x) shifts).sum * Yv < 2 ^ W → regValRange L.Acc (denote (mulCircuit L shifts) s) W = regValRange L.Acc s W + (List.map (fun (x : ℕ) => 2 ^ x) shifts).sum * Yv

Multiplier correctness (Stage B.2 headline). The shift-and-add multiplier over shifts (the set bits of the classical constant a) leaves the accumulator holding Acc + (∑ 2^sh) · Y, provided the carries start false, Y's high bits are zero, and the result does not overflow 2^W. With Acc initialised to 0 and ∑ 2^sh = a, this is Acc = a · Y.

Non-vacuity witness

A concrete MulLayout showing the structure is inhabited (the bounded injectivity/disjointness fields are jointly satisfiable in finitely many wires) and mulCircuit_correct applies. Accumulator on wire 0, multiplicand on wire 1, and two disjoint carry banks ({2,3} for shift 0, {4,5} for shift 1) so the cross-shift disjointness hCarryCross is non-vacuous.

def Reversible.mulLayout1 : MulLayout 6 1 1

A concrete 1-bit multiplier layout on Fin 6 (n = W = 1): accumulator wire 0, multiplicand wire 1, carry banks {2,3} (shift 0) and {4,5} (shift 1), via the arithmetic encoding Carry sh k = 2 + 2·min sh 1 + min k 1 (no case split — every field proof is omega).

Equations

• One or more equations did not get rendered due to their size.

Stage B.3: the modular (ZMod N) connection — the multiplier realises mulConst

mulCircuit_correct gives the exact integer product a · Y in the W-bit accumulator (no overflow). The Shor mulOracle action is y ↦ a · y on ZMod N (mulConst), and that is precisely the accumulator's value cast into ZMod N — the cast performs the mod N reduction, with no N = 2^W assumption and no truncation hypothesised away (the no-overflow hypothesis guarantees the register holds the exact integer; the ZMod N cast then reduces it honestly).

Honest scope: the accumulator physically holds the exact integer a · Y (W bits, W chosen large enough — for Shor W ≥ 2·bitlen N, since a, y < N ⇒ a·y < N²); its ZMod N interpretation is the oracle action. Reducing the register in place to a bitlen N-bit representative of a·y mod N is a reversible modular-reduction circuit (conditional-subtract), a qubit-count optimisation not built here.

theorem Reversible.mulCircuit_correct_zmod {m n W : ℕ} (N : ℕ) (L : MulLayout m n W) (shifts : List ℕ) (s : State m) (Yv : ℕ) (hnd : shifts.Nodup) (hsh : ∀ sh ∈ shifts, sh + n ≤ W) (hcarry : ∀ sh ∈ shifts, ∀ (k : ℕ), s (L.Carry sh k) = false) (hYhigh : ∀ (j : ℕ), n ≤ j → j < W → s (L.Y j) = false) (hYv : regValRange L.Y s n = Yv) (hAcc0 : regValRange L.Acc s W = 0) (hbound : (List.map (fun (x : ℕ) => 2 ^ x) shifts).sum * Yv < 2 ^ W) : ↑(regValRange L.Acc (denote (mulCircuit L shifts) s) W) = mulConst N ↑(List.map (fun (x : ℕ) => 2 ^ x) shifts).sum ↑Yv

Modular-multiplication correctness (Tranche 3 capstone). With the accumulator initialised 0 and no overflow, the shift-and-add multiplier's output register, read in ZMod N, is the mulConst (modular-multiplication) action (∑ 2^sh) · Y. For ∑ 2^sh = a this is Shor's mulOracle action y ↦ a · y mod N.