\section{Introduction}
\label{sec:intro}

The security of Bitcoin reduces to three mathematical assumptions: that discrete logarithms in the group of
rational points of the curve \secp{} cost about $\sqrt n\approx 2^{128}$ group operations, that SHA-256 is preimage-
and collision-resistant at the generic $2^{256}$ and $2^{128}$ levels, and that ECDSA and BIP340 Schnorr signatures are
unforgeable under these assumptions. The first of these is a ``square-root barrier'': in the generic-group model it
is a theorem \citep{shoup1997lower}, and the only way past it is an algorithm that exploits the specific
representation of the group. \secp{} has an unusually rich representation---a generalised-Mersenne prime, the
equation $y^2=x^3+7$ with $j$-invariant~0, complex multiplication by the Eisenstein integers and an automorphism group
of order six---and this has fed a persistent folklore that the curve's ``special structure'' might hide a shortcut.
The known mathematics says the structure yields constant factors (a $\sqrt6$ reduction in Pollard's rho, a halving of
doublings in scalar multiplication) and nothing more; the known computational records stop at 112--113 bits.

This paper asks whether a systematic, automated exploration of that structure---and of the corresponding structure
in the signature schemes and in SHA-256---can find anything the literature has missed, and it answers the question
with the discipline the question deserves. We set up a six-stage discovery pipeline (verified literature database,
structured hypotheses, exact symbolic checks, seeded experiments with provenance, machine-checked statements in
Lean~4, and a six-way classification of every outcome), executed it autonomously under a written mandate, and let
it evaluate 25 hypotheses across four axes: the algebraic structure of \secp{} (Axis~A), the complexity of generic
and preprocessing discrete-logarithm algorithms (Axis~B), reduced-step SHA-256 (Axis~C), and the methodology itself
(Axis~D). The mandate's first instruction was ``do not assume such shortcuts exist''; the paper's first result is that
none were found, and that the absence is documented quantitatively rather than asserted.

\paragraph{Contributions.} The contributions are of four kinds, and we label each with the classification it
received.

\emph{Algebraic structure (known results reproduced, with one explicit form we did not find written down).} We
verify every \secp{} parameter and derived invariant twice with exact arithmetic (Python and PARI/GP), prove that
$\End(E)=\Z[\omega]$ leaves no endomorphism to exploit beyond the six automorphisms, and show that the GLV lattice is
the Eisenstein ideal $(\bar\pi-1)$, so that the constants hard-coded in \libsecp{} are literally
$a_1=(t-f)/2-1$, $b_1=-f$, $a_2=a_1-b_1$, $b_2=a_1$ with $4p=t^2+3f^2$ (Proposition~\ref{prop:glv}). The pipeline's
identity search found this on its own (as ``$t^2+3b_1^2=4p$'') among 22 exact identities and 0 false positives. We
prove that the automorphism orbits admit no compatible group structure (Proposition~\ref{prop:noquotient}), closing
the most natural ``beyond $\sqrt6$'' idea, and we quantify why summation-polynomial index calculus does not beat
$\sqrt n$ over prime fields.

\emph{Algorithmic complexity (known results reproduced with precise constants; one rejected shortcut).} A native
engine solved $6\,240$ synthetic ECDLP instances of 20--56 bits, all verified. The fitted exponents are
$0.48$--$0.50$; the rho constant is $1.254\sqrt n$ against the random-mapping prediction $1.2533$; the order-6
automorphism classes reduce iterations by $2.42\times$ ($\sqrt6=2.449$) but, in our implementation, save no wall-clock
time because canonicalisation costs as much as a group addition---a point the literature's record computations
solve with engineering we did not replicate. Parallel collision search reaches $22\times$ on 28 threads;
time--memory curves match $m+n/(2m)$ for BSGS and show the two-sided optimum of distinguished-point rho; discrete
logarithms with preprocessing cost $1.5\sqrt{n/T}$ online after $T$ stored points. An automated sweep over 25
iteration-function designs found nothing below the random-mapping constant (rejected shortcut). Batch verification
of BIP340 signatures reaches $3.1\times$ over single verification in the same arithmetic and saturates for an
identified reason.

\emph{SHA-256 (empirical observations and known results reproduced).} Reduced-step experiments quantify diffusion
and statistical regularity as functions of the step count, calibrate generic SAT and SMT encodings for preimage and
collision search against the published dedicated-tool records, and reproduce the 9-step local collision in both
the linearised and the real model; nothing bears on the 64-step function (Sections~\ref{sec:sha} and~\ref{sec:results}).

\emph{Methodology and formal verification.} Bit-level identities that implementations rely on---the optimised forms
of $\Ch$ and $\Maj$, linearity and bijectivity of the $\Sigma$ functions, the bijectivity of the SHA-256 step and
the invertibility of the message schedule---and the abstract-group facts behind ECDSA malleability and Schnorr
correctness are machine-checked in Lean~4 (Section~\ref{sec:formal}). The pipeline's record (Table~\ref{tab:hypotheses})
is a majority of known results reproduced with quantified constants, two rejected conjectures with proofs or
counterexamples, several empirical observations, and no claim of novelty beyond exposition; we argue that this is
the correct output of an autonomous agent on this problem, and that the discipline---operation counts next to
timings, two implementations per component, provenance on every number, formal statements kept separate from
informal ones---is the transferable contribution.

\paragraph{Scope and integrity.} All attacks were run on synthetic curves and keys generated by the experiments; no
real key, address or blockchain datum was used; full-strength primitives were analysed only through legitimate
implementations and exact algebra. The repository releases every script, result and figure source with a
reproducibility statement (Appendix~\ref{app:repro}).

\paragraph{Organisation.} Section~\ref{sec:foundations} fixes the mathematical foundations and the meaning of the
barrier; Section~\ref{sec:lit} reviews the literature and the research gaps; Sections~\ref{sec:secp}--\ref{sec:sha}
develop the theory of the three axes with the algebraic results; Section~\ref{sec:framework} describes the discovery
pipeline; Sections~\ref{sec:design} and~\ref{sec:results} give the experimental design and results;
Section~\ref{sec:formal} lists the formal results and the negative findings; Sections~\ref{sec:implications}
and~\ref{sec:limitations} discuss implications and limitations; Section~\ref{sec:conclusion} concludes.