\section{Literature Review and Research Gaps}
\label{sec:lit}

Stage~1 of the pipeline produced a structured database of 82 items (21 theorems, 17 algorithms, 6 security
assumptions, 10 complexity bounds, 10 experimental records, 8 open problems, 10 negative results;
\code{literature/db.yaml}) and a bibliography of 129 entries each verified against Crossref, IACR ePrint, a DOI
record or the official standard. We summarise what is settled, what is open, and which of the mandate's questions
the literature already answers.

\subsection{The elliptic-curve discrete logarithm}

The square-root barrier is a theorem in the generic-group model \citep{shoup1997lower,nechaev1994complexity}, matched by
baby-step giant-step \citep{shanks1971class} and Pollard's rho \citep{pollard1978monte} with the random-mapping constant
$\sqrt{\pi n/2}$ \citep{harris1960probability,flajolet1990random}, attained in practice by $r$-adding walks with
$r\ge 20$ \citep{teske1998speeding,teske2001random} and parallelised with linear speed-up by distinguished points
\citep{vanoorschot1999parallel}. With $S$ bits of curve-specific precomputation the online cost obeys
$ST^2=\tilde\Omega(n)$ \citep{corrigangibbs2018discrete}, which the rho-based preprocessing of \citet{bernstein2013nonuniform}
and \citet{lee2011generic} matches. Automorphisms give constant factors: $\sqrt2$ for negation and $\sqrt6$ for the
$j=0$ family \citep{wiener1999faster,duursma1999speeding,gallant2000improving}, provided fruitless cycles are handled
\citep{bos2010negation,bernstein2011correct}; \citet{bernstein2012two} and \citet{galbraith2010interval} sharpen the
BSGS and kangaroo constants, and \citet{cheon2012speeding} show (for $\F_p^*$) that the representation of group
elements can make each rho step cheaper without changing the step count. Algebraic attacks need structure that
\secp{} lacks: small embedding degree \citep{menezes1993reducing,frey1994remark}, anomalous order
\citep{semaev1998evaluation,smart1999discrete,satoh1998fermat}, composite order \citep{pohlig1978improved}, or an
extension field for summation-polynomial index calculus \citep{semaev2004summation,gaudry2009index,diem2011discrete,petit2012elliptic};
\citet{galbraith2016recent} survey the state of the art and record that no sub-exponential algorithm is known for
prime fields, and \citet{bernstein2014safecurves} tabulate the exclusion criteria for standard curves.

Table~\ref{tab:ecdlp-records} lists the completed ECDLP computations we could verify. The largest prime-field
instance remains the 112-bit computation of \citet{bos2012solving} (July 2009); the binary-field records are 113-bit
curves \citep{wenger2014solving,wenger2016harder,bernstein2016faster}; the 131-bit Certicom challenges are open
\citep{certicom2009challenge}. The gap to \secp{} is a factor of about $2^{72}$ in expected group operations.

\begin{table}[htbp]
  \centering\footnotesize
      \caption{Completed elliptic-curve discrete-logarithm computations (verified records only).}
    \label{tab:ecdlp-records}
  \resizebox{\textwidth}{!}{%
    \begin{tabular}{@{}llllll@{}}
      \toprule
      Instance & Bits & Field & Hardware & Completed & Source \\
      \midrule
      ECCp-79/-89/-97 & 79/89/97 & prime & distributed PCs & 1997--1998 & \citet{certicom2009challenge} \\
      ECC2K-108 & 108 & binary, Koblitz & distributed ($1.3\cdot10^6$ machine-days) & Apr.\ 2000 & \citet{certicom2009challenge} \\
      ECCp-109 & 109 & prime & distributed ($9.0\cdot10^6$ machine-days) & Oct.\ 2002 & \citet{certicom2009challenge} \\
      ECC2-109 & 109 & binary & distributed ($2.1\cdot10^7$ machine-days) & Apr.\ 2004 & \citet{certicom2009challenge} \\
      secp112r1 & 112 & prime & $\approx 215$ PlayStation~3 & Jul.\ 2009 & \citet{bos2012solving} \\
      113-bit Koblitz & 113 & binary, Koblitz & 18 Virtex-6 FPGAs & 2014 & \citet{wenger2014solving} \\
      sect113r1 & 113 & binary & 10 Kintex-7 FPGAs & 2015 & \citet{wenger2016harder} \\
      sect113r2 & 113 & binary & Spartan-6 FPGAs & 2016 & \citet{bernstein2016faster} \\
      ECCp-131, ECC2-131, ECC2K-130 & 130--131 & prime/binary & --- & open & \citet{certicom2009challenge,bailey2009breaking} \\
      \bottomrule
    \end{tabular}
  }
  \par\smallskip{\footnotesize Figures as stated in the sources (\code{literature/records.md}). \secp{} has $n\approx 2^{256}$: rho with the negation map needs $\approx\sqrt{\pi n/4}\approx 2^{127.8}$ operations, about $2^{72}$ times the 112-bit computation.}

\end{table}

\subsection{Signatures}

Schnorr signatures are EUF-CMA under the discrete-logarithm assumption in the random-oracle model by the forking
lemma \citep{pointcheval2000security}; the loss in the number of hash queries is unavoidable for algebraic reductions
and the random oracle cannot be removed \citep{paillier2005discrete,seurin2012exact}. ECDSA requires an idealisation of
the conversion function $R\mapsto x(R)\bmod n$ \citep{brown2005generic,vaudenay2003security,fersch2016provable,fersch2017one},
extended to additive key derivation and presignatures by \citet{groth2022security}. Nonce leakage is fatal
\citep{howgravegraham2001lattice,breitner2019biased,aldaya2020ladderleak,jancar2020minerva}, hence deterministic nonces
\citep{pornin2013rfc6979,wuille2020bip340}. Batch verification of Schnorr-type signatures is classical
\citep{naccache1994can,bellare1998fast,bernstein2012high} and rests on multi-scalar multiplication
\citep{straus1964addition,pippenger1980evaluation,moller2001algorithms}; multi-signatures build on the same linearity
\citep{bellare2006multi,maxwell2019simple,nick2021musig2}. The reference implementation is \libsecp{} \citep{wuille2013libsecp256k1}.

\subsection{SHA-256}

Beyond the Merkle--Damg\aa rd reduction \citep{merkle1989one,damgard1989design} and the structural analysis of
\citet{gilbert2003security}, knowledge about SHA-256 is knowledge about reduced step counts
(Table~\ref{tab:sha-lit}). Collision attacks progressed from 21--24 steps in 2008
\citep{nikolic2008collisions,indesteege2008collisions,sanadhya2008new} to 27--28 practical steps
\citep{mendel2011finding,mendel2013improving}, 31 practical steps \citep{li2024first} and a theoretical 37-step
attack \citep{zhang2026collision}; semi-free-start collisions reach 38--39 steps \citep{mendel2013improving,li2024new};
preimages reach 43 steps \citep{aoki2009preimages} and 45 steps (52 for the compression function) at complexities
within a small factor of brute force \citep{khovratovich2012bicliques}. SAT-based analysis started with
\citet{mironov2006applications}; pure SAT search stalls around 28 steps while SAT combined with computer algebra
reproduces the 38-step semi-free-start result \citep{nejati2017adaptive,alamgir2024sha256}. The full SHA-1 collisions
\citep{stevens2017first,leurent2020sha1} are the benchmark for what a mature differential attack on a 80-step design
costs ($2^{63}$).

\begin{table}[htbp]
  \centering\footnotesize
      \caption{Reduced-step cryptanalysis of SHA-256 (64 steps): published records.}
    \label{tab:sha-lit}
  \resizebox{\textwidth}{!}{%
    \begin{tabular}{@{}lllll@{}}
      \toprule
      Type & Steps & Complexity & Practical? & Source \\
      \midrule
      Collision & 21 & $\approx 2^{19}$ & yes & \citet{nikolic2008collisions} \\
      Collision & 23 / 24 & $2^{18}$ / $2^{28.5}$ & yes & \citet{indesteege2008collisions} \\
      Collision & 23 / 24 & $2^{11.5}$ / $2^{28.5}$ & yes & \citet{sanadhya2008new} \\
      Collision & 27 & practical & yes & \citet{mendel2011finding} \\
      Collision & 28 (31) & practical ($\le 2^{65.5}$) & yes (no) & \citet{mendel2013improving} \\
      Collision & 31 & $\approx 1.2$ h on 64 threads & yes & \citet{li2024first} \\
      Collision & 37 & theoretical & no & \citet{zhang2026collision} \\
      Semi-free-start collision & 32 / 38 / 39 & practical & yes & \citet{mendel2011finding,mendel2013improving,li2024new} \\
      Semi-free-start (SAT+CAS) & 38 & solver reproduction & yes & \citet{alamgir2024sha256} \\
      Collision (pure SAT) & $\le 28$ & --- & yes & \citet{alamgir2024sha256} \\
      Preimage & 43 & $2^{254.9}$ & no & \citet{aoki2009preimages} \\
      Preimage (hash / compression) & 45 / 52 & $\approx 2^{256}$ (bicliques) & no & \citet{khovratovich2012bicliques} \\
      \bottomrule
    \end{tabular}
  }
  \par\smallskip{\footnotesize Figures as stated in the abstracts (\code{literature/records.md}). No attack on the full 64-step function is known; the generic bounds $2^{128}$ (collision) and $2^{256}$ (preimage) stand.}

\end{table}

\subsection{Automated discovery}

Program-search systems have produced verified mathematical constructions---matrix-multiplication tensors
\citep{fawzi2022discovering}, combinatorial bounds \citep{romeraparedes2024mathematical,novikov2025alphaevolve},
olympiad geometry proofs \citep{trinh2024solving}, conjectures in knot theory and representation theory
\citep{davies2021advancing}---and end-to-end ``AI scientist'' pipelines have been proposed \citep{lu2024ai}. None
targets standardised cryptographic primitives, where the ground truth is dominated by impossibility results, so
Axis~D has no published baseline and defines its own (rediscovery rate, false-positive rate, and the quality of the
negative results). On the formal side, \citet{boving2025interactive} make bit-vector facts about hash-function steps
machine-checkable in Lean~4 \citep{demoura2021lean}; we use this to separate checked identities from informal ones.

\subsection{Research gaps and what the mandate already settles}

Of the mandate's questions, the literature settles the following (\code{literature/research\_gaps.md}): A1 (no
improvement beyond constant factors from the endomorphism), A2 (orbits give exactly $\sqrt{\lvert\Aut\rvert}$), A5
(generic algorithms cannot beat $\sqrt n$, with or without preprocessing), B1 (the proof structures differ by the
conversion-function idealisation), B2 (batch verification is known for Schnorr, not for ECDSA), and C1/C2/C4 up to
the recorded step counts. What is not settled, and what we test, is quantitative and methodological: the measured
constants and their interaction with distinguished-point overheads and fruitless cycles at 20--48 bits (gap~2); the
preprocessing constant on a fixed curve (gap~3); whether an automated search over iteration-function designs or over
algebraic identities finds anything the theory does not predict (gaps~1, 8); how far generic SAT encodings get on
step-reduced SHA-256 compared with the dedicated tools (gap~6); and whether the elementary identities that
implementations rely on can be made machine-checked at negligible cost (gap~7). The closed form of the GLV
constants (Proposition~\ref{prop:glv}) is the one place where the symbolic search produced something we did not find
written down, and we are careful to call it an exposition of a known structure rather than a discovery.