Measurement-based AND-adder re-cost (Build #21, L5-d)

Category: 3-Local (QM-validity content; no CSD ontology).

This file delivers the adder-level Toffoli re-count of the AND-based ripple adder (Mathlib/QuantumInfo/Reversible/AndAdd.lean, #30) obtained by replacing each of its reverse-pass AND-uncompute CCX Toffolis with the measurement gadget (gadgetGateList, Empirical/QM/MeasurementUncompute.lean, 0 Toffoli), whose per-block equivalence to the unitary AND-uncompute is the proven content of #31 (Empirical/QM/MeasurementUncomputeLift.lean, andUncompute_measureUncompute_same_data / andUncompute_measurement_saving).

The CSD anti-hollow-cost ethos is binding: the saving is not a count over an unverified swap. It aggregates numUncomputeBlocks L (= 3n) per-block #31 replacements, each a 1 → 0 Toffoli swap on a block proven to have the same data effect (andUncompute_measurement_saving). The Part-1 closed form is derived from those per-block lemmas (measUncomputeGadgets_toffoli routes through gadgetBlockToffoli_eq_zero, which is literally #31's second conjunct), not asserted independently.

The exact pre-replacement count (decision-relevant finding)

The #30 adder is andForward L ++ andSumPass L ++ inverse (andForward L). Its reverse pass inverse (andForward L) carries 3n AND-uncompute CCX Toffolis, NOT n: each of the n carry bits uses a 3-Toffoli preserving-majority cell (andCarryCell), so the reverse pass has 3 AND-uncompute blocks per carry bit (andAdd_uncompute_toffoli : … = 3 * n). Each block is a single Reversible.andUncompute-shaped CCX, so #31's per-block lemma applies to every one.

Part 1 — the Toffoli count (the deliverable)

• before (#30): andAdd_toffoli_eq : (circuitCost (andAdd L)).toffoli = 6 * n (3n compute + 3n uncompute; sum pass CNOT-only).
• after (this file): measAddToffoli_eq : measAddToffoli L = 3 * n (forward kept; the 3n AND-uncompute Toffolis become 3n gadgets, each 0 Toffoli).
• saving: measAdd_toffoli_savings_eq : (circuitCost (andAdd L)).toffoli - measAddToffoli L = 3 * n and the first-class before/after form measAdd_toffoli_saving : before = after + numUncomputeBlocks L.
• at n = 256 (measAdd_toffoli_256): before 1536, after 768, saving 768 (a 2× reduction).

Part 2 — the correctness anchor (so the count is not hollow)

• MUST-HAVE: measAdd_saving_aggregates — the saving is numUncomputeBlocks L (= 3n) times the per-block #31 saving (circuitCost (andUncompute a b g)).toffoli - gadgetBlockToffoli = 1 (perBlock_saving, from andUncompute_measurement_saving). The count provably aggregates 3n proven-equivalent block replacements.

• STRETCH (single carry, unitary side done; gadget n-fold amplitude WALLED): Reversible.ccxAtMat_lifts_denote lifts a single AND-uncompute CCX block into the full register QReg m as the permutation matrix ccxAtMat, generalizing #31's fixed-wire (0,1,2) lift to arbitrary wires of any width. This shows the per-block unitary embedding into the full register is not the obstruction. (Extracted 2026-08-21: the lift cluster is generic mathematics and now lives Category-1 in Mathlib/QuantumInfo/Reversible/Lift.lean, beside the DSL it bridges; this file keeps the cost accounting and the wall documentation.)

  The wall (precise, decision-relevant). The genuine gadget hybrid — replacing one AND-uncompute by the measurement gadget and proving the full-register data output on S unchanged — walls at the tensor factor. The gadget is not a permutation: measureUncompute_uncomputes sends the AND-shaped block state Σ c_{xy}|x,y,x∧y⟩ to (√2)⁻¹ • Σ c_{xy}|x,y,m⟩ (a (√2)⁻¹ scalar plus an ancilla reset to the outcome m). So the clean "basis-state ↦ basis-state" induction that lifts unitary permutation circuits (and underlies ccxAtMat_lifts_denote) breaks at the replaced block: the post-gadget full-register state is no longer a basis-state permutation of the input. Applying the gadget as a local tensor factor measureUncompute ⊗ I to a general entangled full-register superposition requires the factorization QReg m ≅ QReg 3 ⊗ QReg (m−3). ⚠️ Wall note updated 2026-08-22 (MG-5): that factorization is no longer missing — it is QuantumInfo.regTensorEquiv (Mathlib/QuantumInfo/RegisterTensor.lean), together with tensorFirst, the "operator on a wire block, identity elsewhere" construction and its basis-state computation rule. So the obstruction is not the absence of API. What remains undone is the argument itself: threading the non-permutation gadget through the adder's 3n blocks and proving the full-register data output on S unchanged. The single-block unitary embedding is sound; the n-fold hybrid amplitude equality is open work (⚠️ RESIDUE(R-013)), not a missing library.

Honest scope (Part 3)

This is an adder-level re-cost on proven-equivalent blocks. No ECDSA score change is claimed. The ECDSA score requires (i) swapping the corpus point-addition's adders (Cuccaro, in-place) for AND-based adders throughout the curve arithmetic, AND (ii) the harness step #7 — neither is done here. The Part-1 count is exact and the Part-2 anchor proves it aggregates 3n #31-equivalent blocks (so the count is not hollow); the full n-fold amplitude state-equality of the hybrid adder is WALLED at the QReg 3 ⊗ QReg (m−3) tensor factor, as stated above and reported.

Part 1 — the measurement-based re-cost

def CSD.Empirical.QM.gadgetBlockToffoli : ℕ

The per-block measurement-gadget Toffoli cost (= 0). The Toffoli total of one gadgetGateList (Hadamard + measurement + conditional CZ). It is #31's second conjunct (andUncompute_measurement_saving), the proven-equivalent Toffoli-free replacement.

Equations

• CSD.Empirical.QM.gadgetBlockToffoli = (List.map (fun (g : CSD.Empirical.QM.GadgetGate) => (CSD.Empirical.QM.gadgetGateCost g).toffoli) CSD.Empirical.QM.gadgetGateList).sum

theorem CSD.Empirical.QM.gadgetBlockToffoli_eq_zero : gadgetBlockToffoli = 0

gadgetBlockToffoli = 0, extracted from #31's andUncompute_measurement_saving (the gadget Toffoli count is wire-independent; any width witness gives it).

def CSD.Empirical.QM.numUncomputeBlocks {m n : ℕ} (L : Reversible.AndAddLayout m n) : ℕ

The number of AND-uncompute blocks in the #30 reverse pass. It is the Toffoli count of inverse (andForward L), namely 3n (3 per carry bit, n bits); each block is a single Reversible.andUncompute-shaped CCX replaced by the measurement gadget.

Equations

• CSD.Empirical.QM.numUncomputeBlocks L = (Reversible.circuitCost (Reversible.inverse (Reversible.andForward L))).toffoli

theorem CSD.Empirical.QM.numUncomputeBlocks_eq {m n : ℕ} (L : Reversible.AndAddLayout m n) : numUncomputeBlocks L = 3 * n

numUncomputeBlocks L = 3 * n (#30 andAdd_uncompute_toffoli).

theorem CSD.Empirical.QM.replicate_flatten_map_sum (k : ℕ) (l : List GadgetGate) (f : GadgetGate → ℕ) : (List.map f (List.replicate k l).flatten).sum = k * (List.map f l).sum

Aggregating k gadget blocks. The Toffoli total of k concatenated copies of any gate list l is k times the per-copy total — the elementary accounting behind "replace each block by a proven-equivalent gadget and sum".

theorem CSD.Empirical.QM.measUncomputeGadgets_toffoli {m n : ℕ} (L : Reversible.AndAddLayout m n) : (List.map (fun (g : GadgetGate) => (gadgetGateCost g).toffoli) (List.replicate (numUncomputeBlocks L) gadgetGateList).flatten).sum = 0

The measurement-based uncompute pass is Toffoli-free. Replacing every one of the numUncomputeBlocks L reverse-pass AND-uncompute CCX Toffolis by the gadget (gadgetGateList) gives numUncomputeBlocks L copies of a 0-Toffoli block, total 0. Derived: the k-fold aggregation (replicate_flatten_map_sum) times the per-block 0 (gadgetBlockToffoli_eq_zero, i.e. #31's saving).

def CSD.Empirical.QM.measAddToffoli {m n : ℕ} (L : Reversible.AndAddLayout m n) : ℕ

The measurement-based adder's Toffoli count. The forward AND-compute pass keeps its Toffolis, the sum pass is CNOT-only, and each of the numUncomputeBlocks L reverse-pass AND-uncompute Toffolis becomes a measurement gadget (gadgetGateList, 0 Toffoli). The third summand is the Toffoli total of those numUncomputeBlocks L gadget blocks — so the count is, by construction, the aggregate of the per-block replacements.

Equations

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

theorem CSD.Empirical.QM.measAddToffoli_eq {m n : ℕ} (L : Reversible.AndAddLayout m n) : measAddToffoli L = 3 * n

Part-1 closed form (after): measAddToffoli L = 3 * n. Forward 3n (andForwardPrefix_toffoli) + sum 0 (andSumPrefix_toffoli) + uncompute 0 (measUncomputeGadgets_toffoli). The uncompute Toffolis vanish; the forward half survives.

theorem CSD.Empirical.QM.andAdd_toffoli_eq {m n : ℕ} (L : Reversible.AndAddLayout m n) : (Reversible.circuitCost (Reversible.andAdd L)).toffoli = 6 * n

Part-1 closed form (before): (circuitCost (andAdd L)).toffoli = 6 * n (re-export of #30 andAdd_toffoli: 3n compute + 3n uncompute).

theorem CSD.Empirical.QM.measAdd_toffoli_saving {m n : ℕ} (L : Reversible.AndAddLayout m n) : (Reversible.circuitCost (Reversible.andAdd L)).toffoli = measAddToffoli L + numUncomputeBlocks L

The saving, before/after first-class form. The #30 total equals the measurement-based total plus the saved Toffolis, which are exactly the numUncomputeBlocks L (= 3n) uncompute Toffolis the gadget eliminates: before = after + numUncomputeBlocks L.

theorem CSD.Empirical.QM.measAdd_toffoli_savings_eq {m n : ℕ} (L : Reversible.AndAddLayout m n) : (Reversible.circuitCost (Reversible.andAdd L)).toffoli - measAddToffoli L = 3 * n

The saving as a closed form: before − after = 3 * n.

theorem CSD.Empirical.QM.measAdd_toffoli_256 {m : ℕ} (L : Reversible.AndAddLayout m 256) : (Reversible.circuitCost (Reversible.andAdd L)).toffoli = 1536 ∧ measAddToffoli L = 768 ∧ (Reversible.circuitCost (Reversible.andAdd L)).toffoli - measAddToffoli L = 768

Explicit numbers at n = 256. Before 1536 (6·256), after 768 (3·256), saving 768 (a 2× Toffoli reduction).

Part 2 — the correctness anchor

theorem CSD.Empirical.QM.perBlock_saving {k : ℕ} (a b g : Fin k) : (Reversible.circuitCost (Reversible.andUncompute a b g)).toffoli - gadgetBlockToffoli = 1

The per-block #31 saving. Each reverse-pass AND-uncompute is one CCX (1 Toffoli, andCell_uncompute_toffoli); its measurement-gadget replacement is 0 Toffoli (gadgetBlockToffoli). So the per-block saving is 1 − 0 = 1 Toffoli on a block proven to have the same data effect (andUncompute_measureUncompute_same_data). This is #31's andUncompute_measurement_saving, in subtraction form.

theorem CSD.Empirical.QM.measAdd_saving_aggregates {m n : ℕ} (L : Reversible.AndAddLayout m n) (a b g : Fin m) : (Reversible.circuitCost (Reversible.andAdd L)).toffoli - measAddToffoli L = numUncomputeBlocks L * ((Reversible.circuitCost (Reversible.andUncompute a b g)).toffoli - gadgetBlockToffoli)

Compositional anchor (the count is not hollow). The total Toffoli saving equals the number of reverse-pass AND-uncompute blocks (numUncomputeBlocks L = 3n) times the per-block #31 saving (perBlock_saving, 1 Toffoli on a proven-equivalent block). So the re-cost is the sum over the 3n carries' AND-uncompute blocks of the #31 per-block replacement, not a count over an unverified swap.

Part 2 (stretch) — the single-block unitary lift into the full register QReg m

(Extracted 2026-08-21.) The stretch deliverable — Reversible.ccxAtMat_lifts_denote, the arbitrary-wire, any-width generalization of #31's fixed-wire lift, with its cluster (ccxAt / ccxAtMat / stateOfReg / regOfState / toEuclideanLin_basisState_m) — is generic mathematics and lives Category-1 in Mathlib/QuantumInfo/Reversible/Lift.lean, beside the DSL it bridges (available here through the import chain). It shows the per-block unitary embedding into the full register is not the obstruction; the wall is the non-permutation measurement gadget tensor-factor, documented in the module header, which is application content and stays here.

Non-vacuity witness