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

Table~\ref{tab:contrib} pairs each contribution with its classification and the limitation that bounds it.

\begin{table}[htbp]
  \centering\footnotesize
  \begin{threeparttable}
    \caption{Research contributions and their limitations.}
    \label{tab:contrib}
    \begin{tabular}{@{}p{4.6cm}p{3.0cm}p{6.6cm}@{}}
      \toprule
      Contribution & Classification & Limitation \\
      \midrule
      Two-implementation verification of all \secp{} invariants (Table~\ref{tab:secp-params}) & known, reproduced & exact for the standard; says nothing about implementations \\
      $\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 \\
      No group law on automorphism orbits (Prop.~\ref{prop:noquotient}) & rejected conjecture & elementary; closes one idea only \\
      ECDLP baselines on $6\,240$ instances with constants and CIs & known, reproduced & $\le 56$ bits; random-mapping model extrapolates, data do not \\
      $\sqrt6$ in iterations, $\approx 1\times$ in time for order-6 classes & known + implementation observation & specific to our canonicalisation; record implementations do better \\
      Iteration-function sweep: nothing below the random-mapping floor & rejected shortcut & bounded design space of generic walks \\
      Parallel, time--memory and preprocessing curves & known, reproduced & one machine family; constants depend on parameters \\
      Signature benchmarks and batch-verification saturation mechanism & known, reproduced & two Apple-silicon hosts, two libraries \\
      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 \\
      Lean~4 library of SHA-256 and signature facts; refutation of $\sigma$-singularity & machine-checked & bit-level and abstract-group facts only \\
      Six-stage pipeline executed autonomously with a conservative classifier & methodological & single run, single agent, qualitative assessment \\
      \bottomrule
    \end{tabular}
  \end{threeparttable}
\end{table}


\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}