1\section{Limitations}2\label{sec:limitations}34\begin{itemize}5\item \textbf{Scale.} The ECDLP experiments run on groups of at most $2^{48}$--$2^{56}$ elements. The fitted6exponents and constants describe this range; extrapolation to $2^{256}$ rests on the random-mapping heuristic and on7Shoup's bound, not on our data. We state no result about \secp{} itself that is not an exact algebraic verification.8\item \textbf{Generic design space.} The iteration-function search (\Hname{H09}) explores a bounded parameter space of9$r$-adding and mixed walks; it cannot find a non-generic idea, and its negative result is a statement about that space.10\item \textbf{SHA-256 encodings.} Our CNF and SMT encodings are generic (Tseitin, ripple-carry adders) and unguided by11differential characteristics; the step counts they reach are therefore far below the literature's and should be read12as a calibration of generic solvers, not as a limit of SAT-based cryptanalysis \citep{alamgir2024sha256}.13\item \textbf{Formal coverage.} The Lean statements cover bit-level identities and abstract-group facts. They do not14formalise the curve arithmetic, the random-mapping analysis or any probabilistic claim; those remain informal.15\item \textbf{Timing measurements.} Wall-clock figures come from two Apple Silicon machines and depend on the16toolchains used; operation counts are the portable quantity. Batch-verification speed-ups are relative to the same17arithmetic library and would differ against a hand-optimised assembly implementation.18\item \textbf{Novelty.} The one algebraic statement we did not find written explicitly (the closed form of the19\libsecp{} GLV constants) is a direct consequence of classical CM theory; we claim exposition, not discovery, and a20reader who knows a prior statement of it should treat it as a reproduction.21\item \textbf{Single agent, single run.} The pipeline was executed once by one autonomous agent; we do not measure22variance across runs or agents, and the methodological assessment (\Hname{H24}) is qualitative. A controlled23comparison against a baseline agent without the pipeline's discipline is left to future work.24\item \textbf{Literature verification.} Bibliographic entries were verified against public records; where a venue25record omitted a field (volume numbers of some Springer series), it was filled from series knowledge and flagged in26\code{literature/unverified.md}.27\end{itemize}28