1\section{Limitations}2\label{sec:limitations}34Table~\ref{tab:contrib} pairs each contribution with its classification and the limitation that bounds it.56\begin{table}[htbp]7 \centering\footnotesize8 \begin{threeparttable}9 \caption{Research contributions and their limitations.}10 \label{tab:contrib}11 \begin{tabular}{@{}p{4.6cm}p{3.0cm}p{6.6cm}@{}}12 \toprule13 Contribution & Classification & Limitation \\14 \midrule15 Two-implementation verification of all \secp{} invariants (Table~\ref{tab:secp-params}) & known, reproduced & exact for the standard; says nothing about implementations \\16 $\End(E)=\Z[\omega]$; GLV lattice $=(\bar\pi-1)$; closed form of the \libsecp{} constants & known structure, explicit form & a consequence of classical CM theory; exposition, not discovery \\17 No group law on automorphism orbits (Prop.~\ref{prop:noquotient}) & rejected conjecture & elementary; closes one idea only \\18 ECDLP baselines on $6\,240$ instances with constants and CIs & known, reproduced & $\le 56$ bits; random-mapping model extrapolates, data do not \\19 $\sqrt6$ in iterations, $\approx 1\times$ in time for order-6 classes & known + implementation observation & specific to our canonicalisation; record implementations do better \\20 Iteration-function sweep: nothing below the random-mapping floor & rejected shortcut & bounded design space of generic walks \\21 Parallel, time--memory and preprocessing curves & known, reproduced & one machine family; constants depend on parameters \\22 Signature benchmarks and batch-verification saturation mechanism & known, reproduced & two Apple-silicon hosts, two libraries \\23 SHA-256 diffusion, bias, SAT/SMT calibration, UNSAT for $\le 8$ steps, local collision & known / empirical & generic encodings; no characteristic guidance; nothing about 64 steps \\24 Lean~4 library of SHA-256 and signature facts; refutation of $\sigma$-singularity & machine-checked & bit-level and abstract-group facts only \\25 Six-stage pipeline executed autonomously with a conservative classifier & methodological & single run, single agent, qualitative assessment \\26 \bottomrule27 \end{tabular}28 \end{threeparttable}29\end{table}303132\begin{itemize}33\item \textbf{Scale.} The ECDLP experiments run on groups of at most $2^{48}$--$2^{56}$ elements. The fitted34exponents and constants describe this range; extrapolation to $2^{256}$ rests on the random-mapping heuristic and on35Shoup's bound, not on our data. We state no result about \secp{} itself that is not an exact algebraic verification.36\item \textbf{Generic design space.} The iteration-function search (\Hname{H09}) explores a bounded parameter space of37$r$-adding and mixed walks; it cannot find a non-generic idea, and its negative result is a statement about that space.38\item \textbf{SHA-256 encodings.} Our CNF and SMT encodings are generic (Tseitin, ripple-carry adders) and unguided by39differential characteristics; the step counts they reach are therefore far below the literature's and should be read40as a calibration of generic solvers, not as a limit of SAT-based cryptanalysis \citep{alamgir2024sha256}.41\item \textbf{Formal coverage.} The Lean statements cover bit-level identities and abstract-group facts. They do not42formalise the curve arithmetic, the random-mapping analysis or any probabilistic claim; those remain informal.43\item \textbf{Timing measurements.} Wall-clock figures come from two Apple Silicon machines and depend on the44toolchains used; operation counts are the portable quantity. Batch-verification speed-ups are relative to the same45arithmetic library and would differ against a hand-optimised assembly implementation.46\item \textbf{Novelty.} The one algebraic statement we did not find written explicitly (the closed form of the47\libsecp{} GLV constants) is a direct consequence of classical CM theory; we claim exposition, not discovery, and a48reader who knows a prior statement of it should treat it as a reproduction.49\item \textbf{Single agent, single run.} The pipeline was executed once by one autonomous agent; we do not measure50variance across runs or agents, and the methodological assessment (\Hname{H24}) is qualitative. A controlled51comparison against a baseline agent without the pipeline's discipline is left to future work.52\item \textbf{Literature verification.} Bibliographic entries were verified against public records; where a venue53record omitted a field (volume numbers of some Springer series), it was filled from series knowledge and flagged in54\code{literature/unverified.md}.55\end{itemize}56