"""Emit the 25 hypothesis records (hypotheses/HNN-*.md). Edit this file to update statuses/verdicts, then rerun.
Statuses/verdicts are updated as results arrive; evidence paths must exist (registry.py warns otherwise)."""
import pathlib, yaml
ROOT = pathlib.Path(__file__).resolve().parents[1]
H = []
def add(**kw): H.append(kw)

add(id="H01", title="Standardised secp256k1 parameters and GLV constants are exactly consistent", axis="A", kind="algebraic",
    statement="p and n are prime, G ∈ E, [n]G = O, h = 1, β³ ≡ 1 (mod p), λ³ ≡ 1 (mod n), φ(G) = (βG_x, G_y) = [λ]G, the libsecp256k1 lattice basis satisfies a_i + b_i λ ≡ 0 (mod n) and has determinant n.",
    motivation="Every later result depends on these constants; an error here would invalidate the study.",
    assumptions="SEC 2 v2.0 parameter values; libsecp256k1 scalar_impl.h constants.",
    expected_contribution="Independent two-implementation verification (pure Python and PARI/GP).",
    related_work=["certicom2010sec2", "gallant2001faster", "wuille2013libsecp256k1"],
    possible_counterexamples="A transcription error in any constant; a wrong pairing of β with λ (β with λ² fails).",
    verification_strategy="experiments/baselines/secp256k1_facts.py: 14 named facts computed in Python and PARI/GP must agree.",
    computational_budget="seconds", status="evaluated", classification="known_reproduced",
    evidence=["results/baselines/secp256k1_facts.json"],
    verdict="All 14 facts agree between Python and PARI/GP; (β, λ²) mismatch confirmed as expected.",
    commands=[".venv/bin/python experiments/baselines/secp256k1_facts.py"])
add(id="H02", title="End(E) = Z[ω] and the GLV basis is the Eisenstein ideal (π̄ − 1): closed form of the libsecp256k1 constants", axis="A", kind="algebraic",
    statement="For secp256k1, t² − 4p = −3f² with f integral; End(E) = Z[ω]; the GLV lattice {(k1,k2): k1 + k2 λ ≡ 0 (mod n)} is the principal ideal (π̄−1)Z[ω] and a1 = (t−f)/2 − 1, b1 = −f, a2 = a1 − b1, b2 = a1, with a1² − a1 b1 + b1² = n.",
    motivation="Research question A1: are there efficiently computable endomorphisms beyond the automorphisms? CM theory says no; the closed form explains the 'magic' constants.",
    assumptions="E ordinary, p ≡ 1 (mod 3), j = 0.",
    expected_contribution="Explanation of constants usually presented as output of the extended Euclidean algorithm; proof that no endomorphism outside Z[φ] exists.",
    related_work=["gallant2001faster", "sica2002analysis", "galbraith2011endomorphisms", "silverman2009arithmetic"],
    possible_counterexamples="If a1 ≠ (t−f)/2 − 1 exactly, the ideal description would be wrong (it was checked exactly).",
    verification_strategy="Exact integer check of the closed form; identity search Q1/Q3; extended-Euclid re-derivation.",
    computational_budget="seconds", status="evaluated", classification="known_reproduced",
    evidence=["results/automated_discovery/identity_search.json", "results/baselines/secp256k1_facts.json"],
    verdict="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.",
    commands=[".venv/bin/python experiments/automated_discovery/identity_search.py"])
add(id="H03", title="GLV decomposition halves doublings; sub-scalars never exceed 128 bits", axis="A", kind="algebraic",
    statement="With the published basis, |k1|, |k2| < 2^128 for every k, and [k]P via interleaved wNAF uses ≈ 128 doublings instead of 256, giving ≈ 1.65× fewer group operations than wNAF alone.",
    motivation="Quantify the known constant-factor gain exactly in operation counts (A3).",
    assumptions="Affine operation model; wNAF window 4–5.", expected_contribution="Exact operation counts for the paper's baseline table.",
    related_work=["gallant2001faster", "sica2002analysis", "hankerson2004guide"],
    possible_counterexamples="A scalar with a 129-bit component (none found in 2 200 samples; the Sica–Ciet–Quisquater bound guarantees ≤ 128 + small).",
    verification_strategy="experiments/baselines/scalar_mult_opcount.py on 200 random scalars, all methods return the same point.",
    computational_budget="seconds", status="evaluated", classification="known_reproduced",
    evidence=["results/baselines/scalar_mult_opcount.json"],
    verdict="Max sub-scalar size 128 bits; 184 vs 304 group ops (GLV+wNAF vs wNAF), 2.07× vs double-and-add.",
    commands=[".venv/bin/python experiments/baselines/scalar_mult_opcount.py"])
add(id="H04", title="Automorphism orbits give exactly √6 on Pollard rho, with measurable fruitless-cycle overhead", axis="A", kind="algebraic",
    statement="On synthetic j = 0 prime-order curves, rho on classes of size 6 needs √6 fewer iterations than plain rho (and √2 for the negation map alone), up to fruitless-cycle handling costs.",
    motivation="Research question A2 (equivalence classes reduce redundant computation).",
    assumptions="Random-mapping heuristic; Teske r-adding walk r = 20.",
    expected_contribution="Precise measurement of the achieved versus theoretical factor and of the cycle overhead.",
    related_work=["wiener1999faster", "duursma1999speeding", "gallant2000improving", "bos2010negation", "bernstein2011correct"],
    possible_counterexamples="Achieved factor materially below √6 because of fruitless cycles or canonicalisation cost.",
    verification_strategy="Rust engine: rho_dp1 vs rho_dp1_neg vs rho_dp1_aut3 vs rho_dp1_neg_aut3 on 20 j = 0 curves per size.",
    computational_budget="≈ 1 node-hour", status="evaluated", classification="known_reproduced", evidence=['results/synthetic_ecdlp/scaling_j0_M2U64.json', 'results/synthetic_ecdlp/analysis.json'],
    verdict='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 √6 = 2.449; constant 0.499·√n vs √(π/12) = 0.512; negation alone 1.29 vs √2, φ-orbits alone 1.52 vs √3; fruitless cycles ≤ 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.')
add(id="H05", title="The automorphism orbit set cannot be made a group of order n/6 (rejected conjecture)", axis="A", kind="algebraic",
    statement="Conjecture: the quotient E(F_p)/Aut(E) inherits a group law making the DLP a problem of size n/6. Reality: the orbit relation is not a congruence (P ~ φP does not imply P + Q ~ φP + Q).",
    motivation="A natural 'beyond √6' idea; must be ruled out explicitly (A5).",
    assumptions="Aut(E) ≅ Z/6 acting by automorphisms fixing O.",
    expected_contribution="Negative result with proof and computed counterexamples.",
    related_work=["wiener1999faster", "silverman2009arithmetic"],
    possible_counterexamples="None: the statement is refuted by a single pair.",
    verification_strategy="theory/elliptic_curves/orbit_quotient_counterexample.py: 500 random pairs on 16/20/24-bit curves.",
    computational_budget="seconds", status="evaluated", classification="rejected",
    evidence=["results/theory/orbit_quotient_counterexample.json"],
    verdict="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 ≠ |H| = 1.",
    commands=[".venv/bin/python theory/elliptic_curves/orbit_quotient_counterexample.py"])
add(id="H06", title="No known algebraic attack applies to secp256k1; prime-field index calculus with m = 2 costs ≫ √n", axis="A", kind="algebraic",
    statement="n ≠ p; the embedding degree exceeds 10^6 (in fact it is the full order of p mod n); the twist has a 220-bit prime cofactor; x³ + 7 has no roots (no 2-torsion) and 7 is a non-residue (no x = 0 points); Semaev decomposition with |F| ≈ √p succeeds for a random point with probability 1 − exp(−|F|²/2n) but the cost of a relation is |F|/rate ≫ √n per relation and |F| relations are needed.",
    motivation="Section 3.2 of the mandate: applicability limits of algebraic attacks.",
    assumptions="Standard reductions (MOV/Frey–Rück, Semaev/Smart/Satoh–Araki, Semaev 2004).",
    expected_contribution="Exact verification table plus an empirical decomposition experiment on 16–28-bit curves.",
    related_work=["menezes1993reducing", "frey1994remark", "smart1999discrete", "semaev2004summation", "gaudry2009index", "diem2011discrete", "petit2012elliptic", "bernstein2014safecurves"],
    possible_counterexamples="A small embedding degree or anomalous order (both excluded exactly).",
    verification_strategy="secp256k1_facts.py (exact) and experiments/synthetic_ecdlp/index_calculus_probe.py.",
    computational_budget="seconds", status="evaluated", classification="known_reproduced",
    evidence=["results/baselines/secp256k1_facts.json", "results/synthetic_ecdlp/index_calculus_probe.json"],
    verdict="All exclusion criteria verified; measured decomposition rates match the Poisson prediction within sampling error; even with a free decomposition oracle the relation stage costs ≥ 2.4√n and the linear algebra |F|² ≫ √n.",
    commands=[".venv/bin/python experiments/synthetic_ecdlp/index_calculus_probe.py"])
add(id="H07", title="An exhaustive small-coefficient identity search finds only CM-explained relations and no cross-modulus or generator-specific relation", axis="A", kind="algebraic",
    statement="Among 58 064 candidate relations (binary quadratic forms, modular quadratics, GLV linear relations, cross-modulus and generator relations), every identity found is implied by β, λ being cube roots of unity and by the Eisenstein-ideal structure; the negative-control spaces Q4/Q5 return 0 hits.",
    motivation="Stage 2–3 automation: can a dumb generator rediscover structure, and does it hallucinate structure where there is none?",
    assumptions="Coefficient bound 6; constant set {p, n, t, f, a1, b1, a2, b2, β, λ, Gx, Gy}.",
    expected_contribution="Calibration of the discovery engine (true positives explained, false positives zero).",
    related_work=["gallant2001faster", "sica2002analysis"],
    possible_counterexamples="A relation involving Gx or Gy would indicate a non-random generator (none).",
    verification_strategy="experiments/automated_discovery/identity_search.py", computational_budget="seconds",
    status="evaluated", classification="empirical_observation", evidence=["results/automated_discovery/identity_search.json"],
    verdict="22 identities found, 22 explained, 0 unexplained, 0 false positives (expected chance hits 10^-73).",
    commands=[".venv/bin/python experiments/automated_discovery/identity_search.py"])
# ---- Axis B: algorithmic complexity ----
add(id="H08", title="Measured ECDLP cost scales as n^0.5 with constants matching random-mapping theory", axis="B", kind="algorithmic",
    statement="Fitting T(n) = a n^α (log n)^β to measured group-operation counts for BSGS, rho (Floyd/Brent/DP) and kangaroo on 20–48-bit prime-order curves gives α = 0.50 ± 0.02 and constants ≈ 2 (BSGS), ≈ √(π/2) ≈ 1.25 (rho), ≈ 2 (kangaroo on the full interval).",
    motivation="Reproducible baseline before any novel algorithm (mandate §9).",
    assumptions="Teske r = 20 walk; distinguished-point fraction tuned per size.",
    expected_contribution="Baseline table and log–log scaling figure with bootstrap confidence intervals.",
    related_work=["pollard1978monte", "teske2001random", "vanoorschot1999parallel", "shanks1971class", "pollard2000kangaroos", "flajolet1990random"],
    possible_counterexamples="α significantly different from 0.5, or a rho constant below √(π/2) (which would contradict the random-mapping model).",
    verification_strategy="experiments/synthetic_ecdlp/run_scaling.py on the cluster; analysis script fits and bootstraps.",
    computational_budget="≈ 4 node-hours", status="evaluated", classification="known_reproduced", evidence=['results/synthetic_ecdlp/scaling_generic_M3U96a.json', 'results/synthetic_ecdlp/scaling_j0_M2U64.json', 'results/synthetic_ecdlp/analysis.json'],
    verdict='3 840 verified instances, 20–56 bits: fitted α ∈ [0.478, 0.500] (≥ 32 bits) for all seven configurations with CIs touching 0.5; pooled rho constant 1.254·√n [1.21, 1.30] on 480 runs vs √(π/2) = 1.2533; BSGS 1.50·√n (x-keyed ±j table); kangaroo 1.94·√n; Floyd 2.67·√n, Brent 1.65·√n.')
add(id="H09", title="Automated search over iteration-function designs cannot beat the random-mapping constant for a given class size", axis="B", kind="algorithmic",
    statement="Across r ∈ {3, 8, 16, 20, 32, 64}, mixed walks, and DP densities, no configuration achieves expected iterations below √(π n/(2·|class|)) by more than statistical noise; small r is measurably worse (Teske).",
    motivation="Research question A4/B4: can automated algorithm search discover a better generic iteration?",
    assumptions="Walks are deterministic functions of the current point (generic-group restriction).",
    expected_contribution="Negative result consistent with Shoup's bound: the design space contains no asymptotic shortcut; constant-factor ranking of designs.",
    related_work=["teske2001random", "shoup1997lower", "cheon2012speeding", "bernstein2012two"],
    possible_counterexamples="A configuration with constant < 1.25 at all sizes (would require explanation).",
    verification_strategy="Rust engine sweep on 32–40-bit curves, 40 instances per configuration.",
    computational_budget="≈ 2 node-hours", status="evaluated", classification="rejected", evidence=['results/synthetic_ecdlp/sweep_r_M3U96a.json', 'results/synthetic_ecdlp/analysis.json'],
    verdict='25 configurations × 80 instances: r = 2 and r = 3 walks cost 3.77·√n and 2.26·√n (negative control), r ≥ 8 cluster at 1.1–1.5·√n with CIs overlapping √(π/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.')
add(id="H10", title="Parallel distinguished-point collision search has near-linear speed-up up to 28 threads", axis="B", kind="algorithmic",
    statement="Wall-clock speed-up S(t) ≥ 0.8 t for t ≤ 28 threads on a Mac Studio M3 Ultra at 44–48 bits, with total group operations independent of t up to the DP overhead.",
    motivation="Measure parallel efficiency (mandate §4).", assumptions="Shared DP table; one walk per thread.",
    expected_contribution="Parallel-efficiency figure.", related_work=["vanoorschot1999parallel"],
    possible_counterexamples="Lock contention or memory bandwidth limiting S(t).",
    verification_strategy="Rust engine --threads sweep on M3U96a/M3U96b.", computational_budget="≈ 1 node-hour",
    status="evaluated", classification="known_reproduced", evidence=['results/synthetic_ecdlp/parallel_M3U96a.json', 'results/synthetic_ecdlp/analysis.json'],
    verdict='56-bit instances on an Apple M3 Ultra: 14.8× on 16 threads (efficiency 0.93), 22.1× on 28 threads (0.79, P+E cores); total group operations within a factor 1.0 of single-thread.')
add(id="H11", title="Time–memory trade-off: BSGS with memory m costs m + n/m operations; rho with DP density θ stores ≈ θ·√(πn/2) points", axis="B", kind="algorithmic",
    statement="Measured (time, memory) points for BSGS at m ∈ {n^0.25 … n^0.5} and for DP-rho at several θ lie on the predicted curves; BSGS is deterministic and rho has coefficient of variation ≈ 0.52 (Rayleigh).",
    motivation="Mandate §9: report the time–memory trade-off for each algorithm.",
    assumptions="Hash-table memory counted as entries × bytes.", expected_contribution="Trade-off figure.",
    related_work=["shanks1971class", "vanoorschot1999parallel", "bernstein2012two"],
    possible_counterexamples="Deviation from m + n/m (would indicate an implementation error).",
    verification_strategy="Rust engine bsgs --memory sweep; rho --dp sweep.", computational_budget="≈ 1 node-hour",
    status="evaluated", classification="known_reproduced", evidence=['results/synthetic_ecdlp/tmto_M2U64.json', 'results/synthetic_ecdlp/analysis.json'],
    verdict='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, ≈ √(πn/2)) to 2^-2 (restart-dominated) and 2^-14 (overshoot-dominated).')
add(id="H12", title="Discrete logarithms with preprocessing: online cost ≈ 1.5·√(n/T) after storing T distinguished points", axis="B", kind="algorithmic",
    statement="With T stored DPs produced by walks of length W = √(n/T), the online phase needs c·√(n/T) group operations with c ≈ 1.5, i.e. a per-instance speed-up of ≈ √T/1.5 over plain rho, consistent with ST² = Ω̃(n).",
    motivation="Non-uniform attacks are the one known way to go below √n per instance; measure the constant.",
    assumptions="Walk independent of the target (M_j = u_j G); DP mask ≈ log₂ W bits.",
    expected_contribution="Quantified reproduction of Bernstein–Lange on 22–26-bit groups (Python) and larger (Rust).",
    related_work=["bernstein2013nonuniform", "lee2011generic", "corrigangibbs2018discrete"],
    possible_counterexamples="Online cost not decreasing as 1/√T.",
    verification_strategy="experiments/synthetic_ecdlp/preprocessing_python.py (60 instances per cell).",
    computational_budget="≈ 10 min laptop", status="evaluated", classification="known_reproduced",
    evidence=["results/synthetic_ecdlp/preprocessing_python.json"],
    verdict="Online/√(n/T) ratio 1.48–1.67 across T = 2^4 … 2^12 at 22 and 26 bits; per-instance speed-up 2.6× → 42× as predicted by √T scaling.",
    commands=[".venv/bin/python experiments/synthetic_ecdlp/preprocessing_python.py"])
add(id="H13", title="BIP340 batch verification reduces per-signature cost by a factor that grows with batch size and saturates", axis="B", kind="algorithmic",
    statement="Verifying b signatures with random 128-bit weights and a multi-scalar multiplication costs per signature a decreasing function of b, with speed-up ≈ 2× at b = 16 and ≈ 3× or more at b ≥ 256, without changing consensus semantics.",
    motivation="Research question B2.", assumptions="Random weights; lift_x cost included.",
    expected_contribution="Measured curve with CI on two hardware platforms; operation counts of the MSM.",
    related_work=["bernstein2012high", "wuille2020bip340", "naccache1994can", "bellare1998fast", "pippenger1980evaluation"],
    possible_counterexamples="No speed-up (would indicate an MSM implementation issue).",
    verification_strategy="experiments/signature_benchmarks/sigbench (k256 arithmetic), negative control with one invalid signature.",
    computational_budget="≈ 30 min", status="evaluated", classification="known_reproduced",
    evidence=["results/signature_benchmarks/summary.json", "results/signature_benchmarks/bench_MacBookPro-de-simon-pierre-2.json", "results/signature_benchmarks/bench_MacStudnpierre2.json"],
    verdict="Per-signature cost falls from 24.5 µs (single, k256) to 7.9 µs at b = 2048 with Pippenger (S = 3.10 [3.05, 3.16]; 1.67× vs libsecp256k1 single verify); Straus plateaus at ≈ 2×; ≈ 3 µs/sig of non-MSM work (lift_x, tagged hash) caps the gain; negative control rejected; same shape on M3 Ultra.")
add(id="H14", title="Implementation choice dominates signature performance: three orders of magnitude between pure Python and libsecp256k1", axis="B", kind="algorithmic",
    statement="ECDSA/Schnorr verification spans ≈ 10³× between the pure-Python reference and libsecp256k1, with k256 within a small factor of libsecp256k1; sign and verify costs differ by the cost of the second scalar multiplication.",
    motivation="Research question B5.", assumptions="Single-threaded, prehashed messages.",
    expected_contribution="Implementation table.", related_work=["wuille2013libsecp256k1", "bernstein2012high"],
    possible_counterexamples="None (descriptive).", verification_strategy="sigbench + run_bench.py on laptop and M3U96a.",
    computational_budget="≈ 30 min", status="evaluated", classification="empirical_observation",
    evidence=["results/signature_benchmarks/summary.json"],
    verdict="Schnorr verify: 7.4 ms (pure Python) vs 24.5 µs (k256) vs 13.2 µs (libsecp256k1): 560× spread; libsecp256k1 verifies 1.9× faster than k256 while k256 signs 1.8× faster (table-based generator multiplication 8.3 µs vs blinded ecmult_gen 19.8 µs); ECDSA and Schnorr verification within 5 % in libsecp256k1.")
# ---- Axis C: SHA-256 ----
add(id="H15", title="A single-bit message difference reaches full avalanche within a small number of steps", axis="C", kind="sha256",
    statement="The mean fraction of flipped state bits after s steps reaches 0.49 within s* steps of the compression function for a single-bit difference in W_0 (s* to be measured) and the random-oracle control is at 0.5 from step 1.",
    motivation="Research question C1 (regularities of reduced rounds).", assumptions="2000 random messages per configuration.",
    expected_contribution="Diffusion heatmap and s*.", related_work=["nist2015fips180", "gilbert2003security"],
    possible_counterexamples="Flip ratio plateauing below 0.5 (would indicate a structural weakness).",
    verification_strategy="experiments/reduced_round_sha256/diffusion.py", computational_budget="minutes",
    status="evaluated", classification="known_reproduced", evidence=['results/reduced_round_sha256/summary.json', 'results/reduced_round_sha256/diffusion_seed1.json'],
    verdict='Full diffusion (mean flip ratio ≥ 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 × 2000 messages; after 64 steps Hamming weight 128.0 ± 8.1 = random-oracle control.')
add(id="H16", title="Statistically detectable input–output correlations vanish after a small number of steps", axis="C", kind="sha256",
    statement="With N = 20 000 samples, the number of (input bit, output bit) pairs with |corr| > 4/√N is large for s ≤ 4 and zero for s ≥ s** (to be measured), identical to the random-oracle control; output-byte chi-square tests are uniform beyond s**.",
    motivation="C1/C3.", assumptions="Single-block random messages.", expected_contribution="Bias figure.",
    related_work=["nist2015fips180"], possible_counterexamples="Residual correlations at 64 steps.",
    verification_strategy="experiments/reduced_round_sha256/bias_test.py", computational_budget="minutes",
    status="evaluated", classification="empirical_observation", evidence=['results/reduced_round_sha256/summary.json', 'results/reduced_round_sha256/bias_seed1.json'],
    verdict='N = 20 000 × 3 seeds: r ≤ 3 trivially biased (untouched IV registers); r = 4 bias/χ² 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σ bits in 10 752 tests, as expected by chance).')
add(id="H17", title="SAT preimage search on step-reduced SHA-256 scales exponentially in the number of steps and in the number of free bits", axis="C", kind="sha256",
    statement="For fixed free message bits k, CaDiCaL/Kissat time grows roughly exponentially with the step count s, becoming infeasible (300 s) at s ≈ s_k; SMT (Z3 bit-vectors) is slower than SAT on the same cells.",
    motivation="C2 (SAT/SMT understanding of reduced-round constraints).", assumptions="Tseitin encoding, ripple-carry adders.",
    expected_contribution="Scaling figure and table across 11 step counts × 7 free-bit counts × 2 solvers.",
    related_work=["mironov2006applications", "nejati2017adaptive", "alamgir2024sha256", "biere2024cadical", "demoura2008z3"],
    possible_counterexamples="Sub-exponential growth (would be surprising and would need explanation).",
    verification_strategy="experiments/reduced_round_sha256/preimage_sat.py on M3U96b", computational_budget="≈ 3 node-hours",
    status="evaluated", classification="empirical_observation", evidence=['results/reduced_round_sha256/summary.json', 'results/reduced_round_sha256/preimage_sat_scaling.json'],
    verdict='572 cells, all SAT answers re-hashed. r ≤ 16: solved by propagation (0 conflicts, ≤ 0.03 s) for any k. r ≥ 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 ≥ 24 cell times out at 300 s; Z3 2–4 orders of magnitude slower and times out at r ≥ 16. Generic SAT is slower than 2^16 brute force once the expansion matters.')
add(id="H18", title="Generic SAT encodings find step-reduced collisions only far below the published dedicated-tool records", axis="C", kind="sha256",
    statement="With a 600 s budget, CaDiCaL finds collisions (standard IV) for s ≤ s_c steps and semi-free-start collisions for s ≤ s_sfs, while the literature records are 31 steps (practical collision, Li et al. ASIACRYPT 2024; 37-step theoretical, 2026) and 39 steps (semi-free-start); automated generic search reproduces the easy regime only.",
    motivation="C4 (can automated searches reproduce known reduced-round results?).", assumptions="Generic encoding, no differential characteristic guidance.",
    expected_contribution="Honest calibration of generic SAT against the state of the art.",
    related_work=["nikolic2008collisions", "sanadhya2008new", "mendel2011finding", "mendel2013improving", "dobraunig2015analysis", "li2024first", "li2024new", "zhang2026collision", "alamgir2024sha256"],
    possible_counterexamples="SAT reaching ≥ 24 steps unaided (would be notable).",
    verification_strategy="experiments/reduced_round_sha256/collision_sat.py", computational_budget="≈ 3 node-hours",
    status="evaluated", classification="known_reproduced", evidence=['results/reduced_round_sha256/summary.json', 'results/reduced_round_sha256/collision_sat.json'],
    verdict='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 ≥ 20: all timeouts. Largest 18 steps vs 28 (pure SAT, Alamgir et al. 2024), 31 (Li et al. 2024), 39 SFS.')
add(id="H19", title="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", axis="C", kind="sha256",
    statement="The Chabaud–Joux/Gilbert–Handschuh correction pattern cancels any single-bit difference after 9 linearised steps (machine-checked); with modular additions the same pattern succeeds with probability ≈ 2^-c (c measured per bit position, highest at the MSB), and SAT finds conforming message words in seconds.",
    motivation="C3/C4.", assumptions="Linearisation of Ch and Maj as in Gilbert–Handschuh 2003.",
    expected_contribution="Reproduction of a classical result with a formal proof of the linear part.",
    related_work=["chabaud1998differential", "gilbert2003security", "nikolic2008collisions"],
    possible_counterexamples="Linearised cancellation failing for some δ (ruled out by bv_decide).",
    verification_strategy="experiments/reduced_round_sha256/local_collision.py + formal/ Lean theorem.",
    computational_budget="minutes", status="evaluated", classification="known_reproduced", evidence=['results/reduced_round_sha256/summary.json', 'results/reduced_round_sha256/local_collision.json', 'formal/README.md'],
    verdict='Pattern (δ, Σ0δ⊕Σ1δ, Σ1(Σ0δ), 0, δ, Σ0δ⊕Σ1δ, 0, 0, δ) cancels in the linearised model for all δ (GF(2) check + Lean theorem localCollision_absorb). Real step: 0 collisions in 32 × 100 000 samples (bound 3·10⁻⁵); survival after step i 0.25 (bits 0–30) / 1.0 (bit 31), after i+1 ≈ 10⁻⁴, after i+2 zero. SAT finds conforming pairs for all 32 positions in 4.4–118 s, all verified.')
add(id="H20", title="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", axis="C", kind="sha256",
    statement="For fixed (K_t, W_t) the step function is a bijection with an explicit inverse; W_{t−16} is determined by W_{t−15..t}; hence for any target state and any chosen message one can invert the full 64-step compression (without feed-forward) and choose the IV — the Merkle–Damgård feed-forward is what makes preimages hard.",
    motivation="Distinguish the compression function from the hash (mandate §6).", assumptions="None.",
    expected_contribution="Machine-checked statements (Lean 4 bv_decide) and an executable demonstration.",
    related_work=["nist2015fips180", "merkle1989one", "damgard1989design", "aoki2009preimages"],
    possible_counterexamples="None (theorem).", verification_strategy="formal/ theorems + tests/test_core.py step inverse test.",
    computational_budget="minutes", status="evaluated", classification="known_reproduced", evidence=['formal/README.md', 'formal/build.log', 'tests/test_formal_lean.py', 'tests/test_core.py'],
    verdict='Machine-checked: stepInv ∘ step = id and step ∘ 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.')
# ---- Axis D: methodology / formal ----
add(id="H21", title="Lean 4 bv_decide machine-checks the SHA-256 word-level identities used by optimised implementations", axis="D", kind="formal",
    statement="Ch(x,y,z) = ((y ⊕ z) ∧ x) ⊕ z, two Maj forms, GF(2)-linearity of Σ0, Σ1, σ0, σ1, bijectivity of Σ0, Σ1 and of the step function are theorems checked with LRAT certificates.",
    motivation="Stage 5: separate machine-checked statements from informal proofs.", assumptions="Lean 4.35 core BitVec semantics.",
    expected_contribution="A reusable formal library of SHA-256 identities.", related_work=["demoura2021lean", "nist2015fips180"],
    possible_counterexamples="A false identity would produce a counterexample from the SAT solver.",
    verification_strategy="lake build in formal/", computational_budget="minutes", status="evaluated", classification="known_reproduced", evidence=['formal/README.md', 'formal/build.log', 'tests/test_formal_lean.py'],
    verdict='Lean 4.35 bv_decide (LRAT certificates re-checked in Lean): Ch_opt, Maj_opt_or, Maj_opt_xor, GF(2)-linearity of Σ0, Σ1, σ0, σ1, injectivity and explicit inverses (Σ0⁻¹ = XOR of 17 rotations) hence bijectivity; clean build 32 s, no sorry, no user axiom, no Mathlib.')
add(id="H22", title="σ0 and σ1 are not injective on 32-bit words (kernel of positive dimension), unlike Σ0 and Σ1", axis="D", kind="formal",
    statement="The logical shift in σ0, σ1 makes the GF(2)-linear maps non-bijective; bv_decide or a rank computation exhibits the kernel; Σ0, Σ1 (rotations only) are bijective.",
    motivation="A small, decidable algebraic question whose answer matters for message-schedule analyses.", assumptions="None.",
    expected_contribution="Exact kernel dimensions and counterexamples.", related_work=["nist2015fips180"],
    possible_counterexamples="σ0 injective (would contradict the rank computation).",
    verification_strategy="formal/ + GF(2) rank script", computational_budget="minutes", status="evaluated", classification="rejected", evidence=['formal/README.md', 'formal/build.log', 'tests/test_formal_lean.py', 'formal/scripts/gf2_rank.py'],
    verdict='Conjecture refuted: σ0 and σ1 are bijective (bv_decide UNSAT certificates for injectivity; GF(2) rank 32 by two independent eliminations; explicit 32×32 inverse matrices verified in Lean). The shift makes each summand singular (x≫3 has rank 29; rotr7⊕rotr18 kills 0xFFFFFFFF) but the sum is a unit. A wrong belief caught by the formal layer.')
add(id="H23", title="Cross-implementation agreement is a necessary gate: every arithmetic component is checked against at least one independent implementation", axis="D", kind="methodology",
    statement="Pure Python (wp34) agrees with PARI/GP (curve facts), python-ecdsa and libsecp256k1 (ECDSA), the 19 official BIP340 vectors, hashlib (SHA-256), and the Rust engine (ECDLP answers) on every tested instance; discrepancies found during development are logged.",
    motivation="Mandate §10: validate custom mathematical code against independent references.", assumptions="None.",
    expected_contribution="Transparent record of the validation layer.", related_work=["wuille2020bip340", "pornin2013rfc6979"],
    possible_counterexamples="Any disagreement (none remained after development; the kangaroo reference initially looped because its hash ignored the retry seed — fixed and logged).",
    verification_strategy="tests/ (pytest) — all must pass.", computational_budget="minutes", status="evaluated", classification="empirical_observation",
    evidence=["tests/test_core.py", "tests/test_dlp_reference.py"],
    verdict="11 reference tests pass; agreement with 5 independent implementations; two development bugs caught by the gate (kangaroo retry loop, PARI output parsing).",
    commands=[".venv/bin/python -m pytest -q tests/test_core.py tests/test_dlp_reference.py"])
add(id="H24", title="The six-stage pipeline rediscovers known structure at a high rate and reports zero validated novel shortcuts", axis="D", kind="methodology",
    statement="Of the 25 hypotheses, the pipeline classifies the majority as known results reproduced or empirical observations, rejects the explicitly 'beyond √n' conjectures with proofs or counterexamples, and produces no claim of a cryptographic weakness; the baseline (literature lookup without computation) would have left the quantitative constants unmeasured.",
    motivation="Outcome C of the mandate (methodological contribution) must be evaluated honestly.", assumptions="Classification rubric of §7 Stage 6.",
    expected_contribution="Discovery-log statistics and a critical assessment of what automation added.",
    related_work=["fawzi2022discovering", "romeraparedes2024mathematical", "lu2024ai"],
    possible_counterexamples="A validated novel result (none).", verification_strategy="experiments/automated_discovery/registry.py",
    computational_budget="none", status="evaluated", classification="empirical_observation", evidence=["research_log/discovery_log.jsonl", "results/automated_discovery/hypothesis_summary.json"],
    verdict="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 σ0/σ1), 0 new verified results, 0 claims of weakness. Automation found one unrecorded closed form (GLV constants) and one wrong belief (σ0/σ1); the baseline (literature reading) would have left every constant unmeasured.")
add(id="H25", title="ECDSA malleability and Schnorr correctness follow from the abstract group axioms alone (formalised)", axis="D", kind="formal",
    statement="In an axiomatised cyclic group with x(−P) = x(P): if (r, s) verifies then (r, −s) verifies; and s = k + e·d implies [s]G = R + [e]P.",
    motivation="Research question B1/B4: which properties depend only on the group structure (and hence are shared by every curve)?",
    assumptions="Abstract group structure fields; modular inverses as hypotheses.", expected_contribution="Machine-checked statements of two textbook facts.",
    related_work=["schnorr1991efficient", "nist2023fips186", "wuille2020bip340"],
    possible_counterexamples="None (theorems).", verification_strategy="formal/ Lean project.", computational_budget="minutes",
    status="evaluated", classification="known_reproduced", evidence=['formal/README.md', 'formal/build.log', 'tests/test_formal_lean.py'],
    verdict='Machine-checked in an axiomatised CyclicGroup structure (fields listed in formal/README.md): schnorr_correct (s = k + e·d mod n ⟹ s•G = R + e•P), ecdsa_correct, ecdsa_malleable ((r,s) valid ⟹ (r, n−s) valid, modular inverse as witness). Only propext/Quot.sound used.')

out = ROOT / "hypotheses"; out.mkdir(exist_ok=True)
for h in H:
    body = h.pop("body", "")
    fm = yaml.safe_dump(h, sort_keys=False, allow_unicode=True, width=120)
    slug = h["title"].lower().split(":")[0].split(";")[0]
    slug = "".join(c if c.isalnum() else "-" for c in slug)[:48].strip("-")
    (out / f"{h['id']}-{slug}.md").write_text(f"---\n{fm}---\n\n# {h['id']} — {h['title']}\n\n{h['statement']}\n")
print(len(H), "hypothesis files written")