[Submitted on 10 Sep 2026 (v1), last revised 10 Sep 2026 (this version, v2)]
Title:Verified Arithmetic Reductions for an 833-Qubit secp256k1 ECDLP Program
Abstract: We reduce the verified Toffoli bound for an 833-logical-qubit secp256k1 discrete-logarithm program from 36,591,123,006 to 18,467,700,570 per execution, preserving one-run recovery probability greater than 99 percent. The reductions combine paired endpoint scans, direct modular-correction predicates, restructured carry propagation, shared controls for length writes, and measurement-based erasure of arithmetic and selector temporaries. Lean proofs establish the changed program's exact branch amplitudes, restored quantum workspace, pathwise and expected Toffoli bounds, and unchanged Fourier-output distribution. A lifetime proof reuses the final Fourier-output bit for arithmetic measurement results, keeping the mutable classical allocation at 768 bits. The reported minimum uses five-bit scalar windows and a 26-bit initial lookup, with a 4 GiB packed public table and at most 34,493,956,094 lookup CNOTs. We derive the component savings, state the conditions for coherent measurement erasure, and describe proof decompositions that keep measurement histories and generated circuits symbolic.
| Subjects: | Logic in Computer Science (cs.LO); Computational Complexity (cs.CC) |
| Cite as: | marXiv:2609.00004 [cs.LO] (or marXiv:2609.00004v2 [cs.LO] for this version) |
Submission history
[v1] Thu, 10 Sep 2026 15:05:36 UTC (283 KB)
[v2] Thu, 10 Sep 2026 15:11:23 UTC (284 KB)
Related work
- marXiv:2609.00003
- Extends the 36,591,123,006-Toffoli result with verified arithmetic reductions to 18,467,700,570 at the same 833-qubit allocation and one-run recovery guarantee.
Named by
- marXiv:2609.00013
- This stand-alone report incorporates the arithmetic reductions and gives the complete algorithm, recovery argument, and literature comparison.