1\section{Introduction}2\label{sec:intro}34The security of Bitcoin reduces to three mathematical assumptions: that discrete logarithms in the group of5rational points of the curve \secp{} cost about $\sqrt n\approx 2^{128}$ group operations, that SHA-256 is preimage-6and collision-resistant at the generic $2^{256}$ and $2^{128}$ levels, and that ECDSA and BIP340 Schnorr signatures are7unforgeable under these assumptions. The first of these is a ``square-root barrier'': in the generic-group model it8is a theorem \citep{shoup1997lower}, and the only way past it is an algorithm that exploits the specific9representation of the group. \secp{} has an unusually rich representation---a generalised-Mersenne prime, the10equation $y^2=x^3+7$ with $j$-invariant~0, complex multiplication by the Eisenstein integers and an automorphism group11of order six---and this has fed a persistent folklore that the curve's ``special structure'' might hide a shortcut.12The known mathematics says the structure yields constant factors (a $\sqrt6$ reduction in Pollard's rho, a halving of13doublings in scalar multiplication) and nothing more; the known computational records stop at 112--113 bits.1415This paper asks whether a systematic, automated exploration of that structure---and of the corresponding structure16in the signature schemes and in SHA-256---can find anything the literature has missed, and it answers the question17with the discipline the question deserves. We set up a six-stage discovery pipeline (verified literature database,18structured hypotheses, exact symbolic checks, seeded experiments with provenance, machine-checked statements in19Lean~4, and a six-way classification of every outcome), executed it autonomously under a written mandate, and let20it evaluate 25 hypotheses across four axes: the algebraic structure of \secp{} (Axis~A), the complexity of generic21and preprocessing discrete-logarithm algorithms (Axis~B), reduced-step SHA-256 (Axis~C), and the methodology itself22(Axis~D). The mandate's first instruction was ``do not assume such shortcuts exist''; the paper's first result is that23none were found, and that the absence is documented quantitatively rather than asserted.2425\paragraph{Contributions.} The contributions are of four kinds, and we label each with the classification it26received.2728\emph{Algebraic structure (known results reproduced, with one explicit form we did not find written down).} We29verify every \secp{} parameter and derived invariant twice with exact arithmetic (Python and PARI/GP), prove that30$\End(E)=\Z[\omega]$ leaves no endomorphism to exploit beyond the six automorphisms, and show that the GLV lattice is31the Eisenstein ideal $(\bar\pi-1)$, so that the constants hard-coded in \libsecp{} are literally32$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's33identity search found this on its own (as ``$t^2+3b_1^2=4p$'') among 22 exact identities and 0 false positives. We34prove that the automorphism orbits admit no compatible group structure (Proposition~\ref{prop:noquotient}), closing35the most natural ``beyond $\sqrt6$'' idea, and we quantify why summation-polynomial index calculus does not beat36$\sqrt n$ over prime fields.3738\emph{Algorithmic complexity (known results reproduced with precise constants; one rejected shortcut).} A native39engine solved $6\,240$ synthetic ECDLP instances of 20--56 bits, all verified. The fitted exponents are40$0.48$--$0.50$; the rho constant is $1.254\sqrt n$ against the random-mapping prediction $1.2533$; the order-641automorphism classes reduce iterations by $2.42\times$ ($\sqrt6=2.449$) but, in our implementation, save no wall-clock42time because canonicalisation costs as much as a group addition---a point the literature's record computations43solve with engineering we did not replicate. Parallel collision search reaches $22\times$ on 28 threads;44time--memory curves match $m+n/(2m)$ for BSGS and show the two-sided optimum of distinguished-point rho; discrete45logarithms with preprocessing cost $1.5\sqrt{n/T}$ online after $T$ stored points. An automated sweep over 2546iteration-function designs found nothing below the random-mapping constant (rejected shortcut). Batch verification47of BIP340 signatures reaches $3.1\times$ over single verification in the same arithmetic and saturates for an48identified reason.4950\emph{SHA-256 (empirical observations and known results reproduced).} Reduced-step experiments quantify diffusion51and statistical regularity as functions of the step count, calibrate generic SAT and SMT encodings for preimage and52collision search against the published dedicated-tool records, and reproduce the 9-step local collision in both53the linearised and the real model; nothing bears on the 64-step function (Sections~\ref{sec:sha} and~\ref{sec:results}).5455\emph{Methodology and formal verification.} Bit-level identities that implementations rely on---the optimised forms56of $\Ch$ and $\Maj$, linearity and bijectivity of the $\Sigma$ functions, the bijectivity of the SHA-256 step and57the invertibility of the message schedule---and the abstract-group facts behind ECDSA malleability and Schnorr58correctness are machine-checked in Lean~4 (Section~\ref{sec:formal}). The pipeline's record (Table~\ref{tab:hypotheses})59is a majority of known results reproduced with quantified constants, two rejected conjectures with proofs or60counterexamples, several empirical observations, and no claim of novelty beyond exposition; we argue that this is61the correct output of an autonomous agent on this problem, and that the discipline---operation counts next to62timings, two implementations per component, provenance on every number, formal statements kept separate from63informal ones---is the transferable contribution.6465\paragraph{Scope and integrity.} All attacks were run on synthetic curves and keys generated by the experiments; no66real key, address or blockchain datum was used; full-strength primitives were analysed only through legitimate67implementations and exact algebra. The repository releases every script, result and figure source with a68reproducibility statement (Appendix~\ref{app:repro}).6970\paragraph{Organisation.} Section~\ref{sec:foundations} fixes the mathematical foundations and the meaning of the71barrier; Section~\ref{sec:lit} reviews the literature and the research gaps; Sections~\ref{sec:secp}--\ref{sec:sha}72develop the theory of the three axes with the algebraic results; Section~\ref{sec:framework} describes the discovery73pipeline; Sections~\ref{sec:design} and~\ref{sec:results} give the experimental design and results;74Section~\ref{sec:formal} lists the formal results and the negative findings; Sections~\ref{sec:implications}75and~\ref{sec:limitations} discuss implications and limitations; Section~\ref{sec:conclusion} concludes.76