1\section{Literature Review and Research Gaps}2\label{sec:lit}34Stage~1 of the pipeline produced a structured database of 82 items (21 theorems, 17 algorithms, 6 security5assumptions, 10 complexity bounds, 10 experimental records, 8 open problems, 10 negative results;6\code{literature/db.yaml}) and a bibliography of 129 entries each verified against Crossref, IACR ePrint, a DOI7record or the official standard. We summarise what is settled, what is open, and which of the mandate's questions8the literature already answers.910\subsection{The elliptic-curve discrete logarithm}1112The square-root barrier is a theorem in the generic-group model \citep{shoup1997lower,nechaev1994complexity}, matched by13baby-step giant-step \citep{shanks1971class} and Pollard's rho \citep{pollard1978monte} with the random-mapping constant14$\sqrt{\pi n/2}$ \citep{harris1960probability,flajolet1990random}, attained in practice by $r$-adding walks with15$r\ge 20$ \citep{teske1998speeding,teske2001random} and parallelised with linear speed-up by distinguished points16\citep{vanoorschot1999parallel}. With $S$ bits of curve-specific precomputation the online cost obeys17$ST^2=\tilde\Omega(n)$ \citep{corrigangibbs2018discrete}, which the rho-based preprocessing of \citet{bernstein2013nonuniform}18and \citet{lee2011generic} matches. Automorphisms give constant factors: $\sqrt2$ for negation and $\sqrt6$ for the19$j=0$ family \citep{wiener1999faster,duursma1999speeding,gallant2000improving}, provided fruitless cycles are handled20\citep{bos2010negation,bernstein2011correct}; \citet{bernstein2012two} and \citet{galbraith2010interval} sharpen the21BSGS and kangaroo constants, and \citet{cheon2012speeding} show (for $\F_p^*$) that the representation of group22elements can make each rho step cheaper without changing the step count. Algebraic attacks need structure that23\secp{} lacks: small embedding degree \citep{menezes1993reducing,frey1994remark}, anomalous order24\citep{semaev1998evaluation,smart1999discrete,satoh1998fermat}, composite order \citep{pohlig1978improved}, or an25extension field for summation-polynomial index calculus \citep{semaev2004summation,gaudry2009index,diem2011discrete,petit2012elliptic};26\citet{galbraith2016recent} survey the state of the art and record that no sub-exponential algorithm is known for27prime fields, and \citet{bernstein2014safecurves} tabulate the exclusion criteria for standard curves.2829Table~\ref{tab:ecdlp-records} lists the completed ECDLP computations we could verify. The largest prime-field30instance remains the 112-bit computation of \citet{bos2012solving} (July 2009); the binary-field records are 113-bit31curves \citep{wenger2014solving,wenger2016harder,bernstein2016faster}; the 131-bit Certicom challenges are open32\citep{certicom2009challenge}. The gap to \secp{} is a factor of about $2^{72}$ in expected group operations.3334\begin{table}[htbp]35 \centering\footnotesize36 \caption{Completed elliptic-curve discrete-logarithm computations (verified records only).}37 \label{tab:ecdlp-records}38 \resizebox{\textwidth}{!}{%39 \begin{tabular}{@{}llllll@{}}40 \toprule41 Instance & Bits & Field & Hardware & Completed & Source \\42 \midrule43 ECCp-79/-89/-97 & 79/89/97 & prime & distributed PCs & 1997--1998 & \citet{certicom2009challenge} \\44 ECC2K-108 & 108 & binary, Koblitz & distributed ($1.3\cdot10^6$ machine-days) & Apr.\ 2000 & \citet{certicom2009challenge} \\45 ECCp-109 & 109 & prime & distributed ($9.0\cdot10^6$ machine-days) & Oct.\ 2002 & \citet{certicom2009challenge} \\46 ECC2-109 & 109 & binary & distributed ($2.1\cdot10^7$ machine-days) & Apr.\ 2004 & \citet{certicom2009challenge} \\47 secp112r1 & 112 & prime & $\approx 215$ PlayStation~3 & Jul.\ 2009 & \citet{bos2012solving} \\48 113-bit Koblitz & 113 & binary, Koblitz & 18 Virtex-6 FPGAs & 2014 & \citet{wenger2014solving} \\49 sect113r1 & 113 & binary & 10 Kintex-7 FPGAs & 2015 & \citet{wenger2016harder} \\50 sect113r2 & 113 & binary & Spartan-6 FPGAs & 2016 & \citet{bernstein2016faster} \\51 ECCp-131, ECC2-131, ECC2K-130 & 130--131 & prime/binary & --- & open & \citet{certicom2009challenge,bailey2009breaking} \\52 \bottomrule53 \end{tabular}54 }55 \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.}5657\end{table}5859\subsection{Signatures}6061Schnorr signatures are EUF-CMA under the discrete-logarithm assumption in the random-oracle model by the forking62lemma \citep{pointcheval2000security}; the loss in the number of hash queries is unavoidable for algebraic reductions63and the random oracle cannot be removed \citep{paillier2005discrete,seurin2012exact}. ECDSA requires an idealisation of64the conversion function $R\mapsto x(R)\bmod n$ \citep{brown2005generic,vaudenay2003security,fersch2016provable,fersch2017one},65extended to additive key derivation and presignatures by \citet{groth2022security}. Nonce leakage is fatal66\citep{howgravegraham2001lattice,breitner2019biased,aldaya2020ladderleak,jancar2020minerva}, hence deterministic nonces67\citep{pornin2013rfc6979,wuille2020bip340}. Batch verification of Schnorr-type signatures is classical68\citep{naccache1994can,bellare1998fast,bernstein2012high} and rests on multi-scalar multiplication69\citep{straus1964addition,pippenger1980evaluation,moller2001algorithms}; multi-signatures build on the same linearity70\citep{bellare2006multi,maxwell2019simple,nick2021musig2}. The reference implementation is \libsecp{} \citep{wuille2013libsecp256k1}.7172\subsection{SHA-256}7374Beyond the Merkle--Damg\aa rd reduction \citep{merkle1989one,damgard1989design} and the structural analysis of75\citet{gilbert2003security}, knowledge about SHA-256 is knowledge about reduced step counts76(Table~\ref{tab:sha-lit}). Collision attacks progressed from 21--24 steps in 200877\citep{nikolic2008collisions,indesteege2008collisions,sanadhya2008new} to 27--28 practical steps78\citep{mendel2011finding,mendel2013improving}, 31 practical steps \citep{li2024first} and a theoretical 37-step79attack \citep{zhang2026collision}; semi-free-start collisions reach 38--39 steps \citep{mendel2013improving,li2024new};80preimages reach 43 steps \citep{aoki2009preimages} and 45 steps (52 for the compression function) at complexities81within a small factor of brute force \citep{khovratovich2012bicliques}. SAT-based analysis started with82\citet{mironov2006applications}; pure SAT search stalls around 28 steps while SAT combined with computer algebra83reproduces the 38-step semi-free-start result \citep{nejati2017adaptive,alamgir2024sha256}. The full SHA-1 collisions84\citep{stevens2017first,leurent2020sha1} are the benchmark for what a mature differential attack on a 80-step design85costs ($2^{63}$).8687\begin{table}[htbp]88 \centering\footnotesize89 \caption{Reduced-step cryptanalysis of SHA-256 (64 steps): published records.}90 \label{tab:sha-lit}91 \resizebox{\textwidth}{!}{%92 \begin{tabular}{@{}lllll@{}}93 \toprule94 Type & Steps & Complexity & Practical? & Source \\95 \midrule96 Collision & 21 & $\approx 2^{19}$ & yes & \citet{nikolic2008collisions} \\97 Collision & 23 / 24 & $2^{18}$ / $2^{28.5}$ & yes & \citet{indesteege2008collisions} \\98 Collision & 23 / 24 & $2^{11.5}$ / $2^{28.5}$ & yes & \citet{sanadhya2008new} \\99 Collision & 27 & practical & yes & \citet{mendel2011finding} \\100 Collision & 28 (31) & practical ($\le 2^{65.5}$) & yes (no) & \citet{mendel2013improving} \\101 Collision & 31 & $\approx 1.2$ h on 64 threads & yes & \citet{li2024first} \\102 Collision & 37 & theoretical & no & \citet{zhang2026collision} \\103 Semi-free-start collision & 32 / 38 / 39 & practical & yes & \citet{mendel2011finding,mendel2013improving,li2024new} \\104 Semi-free-start (SAT+CAS) & 38 & solver reproduction & yes & \citet{alamgir2024sha256} \\105 Collision (pure SAT) & $\le 28$ & --- & yes & \citet{alamgir2024sha256} \\106 Preimage & 43 & $2^{254.9}$ & no & \citet{aoki2009preimages} \\107 Preimage (hash / compression) & 45 / 52 & $\approx 2^{256}$ (bicliques) & no & \citet{khovratovich2012bicliques} \\108 \bottomrule109 \end{tabular}110 }111 \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.}112113\end{table}114115\subsection{Automated discovery}116117Program-search systems have produced verified mathematical constructions---matrix-multiplication tensors118\citep{fawzi2022discovering}, combinatorial bounds \citep{romeraparedes2024mathematical,novikov2025alphaevolve},119olympiad geometry proofs \citep{trinh2024solving}, conjectures in knot theory and representation theory120\citep{davies2021advancing}---and end-to-end ``AI scientist'' pipelines have been proposed \citep{lu2024ai}. None121targets standardised cryptographic primitives, where the ground truth is dominated by impossibility results, so122Axis~D has no published baseline and defines its own (rediscovery rate, false-positive rate, and the quality of the123negative results). On the formal side, \citet{boving2025interactive} make bit-vector facts about hash-function steps124machine-checkable in Lean~4 \citep{demoura2021lean}; we use this to separate checked identities from informal ones.125126\subsection{Research gaps and what the mandate already settles}127128Of the mandate's questions, the literature settles the following (\code{literature/research\_gaps.md}): A1 (no129improvement beyond constant factors from the endomorphism), A2 (orbits give exactly $\sqrt{\lvert\Aut\rvert}$), A5130(generic algorithms cannot beat $\sqrt n$, with or without preprocessing), B1 (the proof structures differ by the131conversion-function idealisation), B2 (batch verification is known for Schnorr, not for ECDSA), and C1/C2/C4 up to132the recorded step counts. What is not settled, and what we test, is quantitative and methodological: the measured133constants and their interaction with distinguished-point overheads and fruitless cycles at 20--48 bits (gap~2); the134preprocessing constant on a fixed curve (gap~3); whether an automated search over iteration-function designs or over135algebraic identities finds anything the theory does not predict (gaps~1, 8); how far generic SAT encodings get on136step-reduced SHA-256 compared with the dedicated tools (gap~6); and whether the elementary identities that137implementations rely on can be made machine-checked at negligible cost (gap~7). The closed form of the GLV138constants (Proposition~\ref{prop:glv}) is the one place where the symbolic search produced something we did not find139written down, and we are careful to call it an exposition of a known structure rather than a discovery.140