Reversible interleaved modular multiply — the general-n Horner LOOP (ECDLP Phase 2, Stage S6.3d-2b)

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

This module delivers the verified general-n interleaved MSB-first modular multiply over 𝔽_p, folding the verified Horner loop body (hornerStep, S6.3d-2a) over all n bits of the multiplier X to leave the accumulator holding X · Y mod N. It is the capstone of the modular-arithmetic chain: the verified field-multiply atom ⟦c⟧ = (· * Yval) mod N an exhibited EC point op would call.

mulLoop L = ((List.range n).map (fun j => hornerStep (L.bank j))).flatMap id

processing bits MSB-first: loop index j = 0, …, n-1 runs hornerStep on bank j, whose control is bound to X (n-1-j) — the (n-1-j)-th bit of the multiplier. Each body is one verified Horner step acc ← (2·acc + [X_{n-1-j}]·Y) mod N (hornerStep_correct). The banks share the accumulator B and the multiplicand Y; every other wire of each bank is FRESH and disjoint (the Θ(n²)-ancilla fresh-wire model inherited from S6.3d-1 / S6.3c).

The invariant (induction over the processed-bank prefix)

After processing banks [0, …, k-1] from acc = 0, the accumulator holds hornerVal k · Yval mod N, where hornerVal k is the top-k-bits-of-X MSB-first reconstruction (hornerVal 0 = 0, hornerVal (k+1) = 2·hornerVal k + bit (n-1-k)). The step k → k+1 is exactly the per-step reasoning of mulStep2_correct: hornerStep_correct on bank k maps (hornerVal k · Yval) mod N to ((2·hornerVal k + bit)·Yval) mod N = (hornerVal (k+1) · Yval) mod N; hornerStep_preserves_Y keeps Y; hornerStep_preserves_external keeps the later banks' wires clean and the not-yet-read X bits intact. The bridge hornerVal n = Xval (hornerVal_full) closes it.

Carve line (what this is, and is NOT)

This is the VERIFIED modular field-multiply X · Y mod N — the ⟦c⟧ = op payoff of the S6.3 Option-1 route — composing the verified Horner step (S6.3d-2a) over all n bits.

Named residue:

1. Fresh per-iteration wires ⟹ Θ(n²) qubits + Θ(n²) Toffoli. Each of the n Horner steps is supplied its OWN doubling scratch / carries / ancilla and controlled-add carries / ancilla, disjoint from every other step's. This is the honest fresh-ancilla cost. In-place reuse (Θ(n) qubits) needs the carry-clean / ancilla-restoring adder the corpus does NOT yet provide (Cuccaro-style inline carry-uncompute, or the self-cleaning high-bit modular adder). That carry-clean adder is the genuine orthogonal residue.
2. This is NOT the EC point operation. It is the verified modular MULTIPLY over registers (X · Y mod N), ℕ / mod N bit arithmetic — no field / group semantics. Assembling these field-multiplies into the full elliptic-curve point op (point add / double) is S6.3e+, NOT built here. And this is the Θ(n²)-qubit version, not the optimised in-place one.

Honest cost

mulLoop_toffoli derives 30 * n² Toffolis: n Horner steps, each 30n (hornerStep_toffoli), composed through cost_comp_toffoli_count over the fold (multiplier_toffoli).

The Horner reconstruction value (pure ℕ)

hornerVal bits n k is the top-k-bits MSB-first reconstruction of the n-bit number whose bits are bits 0, …, bits (n-1) (each bits i ∈ {0,1} for the intended use, but the lemmas hold for any bits). The bridge hornerVal_full (hornerVal bits n n = ∑_{i<n} bits i · 2^i) lets the loop's per-step recurrence land on the full multiplier value.

def Reversible.hornerVal (bits : ℕ → ℕ) (n : ℕ) : ℕ → ℕ

Top-k-bits MSB-first reconstruction: hornerVal bits n 0 = 0, hornerVal bits n (k+1) = 2 · hornerVal bits n k + bits (n-1-k).

Equations

• Reversible.hornerVal bits n 0 = 0
• Reversible.hornerVal bits n k.succ = 2 * Reversible.hornerVal bits n k + bits (n - 1 - k)

@[simp]

theorem Reversible.hornerVal_zero (bits : ℕ → ℕ) (n : ℕ) : hornerVal bits n 0 = 0

theorem Reversible.hornerVal_succ (bits : ℕ → ℕ) (n k : ℕ) : hornerVal bits n (k + 1) = 2 * hornerVal bits n k + bits (n - 1 - k)

theorem Reversible.hornerVal_aux (bits : ℕ → ℕ) (n k : ℕ) : k ≤ n → hornerVal bits n k * 2 ^ (n - k) + ∑ i ∈ Finset.range (n - k), bits i * 2 ^ i = ∑ i ∈ Finset.range n, bits i * 2 ^ i

The Horner-reconstruction bridge (auxiliary, all prefixes). For k ≤ n, the top-k-bits reconstruction times 2^(n-k), plus the bottom n-k bits in place value, is the full value.

theorem Reversible.hornerVal_full (bits : ℕ → ℕ) (n : ℕ) : hornerVal bits n n = ∑ i ∈ Finset.range n, bits i * 2 ^ i

The Horner-reconstruction bridge. The full n-bit MSB-first reconstruction equals the place-value sum ∑_{i<n} bits i · 2^i. Specialised from hornerVal_aux at k = n.

theorem Reversible.regValRange_eq_hornerVal_bits {m : ℕ} (X : ℕ → Fin m) (s : State m) (n : ℕ) : regValRange X s n = hornerVal (fun (i : ℕ) => if s (X i) = true then 1 else 0) n n

The control-bit indicator bit i = if s (X i) then 1 else 0, as a ℕ. The place-value sum of these indicators over [0, n) is exactly regValRange X s n.

The n-bank multiply-loop layout

A MulLoopLayout bundles n per-bit HornerStepLayout banks (bank j, S6.3d-2a), all sharing the accumulator B ((bank j).B = B) and the multiplicand Y ((bank j).Y = Y), with bank j's control bound to X (n-1-j) (MSB-first). The inter-bank geometry needed to fold the steps — bank j's circuit must not touch any of bank k's clean / preset wires (k ≠ k), nor the not-yet-read control bits — is carried by the membership-based footprints Touches / Clean and the single disjointness field hInter. This is bounded and inhabitable for every n (no unbounded ℕ → Fin m injectivity field): the witness assigns each bank a disjoint contiguous block of fresh wires and discharges hInter / hCtrl* by omega, and Touches/Clean are decidable finite disjunctions over the 18/14 families.

Touches L j w holds iff w is one of bank j's 18 touched wire families; Clean L k w iff w is one of bank k's 14 clean/preset families (the ones whose initial value bank k's hornerStep_correct reads). The field hInter says: for j ≠ k, a clean wire of bank k is not touched by bank j — which is exactly what hornerStep_preserves_external needs to transport bank k's preconditions through bank j's step.

def Reversible.Touches {m n : ℕ} (L : ℕ → HornerStepLayout m n) (j : ℕ) (w : Fin m) : Prop

The 18 wire families bank j's hornerStep circuit touches (writes or reads), as a membership predicate over wires. (The doubling block's B is the shared accumulator, listed once via add.B.)

Equations

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

def Reversible.Clean {m n : ℕ} (L : ℕ → HornerStepLayout m n) (k : ℕ) (w : Fin m) : Prop

The 14 wire families bank k's hornerStep_correct reads as a clean / preset precondition: the doubling scratch / carries / ancilla / presets and the controlled-add carries / ancilla / presets. (The shared B, Y and the control bit are handled separately.)

Equations

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

structure Reversible.MulLoopLayout (m n : ℕ) : Type

An n-bank modular-multiply loop layout on Fin m. The n banks share B and Y; bank j's control is X (n-1-j); bank j does not touch bank k's clean wires for k ≠ j (hInter), nor any control bit X i other than its own (hCtrlTouch), and X/B/Y registers are injective on [0,n). All hypotheses are bounded (< n), so the schema is inhabitable for every n.

• bank : ℕ → HornerStepLayout m n

  The n per-bit Horner-step banks (bank j processes bit n-1-j).

• X : ℕ → Fin m

  Shared multiplier (control) register X; bank j reads bit X (n-1-j).

• hBshare (j j' : ℕ) : (self.bank j).B = (self.bank j').B

  Sharing: every bank acts on the same accumulator B.

• hYshare (j j' : ℕ) : (self.bank j).Y = (self.bank j').Y

  Sharing: every bank reads the same multiplicand Y.

• hctrl (j : ℕ) : (self.bank j).ctrl = self.X (n - 1 - j)

  Bank j's control bit is X (n-1-j).

• hInter (j k : ℕ) (w : Fin m) : j < n → k < n → j ≠ k → Clean self.bank k w → ¬Touches self.bank j w

  Inter-bank disjointness: for j ≠ k, bank j's circuit does not touch bank k's clean wires.

• hCtrlTouch (j i : ℕ) : j < n → i < n → i ≠ n - 1 - j → ¬Touches self.bank j (self.X i)

  Bank j's circuit does not touch the control bit X i unless i = n-1-j (its own).

• hXinj (i i' : ℕ) : i < n → i' < n → self.X i = self.X i' → i = i'

  The control register is injective on [0, n).

def Reversible.MulLoopLayout.B {m n : ℕ} (L : MulLoopLayout m n) : ℕ → Fin m

The shared accumulator register (B of bank 0).

Equations

• L.B = (L.bank 0).B

def Reversible.MulLoopLayout.Y {m n : ℕ} (L : MulLoopLayout m n) : ℕ → Fin m

The shared multiplicand register (Y of bank 0).

Equations

• L.Y = (L.bank 0).Y

theorem Reversible.notTouches_preserved {m n : ℕ} (L : MulLoopLayout m n) (j : ℕ) (s : State m) (w : Fin m) (hw : ¬Touches L.bank j w) : denote (hornerStep (L.bank j)) s w = s w

A wire not touched by bank j survives bank j's Horner step. (The Touches predicate lists exactly the 18 families hornerStep_preserves_external requires disjointness from.)

theorem Reversible.bank_step_preserves_clean {m n : ℕ} (L : MulLoopLayout m n) (j k : ℕ) (hj : j < n) (hk : k < n) (hjk : j ≠ k) (s : State m) (w : Fin m) (hw : Clean L.bank k w) : denote (hornerStep (L.bank j)) s w = s w

A clean wire of bank k survives bank j's Horner step (j ≠ k, both < n): by hInter it is not touched, so notTouches_preserved applies. The 14 Clean-membership constructors are unfolded at each call site (the mulLoop_invariant step transports bank k's preconditions through bank j).

theorem Reversible.horner_mod_step (H Yval N : ℕ) (b : Bool) : (2 * (H * Yval % N) + if b = true then Yval else 0) % N = (2 * H + if b = true then 1 else 0) * Yval % N

The Horner arithmetic step. Folding one MSB-first Horner digit through the running residue: (2·((H·Y) mod N) + [bit]·Y) mod N = ((2·H + [bit])·Y) mod N, i.e. the value hornerStep_correct produces from c = (H·Y) mod N is (hornerVal-next · Y) mod N. (Nat.add_mod / Nat.mul_mod absorb the inner reduction; the if is the 0/1 digit.)

The general-n multiply loop and its correctness

def Reversible.mulLoop {m n : ℕ} (L : MulLoopLayout m n) : Circuit m

The general-n modular-multiply loop. Process the multiplier bits MSB-first: bank j (j = 0, …, n-1) runs one verified Horner step acc ← (2·acc + [X_{n-1-j}]·Y) mod N. The banks share the accumulator B and the multiplicand Y; every other wire is fresh.

Equations

• Reversible.mulLoop L = List.flatMap id (List.map (fun (j : ℕ) => Reversible.hornerStep (L.bank j)) (List.range n))

def Reversible.mulLoopUpto {m n : ℕ} (L : MulLoopLayout m n) (k : ℕ) : Circuit m

The first k banks of the loop (prefix [0, …, k-1]), the induction handle for mulLoop.

Equations

• Reversible.mulLoopUpto L k = List.flatMap id (List.map (fun (j : ℕ) => Reversible.hornerStep (L.bank j)) (List.range k))

@[simp]

theorem Reversible.mulLoopUpto_zero {m n : ℕ} (L : MulLoopLayout m n) : mulLoopUpto L 0 = []

theorem Reversible.mulLoop_eq_upto {m n : ℕ} (L : MulLoopLayout m n) : mulLoop L = mulLoopUpto L n

theorem Reversible.mulLoopUpto_succ {m n : ℕ} (L : MulLoopLayout m n) (k : ℕ) : mulLoopUpto L (k + 1) = mulLoopUpto L k ++ hornerStep (L.bank k)

Split the prefix at its last bank: mulLoopUpto L (k+1) = mulLoopUpto L k ++ hornerStep (bank k) (bank k runs LAST). From List.range_succ.

theorem Reversible.mulLoopUpto_preserves {m n : ℕ} (L : MulLoopLayout m n) (k : ℕ) (s : State m) (w : Fin m) (hw : ∀ j < k, ¬Touches L.bank j w) : denote (mulLoopUpto L k) s w = s w

Prefix frame. A wire not touched by any bank j < k survives the whole prefix mulLoopUpto L k (fold of notTouches_preserved).

Preservation of bank k's preconditions through the prefix

Every clean / preset wire of bank k lies in Clean L.bank k, so (for k ≤ n and the prefix length ≤ k) it is untouched by every earlier bank j < k (hInter) and survives mulLoopUpto. The control bit X (n-1-k) survives via hCtrlTouch. These are the lemmas the invariant's step consumes.

theorem Reversible.clean_pres {m n : ℕ} (L : MulLoopLayout m n) {k p : ℕ} (hk : k < n) (hpk : p ≤ k) (s : State m) (w : Fin m) (hw : Clean L.bank k w) : denote (mulLoopUpto L p) s w = s w

theorem Reversible.clean_pres_reg {m n : ℕ} (L : MulLoopLayout m n) {k p : ℕ} (hk : k < n) (hpk : p ≤ k) (s : State m) (f : ℕ → Fin m) (hf : ∀ (i : ℕ), Clean L.bank k (f i)) (q : ℕ) : regValRange f (denote (mulLoopUpto L p) s) q = regValRange f s q

theorem Reversible.mulLoop_invariant {m n : ℕ} (L : MulLoopLayout m n) (s : State m) {N Yval : ℕ} (h2N : 2 * N ≤ 2 ^ n) (hNpos : 0 < N) (hYN : Yval < N) (hB0 : regValRange L.B s n = 0) (hYv : regValRange L.Y s n = Yval) (hcleanAop : ∀ (j i : ℕ), j < n → i < n → s ((L.bank j).dbl.Aop i) = false) (hcleanCadd : ∀ (j i : ℕ), j < n → s ((L.bank j).dbl.addLayout.Cadd i) = false) (hcleandC1 : ∀ (j i : ℕ), j < n → s ((L.bank j).dbl.addLayout.C1 i) = false) (hcleandC2 : ∀ (j i : ℕ), j < n → s ((L.bank j).dbl.addLayout.C2 i) = false) (hcleandanc : ∀ j < n, s (L.bank j).dbl.addLayout.anc = false) (hcleanCcadd : ∀ (j i : ℕ), j < n → s ((L.bank j).add.Ccadd i) = false) (hcleanancC : ∀ j < n, s (L.bank j).add.ancC = false) (hcleanC1 : ∀ (j i : ℕ), j < n → s ((L.bank j).add.C1 i) = false) (hcleanC2 : ∀ (j i : ℕ), j < n → s ((L.bank j).add.C2 i) = false) (hcleananc : ∀ j < n, s (L.bank j).add.anc = false) (hA1dbl : ∀ j < n, regValRange (L.bank j).dbl.addLayout.A1 s n = 2 ^ n - N) (hA2dbl : ∀ j < n, regValRange (L.bank j).dbl.addLayout.A2 s n = N) (hA1add : ∀ j < n, regValRange (L.bank j).add.A1 s n = 2 ^ n - N) (hA2add : ∀ j < n, regValRange (L.bank j).add.A2 s n = N) (k : ℕ) : k ≤ n → regValRange L.B (denote (mulLoopUpto L k) s) n = hornerVal (fun (i : ℕ) => if s (L.X i) = true then 1 else 0) n k * Yval % N ∧ regValRange L.Y (denote (mulLoopUpto L k) s) n = Yval

The multiply-loop invariant. After the first k banks (k ≤ n), the accumulator holds (hornerVal bits n k · Yval) mod N (bits i = [X i]) and the multiplicand still holds Yval. By induction on k, splitting the last bank (mulLoopUpto_succ): the prefix preserves bank k's clean / preset wires (clean_pres) and its control bit (hCtrlTouch); hornerStep_correct then advances the residue (horner_mod_step), hornerStep_preserves_Y keeps Yval.

theorem Reversible.mulLoop_correct {m n : ℕ} (L : MulLoopLayout m n) (s : State m) {N Yval : ℕ} (h2N : 2 * N ≤ 2 ^ n) (hNpos : 0 < N) (hYN : Yval < N) (hB0 : regValRange L.B s n = 0) (hYv : regValRange L.Y s n = Yval) (hcleanAop : ∀ (j i : ℕ), j < n → i < n → s ((L.bank j).dbl.Aop i) = false) (hcleanCadd : ∀ (j i : ℕ), j < n → s ((L.bank j).dbl.addLayout.Cadd i) = false) (hcleandC1 : ∀ (j i : ℕ), j < n → s ((L.bank j).dbl.addLayout.C1 i) = false) (hcleandC2 : ∀ (j i : ℕ), j < n → s ((L.bank j).dbl.addLayout.C2 i) = false) (hcleandanc : ∀ j < n, s (L.bank j).dbl.addLayout.anc = false) (hcleanCcadd : ∀ (j i : ℕ), j < n → s ((L.bank j).add.Ccadd i) = false) (hcleanancC : ∀ j < n, s (L.bank j).add.ancC = false) (hcleanC1 : ∀ (j i : ℕ), j < n → s ((L.bank j).add.C1 i) = false) (hcleanC2 : ∀ (j i : ℕ), j < n → s ((L.bank j).add.C2 i) = false) (hcleananc : ∀ j < n, s (L.bank j).add.anc = false) (hA1dbl : ∀ j < n, regValRange (L.bank j).dbl.addLayout.A1 s n = 2 ^ n - N) (hA2dbl : ∀ j < n, regValRange (L.bank j).dbl.addLayout.A2 s n = N) (hA1add : ∀ j < n, regValRange (L.bank j).add.A1 s n = 2 ^ n - N) (hA2add : ∀ j < n, regValRange (L.bank j).add.A2 s n = N) : regValRange L.B (denote (mulLoop L) s) n = regValRange L.X s n * Yval % N

The verified general-n modular field multiply (the S6.3d-2b headline). Under the accumulator initialised 0, the multiplicand Y holding Yval < N, 2N ≤ 2ⁿ, 0 < N, and every bank's clean / preset wires set (carries / ancilla false, presets A1 = 2ⁿ − N, A2 = N), the loop leaves the accumulator holding (X · Yval) mod N, with the multiplier X arbitrary: regValRange B (denote (mulLoop L) s) n = (regValRange X s n · Yval) % N.

Proof: mulLoop_invariant at k = n gives (hornerVal bits n n · Yval) % N; hornerVal_full / regValRange_eq_hornerVal_bits bridges hornerVal bits n n = regValRange X s n (top n bits of an n-bit number is itself).

Derived cost

theorem Reversible.mulLoop_toffoli {m n : ℕ} (L : MulLoopLayout m n) : (circuitCost (mulLoop L)).toffoli = 30 * n ^ 2

Derived Toffoli cost of the general-n modular multiply: 30 · n² Toffolis. The loop is n Horner steps (hornerStep_toffoli, 30n each), composed through the fold; multiplier_toffoli turns the concatenation cost into the sum of the per-step counts, which is n · 30n = 30n².

Honest reading: this is the Θ(n²)-Toffoli, Θ(n²)-qubit fresh-ancilla figure — each of the n steps uses its own fresh scratch / carries / ancilla. The optimised in-place (Θ(n)-qubit) version needs the carry-clean / ancilla-restoring adder the corpus does not yet provide.

Concrete witness: a 3-bank (n = 3) modular multiply on Fin 135

A genuine MulLoopLayout 135 3, exhibiting MulLoopLayout is inhabited and mulLoop_correct applies. Shared accumulator B → {0,1,2}, multiplicand Y → {3,4,5}, 3-bit multiplier X → {6,7,8} (bit j on wire 6+j, so bank j reads X (2-j) = wire 6+(2-j) = the high-to-low MSB-first order). Each bank j owns the disjoint fresh block [9 + 42·j, 9 + 42·(j+1)) of Fin 135. All disjointness / injectivity is linear-arithmetic on the wire indices (omega), so the schema is manifestly inhabitable; the same stride formula inhabits every n (only the ambient Fin m grows).

def Reversible.wDbl (base : ℕ) (hlo : 9 ≤ base) (hb : base + 22 ≤ 135) : ModDoubleLayout 135 3

Bank j's doubling sub-layout on Fin 135: private block [base, base+22) with base = 9+42·j. All wire families are ⟨base + offset + min i width, _⟩, so every geometry field is omega.

Equations

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

Interface lemmas (CONVENTIONS §9.1, F1): the doubling sub-layout's wire assignments at the value level, one lemma per bundled field.

theorem Reversible.wDbl_Aop_val {base : ℕ} (hlo : 9 ≤ base) (hb : base + 22 ≤ 135) (i : ℕ) : ↑((wDbl base hlo hb).addLayout.Aop i) = base + 0 + min i 2

wDbl's operand wires, value level.

theorem Reversible.wDbl_B_val {base : ℕ} (hlo : 9 ≤ base) (hb : base + 22 ≤ 135) (i : ℕ) : ↑((wDbl base hlo hb).addLayout.B i) = min i 2

wDbl's accumulator wires, value level.

theorem Reversible.wDbl_Cadd_val {base : ℕ} (hlo : 9 ≤ base) (hb : base + 22 ≤ 135) (i : ℕ) : ↑((wDbl base hlo hb).addLayout.Cadd i) = base + 3 + min i 3

wDbl's add-step carry wires, value level.

theorem Reversible.wDbl_A1_val {base : ℕ} (hlo : 9 ≤ base) (hb : base + 22 ≤ 135) (i : ℕ) : ↑((wDbl base hlo hb).addLayout.A1 i) = base + 7 + min i 2

wDbl's step-1 constant-register wires, value level.

theorem Reversible.wDbl_C1_val {base : ℕ} (hlo : 9 ≤ base) (hb : base + 22 ≤ 135) (i : ℕ) : ↑((wDbl base hlo hb).addLayout.C1 i) = base + 10 + min i 3

wDbl's step-1 carry wires, value level.

theorem Reversible.wDbl_A2_val {base : ℕ} (hlo : 9 ≤ base) (hb : base + 22 ≤ 135) (i : ℕ) : ↑((wDbl base hlo hb).addLayout.A2 i) = base + 14 + min i 2

wDbl's step-3 constant-register wires, value level.

theorem Reversible.wDbl_C2_val {base : ℕ} (hlo : 9 ≤ base) (hb : base + 22 ≤ 135) (i : ℕ) : ↑((wDbl base hlo hb).addLayout.C2 i) = base + 17 + min i 3

wDbl's step-3 carry wires, value level.

theorem Reversible.wDbl_anc_val {base : ℕ} (hlo : 9 ≤ base) (hb : base + 22 ≤ 135) : ↑(wDbl base hlo hb).addLayout.anc = base + 21

wDbl's ancilla wire, value level.

def Reversible.wAdd (base ctrl : ℕ) (hlo : 9 ≤ base) (hb : base + 42 ≤ 135) (hc1 : 6 ≤ ctrl) (hc2 : ctrl < 9) : CModAddLayout 135 3

Bank j's controlled-add sub-layout on Fin 135: operand Y → {3,4,5}, control X (2-j) = wire 6 + (2-j), private block [base+22, base+42) with base = 9+42·j.

Equations

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

Interface lemmas (CONVENTIONS §9.1, F1): the controlled-add sub-layout's wire assignments at the value level, one lemma per field.

theorem Reversible.wAdd_Aop_val {base ctrl : ℕ} (hlo : 9 ≤ base) (hb : base + 42 ≤ 135) (hc1 : 6 ≤ ctrl) (hc2 : ctrl < 9) (i : ℕ) : ↑((wAdd base ctrl hlo hb hc1 hc2).Aop i) = 3 + min i 2

wAdd's operand wires, value level.

theorem Reversible.wAdd_B_val {base ctrl : ℕ} (hlo : 9 ≤ base) (hb : base + 42 ≤ 135) (hc1 : 6 ≤ ctrl) (hc2 : ctrl < 9) (i : ℕ) : ↑((wAdd base ctrl hlo hb hc1 hc2).B i) = min i 2

wAdd's accumulator wires, value level.

theorem Reversible.wAdd_Ccadd_val {base ctrl : ℕ} (hlo : 9 ≤ base) (hb : base + 42 ≤ 135) (hc1 : 6 ≤ ctrl) (hc2 : ctrl < 9) (i : ℕ) : ↑((wAdd base ctrl hlo hb hc1 hc2).Ccadd i) = base + 22 + min i 3

wAdd's controlled-add carry wires, value level.

theorem Reversible.wAdd_ctrl_val {base ctrl : ℕ} (hlo : 9 ≤ base) (hb : base + 42 ≤ 135) (hc1 : 6 ≤ ctrl) (hc2 : ctrl < 9) : ↑(wAdd base ctrl hlo hb hc1 hc2).ctrl = ctrl

wAdd's control wire, value level.

theorem Reversible.wAdd_ancC_val {base ctrl : ℕ} (hlo : 9 ≤ base) (hb : base + 42 ≤ 135) (hc1 : 6 ≤ ctrl) (hc2 : ctrl < 9) : ↑(wAdd base ctrl hlo hb hc1 hc2).ancC = base + 26

wAdd's clean-ancilla wire, value level.

theorem Reversible.wAdd_A1_val {base ctrl : ℕ} (hlo : 9 ≤ base) (hb : base + 42 ≤ 135) (hc1 : 6 ≤ ctrl) (hc2 : ctrl < 9) (i : ℕ) : ↑((wAdd base ctrl hlo hb hc1 hc2).A1 i) = base + 27 + min i 2

wAdd's step-1 constant-register wires, value level.

theorem Reversible.wAdd_C1_val {base ctrl : ℕ} (hlo : 9 ≤ base) (hb : base + 42 ≤ 135) (hc1 : 6 ≤ ctrl) (hc2 : ctrl < 9) (i : ℕ) : ↑((wAdd base ctrl hlo hb hc1 hc2).C1 i) = base + 30 + min i 3

wAdd's step-1 carry wires, value level.

theorem Reversible.wAdd_A2_val {base ctrl : ℕ} (hlo : 9 ≤ base) (hb : base + 42 ≤ 135) (hc1 : 6 ≤ ctrl) (hc2 : ctrl < 9) (i : ℕ) : ↑((wAdd base ctrl hlo hb hc1 hc2).A2 i) = base + 34 + min i 2

wAdd's step-3 constant-register wires, value level.

theorem Reversible.wAdd_C2_val {base ctrl : ℕ} (hlo : 9 ≤ base) (hb : base + 42 ≤ 135) (hc1 : 6 ≤ ctrl) (hc2 : ctrl < 9) (i : ℕ) : ↑((wAdd base ctrl hlo hb hc1 hc2).C2 i) = base + 37 + min i 3

wAdd's step-3 carry wires, value level.

theorem Reversible.wAdd_anc_val {base ctrl : ℕ} (hlo : 9 ≤ base) (hb : base + 42 ≤ 135) (hc1 : 6 ≤ ctrl) (hc2 : ctrl < 9) : ↑(wAdd base ctrl hlo hb hc1 hc2).anc = base + 41

wAdd's reduce-step ancilla wire, value level.

def Reversible.wBank (j : ℕ) : HornerStepLayout 135 3

Bank j (j < 3) as a HornerStepLayout 135 3: doubling block wDbl, controlled-add block wAdd (control X (2-j) = wire 6 + (2-j)), sharing B → {0,1,2}. The 70 cross-disjointness fields are all linear-arithmetic on the block offsets (omega).

Equations

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

theorem Reversible.wBank_clean_range (k : ℕ) (hk : k < 3) (w : Fin 135) (hw : Clean wBank k w) : 9 + 42 * k ≤ ↑w ∧ ↑w < 9 + 42 * k + 42

Every Clean (wBank ·) k w wire (k < 3) lies in bank k's private block [9 + 42·k, 9 + 42·k + 42). (All 14 clean / preset families are private; none is B, Y or X.)

theorem Reversible.wBank_touch_range (j : ℕ) (hj : j < 3) (w : Fin 135) (hw : Touches wBank j w) : ↑w < 6 ∨ ↑w = 6 + (2 - j) ∨ 9 + 42 * j ≤ ↑w ∧ ↑w < 9 + 42 * j + 42

Every Touches (wBank ·) j w wire (j < 3) lies in {0,…,5} ∪ {6 + (2 - j)} ∪ [9 + 42·j, 9 + 42·j + 42) — bank j's shared B/Y, its own control bit, and its private block.

def Reversible.wMulLoop : MulLoopLayout 135 3

The concrete 3-bank (n = 3) modular-multiply loop layout on Fin 135. B → {0,1,2}, Y → {3,4,5}, X → {6,7,8} (bit i on wire 6 + i), bank j on the fresh block [9 + 42·j, 9 + 42·(j+1)). The geometry fields reduce to the block-range lemmas wBank_clean_range / wBank_touch_range and omega.

Equations

• Reversible.wMulLoop = { bank := fun (j : ℕ) => Reversible.wBank j, X := fun (i : ℕ) => ⟨6 + min i 2, ⋯⟩, hBshare := ⋯, hYshare := ⋯, hctrl := ⋯, hInter := ⋯, hCtrlTouch := ⋯, hXinj := ⋯ }

theorem Reversible.wMulLoop_bank (j : ℕ) : wMulLoop.bank j = wBank j

Every bank of the loop is the standard wBank (interface lemma, §9.1).

theorem Reversible.wMulLoop_X_val (i : ℕ) : ↑(wMulLoop.X i) = 6 + min i 2

The loop's multiplier wires, value level (interface lemma, §9.1).

Concrete #eval cross-check: the verified n = 3, N = 3 modular multiply on Fin 135

wState sets the shared B → {0,1,2} to 0, the multiplicand Y → {3,4,5} and the multiplier X → {6,7,8} to the given bits, and presets every bank's reduce constants A1 = 2³ − 3 = 5 and A2 = 3 (the 24 preset wires); every scratch / carry / ancilla is false. (N = 3 is forced by the modular reducer's 2N ≤ 2ⁿ, i.e. N ≤ 4 at n = 3; the multiplicand satisfies Y < N = 3.) Reading register B (low 3 bits) off the strict Array Bool evaluator (runArr, via the proven bridge regValRangeArr_eq) gives the value mulLoop_correct constrains, computed instantly. The three witnesses below realise X · Y mod 3 for Y = 2: X = 3 ↦ 6 mod 3 = 0; X = 4 ↦ 8 mod 3 = 2; X = 5 ↦ 10 mod 3 = 1.

def Reversible.wState (y0 y1 y2 x0 x1 x2 : Bool) : State 135

Concrete input state on Fin 135: B = 0, Y = (y0,y1,y2) (wires {3,4,5}), X = (x0,x1,x2) (wires {6,7,8}), every bank's presets A1 = 5 (bits 0,2), A2 = 3 (bits 0,1), all scratch / carries / ancilla false.

Equations

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

theorem Reversible.min3_cases (i : ℕ) : min i 3 = 0 ∨ min i 3 = 1 ∨ min i 3 = 2 ∨ min i 3 = 3

min i 3 (and min i 2) ranges over {0,1,2,3}; this turns an ∀ i clean-wire goal whose wire depends on i only through min i 3 into the four concrete decide-able cases.