\section{Limitations}
\label{sec:limitations}

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