[Submitted on 21 Aug 2026 (this version), latest revision 30 Aug 2026 (v7)]
Title:A Formal, Statistical, and Source Audit of Schrottenloher's Optimized Point-Addition Circuits for Elliptic-Curve Discrete Logarithms
Abstract: Schrottenloher proposes quantum point-addition circuits whose resource savings depend on a compressed binary-Euclidean trace, reversed Bézout reconstruction, and approximate modular arithmetic. The audit covers arXiv:2606.02235v1 through Section 2, Algorithms 1–11, Figure 1, and Tables 1–3 using Lean 4 proofs, exact arithmetic, statistical records, and executions of pinned publication source. The audit verifies component theorems for the compressed trace, reconstruction, conditional multiplication, and modular arithmetic, gives checked counterexamples to 402-round totality and shrinking-field value preservation, identifies resource discrepancies, and leaves Schrottenloher's Table 1 aggregate failure probability and whole-circuit ECDLP resources unresolved. The schedule analysis finds a secp256k1 residue whose trace exceeds the 402-round schedule and terminates at round 405. It proves the tight 511-round universal bound when every remainder retains the full 256-bit width, verifies a deterministic 512-round multiplier schedule, and gives a round-369 input whose next remainder changes after the companion implementation truncates it to the scheduled width. Under a product law that samples a nonzero residue and an independent reconstruction coefficient uniformly modulo the field prime, the probability of a terminal input with an approximate-reconstruction failure at one of the 402 reverse indices is below 2−29 . For the 402-round multiplier with full-width remainders, the out-of-domain probability is below its termination tail plus 2−29 . No theorem transfers that product law to the paper's point-addition call states or combines this bound with the truncation and comparison failures. The grouped counts derived from the pinned publication source reproduce all four displayed baseline non-Clifford exponents in Schrottenloher's Table 1. Captured peak widths are one qubit below two printed widths. Static arithmetic over the pinned source configured with all 65,536 lookup rows yields a 201,410-unit surcharge, exceeding the paper's 196,608 by 4,802. Exact source arithmetic corrects two displayed base-two exponents in Schrottenloher's Table 2 by 0.01. Mapping the recorded source classes to Schrottenloher's Table 3 columns makes generic modular squaring round to 11 percent. The table prints 10 percent.
| Comments: | 25 pages |
| Subjects: | Computational Complexity (cs.CC); Logic in Computer Science (cs.LO) |
| Cite as: | marXiv:2608.00044 [cs.CC] (or marXiv:2608.00044v1 [cs.CC] for this version) |
Submission history
[v1] Fri, 21 Aug 2026 18:15:58 UTC (348 KB)
[v2] Fri, 21 Aug 2026 20:24:15 UTC (608 KB)
[v3] Fri, 21 Aug 2026 20:36:11 UTC (608 KB)
[v4] Fri, 21 Aug 2026 22:03:34 UTC (657 KB)
[v5] Sun, 30 Aug 2026 13:59:23 UTC (657 KB)
[v6] Sun, 30 Aug 2026 14:07:28 UTC (658 KB)
[v7] Sun, 30 Aug 2026 14:30:36 UTC (658 KB)