1% generated by experiments/automated_discovery/registry.py — do not edit2\begin{longtable}{@{}p{0.8cm}p{0.5cm}p{4.2cm}p{2.6cm}p{6.4cm}@{}}3\caption{Hypothesis portfolio and evaluation outcome. Classification vocabulary follows the mandate (new verified result; known result independently reproduced; conditional result; empirical observation; rejected conjecture; unresolved direction).}\label{tab:hypotheses}\\4\toprule ID & Axis & Hypothesis & Classification & Verdict \\ \midrule \endfirsthead5\toprule ID & Axis & Hypothesis & Classification & Verdict \\ \midrule \endhead6\bottomrule \endfoot7H01 & A & Standardised secp256k1 parameters and GLV constants are exactly consistent & Known result reproduced & All 14 facts agree between Python and PARI/GP; ($\beta$, $\lambda$$^2$) mismatch confirmed as expected. \\8H02 & A & End(E) = Z[$\omega$] and the GLV basis is the Eisenstein ideal ($\bar\pi$ -- 1): closed form of the libsecp256k1 constants & Known result reproduced & Closed form holds exactly; all 22 identities found by the search are explained by CM theory. Known in principle (ideal structure of the GLV lattice), the explicit identification with the published constants is a useful clarification, not new mathematics. \\9H03 & A & GLV decomposition halves doublings; sub-scalars never exceed 128 bits & Known result reproduced & Max sub-scalar size 128 bits; 184 vs 304 group ops (GLV+wNAF vs wNAF), 2.07$\times$ vs double-and-add. \\10H04 & A & Automorphism orbits give exactly $\surd$6 on Pollard rho, with measurable fruitless-cycle overhead & Known result reproduced & 180 paired instances at 44--52 bits: iteration speed-up 2.21 [2.00, 2.45] (r = 128) and 2.42 [2.19, 2.70] (r = 20) vs $\surd$6 = 2.449; constant 0.499$\cdot$$\surd$n vs $\surd$($\pi$/12) = 0.512; negation alone 1.29 vs $\surd$2, $\varphi$-orbits alone 1.52 vs $\surd$3; fruitless cycles $\le$ 0.11 per 1000 iterations. Wall-clock speed-up only 0.95 (order-6) and 0.73 (negation) because canonicalisation costs 56--83 ns vs 38 ns per plain iteration in this engine. \\11H05 & A & The automorphism orbit set cannot be made a group of order n/6 (rejected conjecture) & Rejected conjecture & Compatibility fails for 1500/1500 random pairs; proof: a congruence would make the orbit of O a subgroup H with cosets the other orbits, but orbits have size 6 $\ne$ |H| = 1. \\12H06 & A & No known algebraic attack applies to secp256k1; prime-field index calculus with m = 2 costs $\gg$ $\surd$n & Known result reproduced & All exclusion criteria verified; measured decomposition rates match the Poisson prediction within sampling error; even with a free decomposition oracle the relation stage costs $\ge$ 2.4$\surd$n and the linear algebra |F|$^2$ $\gg$ $\surd$n. \\13H07 & A & An exhaustive small-coefficient identity search finds only CM-explained relations and no cross-modulus or generator-specific relation & Empirical observation & 22 identities found, 22 explained, 0 unexplained, 0 false positives (expected chance hits 10\^{}-73). \\14H08 & B & Measured ECDLP cost scales as n\^{}0.5 with constants matching random-mapping theory & Known result reproduced & 3 840 verified instances, 20--56 bits: fitted $\alpha$ $\in$ [0.478, 0.500] ($\ge$ 32 bits) for all seven configurations with CIs touching 0.5; pooled rho constant 1.254$\cdot$$\surd$n [1.21, 1.30] on 480 runs vs $\surd$($\pi$/2) = 1.2533; BSGS 1.50$\cdot$$\surd$n (x-keyed $\pm$j table); kangaroo 1.94$\cdot$$\surd$n; Floyd 2.67$\cdot$$\surd$n, Brent 1.65$\cdot$$\surd$n. \\15H09 & B & Automated search over iteration-function designs cannot beat the random-mapping constant for a given class size & Rejected conjecture & 25 configurations $\times$ 80 instances: r = 2 and r = 3 walks cost 3.77$\cdot$$\surd$n and 2.26$\cdot$$\surd$n (negative control), r $\ge$ 8 cluster at 1.1--1.5$\cdot$$\surd$n with CIs overlapping $\surd$($\pi$/2); mixed walks indistinguishable; best cell r32 at 1.10 [0.92, 1.28] not significantly below the random-mapping constant. No generic iteration design beats the random-mapping floor. \\16H10 & B & Parallel distinguished-point collision search has near-linear speed-up up to 28 threads & Known result reproduced & 56-bit instances on an Apple M3 Ultra: 14.8$\times$ on 16 threads (efficiency 0.93), 22.1$\times$ on 28 threads (0.79, P+E cores); total group operations within a factor 1.0 of single-thread. \\17H11 & B & Time--memory trade-off: BSGS with memory m costs m + n/m operations; rho with DP density $\theta$ stores $\approx$ $\theta$$\cdot$$\surd$($\pi$n/2) points & Known result reproduced & BSGS cost matches m + n/(2m) within 7.8 \% for m from 2\^{}10 to 2\^{}20 at 36 bits; DP-rho at 40 bits spans 1.17--4.95 M operations as the DP density goes from 2\^{}-12 (optimum, $\approx$ $\surd$($\pi$n/2)) to 2\^{}-2 (restart-dominated) and 2\^{}-14 (overshoot-dominated). \\18H12 & B & Discrete logarithms with preprocessing: online cost $\approx$ 1.5$\cdot$$\surd$(n/T) after storing T distinguished points & Known result reproduced & Online/$\surd$(n/T) ratio 1.48--1.67 across T = 2\^{}4 \ldots{} 2\^{}12 at 22 and 26 bits; per-instance speed-up 2.6$\times$ $\to$ 42$\times$ as predicted by $\surd$T scaling. \\19H13 & B & BIP340 batch verification reduces per-signature cost by a factor that grows with batch size and saturates & Known result reproduced & Per-signature cost falls from 24.5 $\mu$s (single, k256) to 7.9 $\mu$s at b = 2048 with Pippenger (S = 3.10 [3.05, 3.16]; 1.67$\times$ vs libsecp256k1 single verify); Straus plateaus at $\approx$ 2$\times$; $\approx$ 3 $\mu$s/sig of non-MSM work (lift\_x, tagged hash) caps the gain; negative control rejected; same shape on M3 Ultra. \\20H14 & B & Implementation choice dominates signature performance: three orders of magnitude between pure Python and libsecp256k1 & Empirical observation & Schnorr verify: 7.4 ms (pure Python) vs 24.5 $\mu$s (k256) vs 13.2 $\mu$s (libsecp256k1): 560$\times$ spread; libsecp256k1 verifies 1.9$\times$ faster than k256 while k256 signs 1.8$\times$ faster (table-based generator multiplication 8.3 $\mu$s vs blinded ecmult\_gen 19.8 $\mu$s); ECDSA and Schnorr verification within 5 \% in libsecp256k1. \\21H15 & C & A single-bit message difference reaches full avalanche within a small number of steps & Known result reproduced & Full diffusion (mean flip ratio $\ge$ 0.49) at step 6 for a W\_0 bit, 11 for W\_5, 21 for W\_15 (6 steps after entry), 8 for an IV bit; identical over 3 seeds $\times$ 2000 messages; after 64 steps Hamming weight 128.0 $\pm$ 8.1 = random-oracle control. \\22H16 & C & Statistically detectable input--output correlations vanish after a small number of steps & Empirical observation & N = 20 000 $\times$ 3 seeds: r $\le$ 3 trivially biased (untouched IV registers); r = 4 bias/$\chi$$^2$ at noise but 6--13 |corr| = 1 pairs (LSB of e\_1 affine in LSB of W\_0); from r = 5 all statistics at the random-oracle floor through r = 64 (two isolated 4.1$\sigma$ bits in 10 752 tests, as expected by chance). \\23H17 & C & SAT preimage search on step-reduced SHA-256 scales exponentially in the number of steps and in the number of free bits & Empirical observation & 572 cells, all SAT answers re-hashed. r $\le$ 16: solved by propagation (0 conflicts, $\le$ 0.03 s) for any k. r $\ge$ 20: only k = 16 solved (CaDiCaL 6.4 s at r = 20, 87 s at r = 32, 262 s at r = 64 for 2/3 seeds); every k $\ge$ 24 cell times out at 300 s; Z3 2--4 orders of magnitude slower and times out at r $\ge$ 16. Generic SAT is slower than 2\^{}16 brute force once the expansion matters. \\24H18 & C & Generic SAT encodings find step-reduced collisions only far below the published dedicated-tool records & Known result reproduced & 264 cells, 119 collisions verified. r = 4, 6, 8: UNSAT in all variants/solvers/seeds (72 runs) --- no collision within the words an 8-step compression reads. r = 10--16: 0-conflict collisions differing in exactly 9 consecutive words (a terminal local collision). r = 18: 53 s standard IV, 7--10 s semi-free-start. r $\ge$ 20: all timeouts. Largest 18 steps vs 28 (pure SAT, Alamgir et al. 2024), 31 (Li et al. 2024), 39 SFS. \\25H19 & C & The 9-step local collision holds with probability 1 in the XOR-linearised model and with low, position-dependent probability in the real step function & Known result reproduced & Pattern ($\delta$, $\Sigma$0$\delta$$\oplus$$\Sigma$1$\delta$, $\Sigma$1($\Sigma$0$\delta$), 0, $\delta$, $\Sigma$0$\delta$$\oplus$$\Sigma$1$\delta$, 0, 0, $\delta$) cancels in the linearised model for all $\delta$ (GF(2) check + Lean theorem localCollision\_absorb). Real step: 0 collisions in 32 $\times$ 100 000 samples (bound 3$\cdot$10$^{-5}$); survival after step i 0.25 (bits 0--30) / 1.0 (bit 31), after i+1 $\approx$ 10$^{-4}$, after i+2 zero. SAT finds conforming pairs for all 32 positions in 4.4--118 s, all verified. \\26H20 & C & The SHA-256 step is a bijection on the state and the message schedule is invertible, so free-start and pseudo-preimage problems on the compression function are trivial & Known result reproduced & Machine-checked: stepInv $\circ$ step = id and step $\circ$ stepInv = id (per-component SAT lemmas, AIG 2048/2420), steps\_bijective for any number of rounds, scheduleStep\_inv and schedule\_backward; executable demonstration in tests/test\_core.py. Consequence (pseudo-preimages of the feed-forward-free compression function are free) stated informally. \\27H21 & D & Lean 4 bv\_decide machine-checks the SHA-256 word-level identities used by optimised implementations & Known result reproduced & Lean 4.35 bv\_decide (LRAT certificates re-checked in Lean): Ch\_opt, Maj\_opt\_or, Maj\_opt\_xor, GF(2)-linearity of $\Sigma$0, $\Sigma$1, $\sigma$0, $\sigma$1, injectivity and explicit inverses ($\Sigma$0$^{-1}$ = XOR of 17 rotations) hence bijectivity; clean build 32 s, no sorry, no user axiom, no Mathlib. \\28H22 & D & $\sigma$0 and $\sigma$1 are not injective on 32-bit words (kernel of positive dimension), unlike $\Sigma$0 and $\Sigma$1 & Rejected conjecture & Conjecture refuted: $\sigma$0 and $\sigma$1 are bijective (bv\_decide UNSAT certificates for injectivity; GF(2) rank 32 by two independent eliminations; explicit 32$\times$32 inverse matrices verified in Lean). The shift makes each summand singular (x$\gg$3 has rank 29; rotr7$\oplus$rotr18 kills 0xFFFFFFFF) but the sum is a unit. A wrong belief caught by the formal layer. \\29H23 & D & Cross-implementation agreement is a necessary gate: every arithmetic component is checked against at least one independent implementation & Empirical observation & 11 reference tests pass; agreement with 5 independent implementations; two development bugs caught by the gate (kangaroo retry loop, PARI output parsing). \\30H24 & D & The six-stage pipeline rediscovers known structure at a high rate and reports zero validated novel shortcuts & Empirical observation & 25 hypotheses evaluated: 16 known results reproduced with measured constants, 6 empirical observations, 3 rejected conjectures (orbit quotient group; iteration-function shortcut; non-injectivity of $\sigma$0/$\sigma$1), 0 new verified results, 0 claims of weakness. Automation found one unrecorded closed form (GLV constants) and one wrong belief ($\sigma$0/$\sigma$1); the baseline (literature reading) would have left every constant unmeasured. \\31H25 & D & ECDSA malleability and Schnorr correctness follow from the abstract group axioms alone (formalised) & Known result reproduced & Machine-checked in an axiomatised CyclicGroup structure (fields listed in formal/README.md): schnorr\_correct (s = k + e$\cdot$d mod n $\Rightarrow$ s$\cdot$G = R + e$\cdot$P), ecdsa\_correct, ecdsa\_malleable ((r,s) valid $\Rightarrow$ (r, n--s) valid, modular inverse as witness). Only propext/Quot.sound used. \\32\end{longtable}33