secp256k1 research state

One operator view for the current decision, formal substrate, evidence, active work, and generated trust checks.

Canonical snapshot snapshot 296 ledger rows / ~257 distinct

Scope boundary. The environment maps and verifies the research boundary. It does not solve the plain secp256k1 discrete logarithm problem. Monitoring means new evidence can reopen a route; it does not mean impossibility was proved.

296

ledger rows

~257

distinct results

164

proved modules

486

corpus claims

routes evaluated

routes selected

Current operating state

The decision layer controls what work is justified; proof volume does not select an attack route.

Reference deployment

RS-2026-07-22-001Select none

No experiment is currently authorized.

No audited route currently satisfies every proposal-level requirement for a new experiment against the primary plain single-target secp256k1 objective.

Why this decision

Canonical rationale, not a claim of impossibility

The generic lower bound and generic algorithms are guardrails or baselines, not non-generic attack mechanisms.
GLV supplies a verified constant-factor structure; Pohlig-Hellman, low-degree pairing transfer, anomalous lifting, and extension-field descent fail target-specific applicability screens.
The open prime-field algebraic, GLV-Semaev, Petit-style, EDS/division-polynomial, and transfer directions do not yet provide an exact nonredundant mechanism plus a justified subgeneric cost bridge.
Multi-target, interval, leakage, implementation, and quantum routes change the input or computational threat model and therefore cannot be promoted as a classical plain-input result.
Building conditional Mathlib foundations now would increase theorem volume without a demonstrated reduction in uncertainty about the exact target.

Route portfolio

All routes are bound to an exact threat model, evidence gate, stop condition, and next action.

Open detailed route map

Disposition distribution

17 canonical routes

Guardrail 1Baseline 1Constant factor 1Ruled out for target 4Open, parked 4Monitor 1Conditional inputs 2Separate threat model 3

Route	Disposition	Threat model	Priority	Next action
Generic-group lower boundR-GENERIC-LOWER-BOUND	Guardrail	classical-generic	P0	Retain as a mandatory comparison and scope guard; no new experiment.
Baby-step giant-step and Pollard rhoR-GENERIC-BASELINE	Baseline	classical-single-target-plain, classical-generic	P0	Use as the benchmark comparator in the evaluation harness.
GLV endomorphism accelerationR-GLV	Constant factor	classical-single-target-plain	P0	Keep as target structure available to a selected route; do not treat it as a standalone attack.
Pohlig-Hellman subgroup reductionR-POHLIG-HELLMAN	Ruled out for target	classical-single-target-plain	P0	Retain as a machine-checked elimination certificate.
MOV, Frey-Ruck, and Tate/Weil pairing transferR-PAIRING-TRANSFER	Ruled out for target	classical-single-target-plain	P0	Keep the target-specific exclusion; defer a full pairing library unless a new route needs it.
Smart, Satoh-Araki, and Semaev anomalous-curve liftingR-ANOMALOUS-PADIC	Ruled out for target	classical-single-target-plain	P0	Retain the formal exclusion; do not build an elliptic formal-group stack for this target now.
Weil descent and GHS-style transferR-WEIL-DESCENT	Ruled out for target	classical-single-target-plain	P1	Document as a target-applicability exclusion; no formal stack now.
Prime-field index calculusR-PRIME-FIELD-INDEX-CALCULUS	Open, parked	classical-single-target-plain	P1	Preserve evidence and prerequisites; wait for explicit route selection before any new experiment.
GLV-symmetrized Semaev systemsR-GLV-SEMAEV	Open, parked	classical-single-target-plain	P1	Keep HYP_GLV_SEMAEV_001 parked until route selection explicitly promotes it.
Petit-style composed rational mapsR-PETIT-COMPOSED-MAPS	Open, parked	classical-single-target-plain	P2	Park until the source specification and route-selection gate justify implementation.
Elliptic divisibility sequences and division-polynomial re-encodingsR-EDS-DIVISION-POLYNOMIAL	Open, parked	classical-single-target-plain	P2	Keep HYP_WARD_EDS_001 parked; finish no additional point-division bridge unless a selected route needs it.
Isogeny, endomorphism-ring, and Frobenius transferR-ISOGENY-ENDOMORPHISM-TRANSFER	Monitor	classical-single-target-plain	P3	Monitor literature and reuse GLV facts; no build now.
Multi-target and reusable-precomputation tradeoffsR-MULTI-TARGET-PRECOMPUTATION	Conditional inputs	classical-conditioned	P1	Represent in the evaluation contract; no experiment in this phase.
Interval DLP, partial-key knowledge, and auxiliary-power algorithmsR-INTERVAL-AUXILIARY-INPUT	Conditional inputs	classical-conditioned	P2	Keep as a scope category for future protocol or leakage analyses.
Hidden-number and lattice attacks on biased or reused ECDSA noncesR-HNP-NONCE-LEAKAGE	Separate threat model	implementation-leakage	P1	Preserve as a separate security track; no lattice foundation build for the primary objective now.
Invalid-curve, twist, fault, and side-channel routesR-PROTOCOL-FAULT-SIDECHANNEL	Separate threat model	implementation-leakage	P1	Record scope; do not expand the Lean substrate until a concrete implementation-verification goal exists.
Fault-tolerant quantum ECDLPR-QUANTUM-SHOR	Separate threat model	fault-tolerant-quantum	P1	Update the registry estimate and monitor primary literature; do not build a quantum Lean stack now.

Formal substrate

11 of 17 critical nodes are closed. Blocked nodes retain exact resume conditions.

Open canonical map

Critical node	Status	Depends on	Blocker	Evidence
Canonical counts, registries, generated views, and active queuetruth-layer	Closed	none	none	STATUS.md tasks/NEXT.md
secp256k1 field and subgroup parameterssecp-parameters	Closed	none	none	Ecdlp/Proved/Secp256k1PrimeP.lean Ecdlp/Proved/Secp256k1PrimeN.lean
Exact rational-point cardinality and full cyclic groupsecp-rational-group	Closed	secp-parameters	none	Ecdlp/Proved/CurveCardinalityExact.lean Ecdlp/Proved/CurveFullGroup.lean
Fixed-transcript generic-group collision coregeneric-security-core	Closed	secp-rational-group	none	Ecdlp/Proved/GenericGroupBound.lean notes/SECURITY_SCOPE.md
Abstract protocol algebra and concrete curve instantiationprotocol-soundness	Closed	secp-rational-group	none	Ecdlp/Proved/ProtocolInstantiation.lean
GLV automorphism on the full rational point groupglv-rational-scope	Closed	secp-rational-group	none	Ecdlp/Proved/GlvSubgroupEigenvalue.lean notes/SECURITY_SCOPE.md
Semaev S3/S4 formal foundationssemaev-foundations	Closed	secp-rational-group	none	Ecdlp/Proved/SemaevThree.lean Ecdlp/Proved/SemaevFour.lean
Division-polynomial, EDS, degree, and coprimality substratedivision-polynomial-foundations	Closed	secp-parameters	none	Ecdlp/Proved/DivisionPolynomialCoprime.lean Ecdlp/Proved/NormEDSConsecutiveZeros.lean
Closed E[n] structure for n in {2,3,5,7} and fixed multiplication rungs through 5small-torsion-family	Closed	division-polynomial-foundations	none	Ecdlp/Proved/TwoTorsionStructure.lean Ecdlp/Proved/SevenTorsionStructure.lean
Coprime and distinct torsion locitorsion-loci	Closed	division-polynomial-foundations	none	Ecdlp/Proved/TwoTorsionCount.lean
Weil divisor, Miller function, and reachable evaluation layerweil-w1-w3	Closed	small-torsion-family	none	Ecdlp/Proved/WeilMillerEval.lean notes/WEIL_LADDER.md
Uniform point-level multiplication coordinate formulan7-uniform	Blocked	division-polynomial-foundations, small-torsion-family	blocker-point-division-map, blocker-n7-certificates	Ecdlp/Targets/n7_uniform_carrier_induction.lean targets/n7_uniform_secp256k1_x.json
Uniform separability and geometric n-torsion countn10-uniform-separability	Blocked	division-polynomial-foundations	blocker-uniform-separability	notes/SEPARABILITY_ROUTES.md
General E[n] structure over the algebraic closuregeneral-n-torsion	Blocked	n7-uniform, n10-uniform-separability	blocker-point-division-map, blocker-uniform-separability	notes/DIVISION_POLY_TORSION_MAP.md
Weil reciprocity and the bilinear non-degenerate pairingweil-w4-w5	Blocked	weil-w1-w3, general-n-torsion	blocker-weil-reciprocity	notes/WEIL_LADDER.md BARRIERS.md
P-256 exact rational-point cardinalityp256-exact-cardinality	Outside release	secp-parameters	blocker-p256-cardinality	Ecdlp/Proved/P256Cardinality.lean
New cryptanalytic hypothesis testingexperimental-hypotheses	Parked	truth-layer	none	experiments/HYPOTHESES.yaml

Accepted blockers

Missing foundations are recorded, but do not authorize work without a selected route.

Blocker	What is missing	Resume condition
No uniform Point-to-division-polynomial multiplication mapupstream-foundation	Mathlib exposes the polynomial identities but not the theorem connecting [n]P to the phi/psi coordinate formulas for all n.	An upstream multiplication-coordinate theorem lands, or a reviewed in-repo induction closes the torsion bridge.
Four N7 algebra walls need large checked elimination certificatesproof-engineering	The statements are machine-elaborated and numerically/symbolically validated, but checked cofactors for the degree-heavy identities are not yet authored.	A reproducible certificate generator emits Lean-checkable cofactors for all four algebra walls.
Uniform separability of multiplication-by-n is not availablemissing-theory	Small n is closed, while the general prime-to-characteristic counting and differential argument remains absent.	A checked [n]*omega=n omega or equivalent general separability theorem is available.
Weil reciprocity and divisor-degree machinery are missingupstream-foundation	The reachable W1-W3 evaluation substrate is closed; W4 reciprocity is required before the pairing can be assembled.	Mathlib or this repository gains the needed divisor/tame-symbol reciprocity layer.
P-256 exact cardinality needs a general point-counting/Hasse routeout-of-scope-foundation	Only n divides the P-256 group cardinality is proved; the secp256k1 j=0 certificate does not transfer.	A reviewed Hasse/Schoof or curve-specific exact-cardinality proof becomes available.

secp256k1 research state

Current operating state

No experiment is currently authorized.

Why this decision

Route portfolio

Disposition distribution

Formal substrate

Accepted blockers

Sync Health

Canonical counts

Decision state

Generated closure

Product boundary

Reconsideration triggers

Operating policy

Work queue

TASK-008 · Maintain evidence-gated candidate intake

TASK-009 · Implement only a newly selected foundation

TASK-010 · Periodic independent adversarial audit

TASK-011 · Validate the external product pilot

TASK-012 · Build configurable intake after a pilot contract