Canonical decision explorer

secp256k1 ECDLP route map

Every route is generated from repo/ECDLP_DECISION_SUBSTRATE.json. Search by mechanism, scope, evidence, or next action.

Evaluated routes

17 routes

Generic-group lower boundR-GENERIC-LOWER-BOUND

Guardrail

P0 classical-generic

Applicability

direct within the generic-group model

Known cost

Omega(sqrt(n)) generic queries, under the exact formal model and success assumptions.

Current evidence

The collision-counting core and square-root consequence are Lean-verified.

Assumptions

Generic encodings reveal no exploitable representation structure.; Complexity is measured in oracle queries with bounded success probability.

Success gate

Any classical plain-input route must identify and justify the non-generic information that escapes this model.

Stop condition

Reject proposals that merely relabel generic operations or hide work in preprocessing.

Next action

Retain as a mandatory comparison and scope guard; no new experiment.

Evidence files

Ecdlp/Proved/GenericGroupBound.lean notes/SECURITY_SCOPE.md

Baby-step giant-step and Pollard rhoR-GENERIC-BASELINE

Baseline

P0 classical-single-target-plain, classical-generic

Applicability

direct

Known cost

Theta(sqrt(n)) group work; BSGS uses Theta(sqrt(n)) memory while rho can use negligible memory with parallel variants.

Current evidence

Core decomposition, step bound, and collision/periodicity statements are Lean-verified; implementation constants are not a secp256k1 break.

Assumptions

Ord(P) is known.; No special target structure is required.

Success gate

Every candidate route must beat the correct time-memory-precomputation baseline under the same input model.

Stop condition

Do not present hardware scaling or parallel rho as an asymptotic improvement.

Next action

Use as the benchmark comparator in the evaluation harness.

Evidence files

Ecdlp/Proved/BabyStepGiantStep.lean Ecdlp/Proved/PollardRho.lean

GLV endomorphism accelerationR-GLV

Constant factor

P0 classical-single-target-plain

Applicability

direct

Known cost

Known use is a constant-factor acceleration or search-space symmetry; no justified o(sqrt(n)) plain-input algorithm follows.

Current evidence

The rational point action, eigenvalue scope on multiples of G, and orbit facts are Lean-verified.

Assumptions

Use the secp256k1 order-3 endomorphism and its eigenvalue on the generator subgroup.

Success gate

Promotion requires a mechanism that changes relation-generation or search complexity, not only orbit size.

Stop condition

Close any proposal whose only gain is a finite orbit quotient or scalar decomposition.

Next action

Keep as target structure available to a selected route; do not treat it as a standalone attack.

Evidence files

Ecdlp/Proved/GlvTorsionAction.lean experiments/p0_glv_semaev/RESULTS.md

Pohlig-Hellman subgroup reductionR-POHLIG-HELLMAN

Ruled out for target

P0 classical-single-target-plain

Applicability

the algorithm applies, but secp256k1 has no smaller prime-order factors to exploit

Known cost

Dominated by the largest prime factor of ord(P); for secp256k1 that factor is n itself.

Current evidence

n is Lean-verified prime and the reduction/reconstruction algebra is formalized.

Assumptions

A useful factorization of ord(P) into smaller factors.

Success gate

A proposal must exhibit an actual nontrivial subgroup decomposition of the target instance.

Stop condition

Stop immediately for the standard generator subgroup because n is prime.

Next action

Retain as a machine-checked elimination certificate.

Evidence files

Ecdlp/Proved/Secp256k1PrimeN.lean Ecdlp/Proved/PohligHellman.lean

MOV, Frey-Ruck, and Tate/Weil pairing transferR-PAIRING-TRANSFER

Ruled out for target

P0 classical-single-target-plain

Applicability

no useful low-embedding-degree transfer is available for secp256k1

Known cost

Transfer is only useful when finite-field DLP in F_(p^k) is easier at the target's embedding degree k.

Current evidence

Lean proves the secp256k1 embedding degree is greater than 100, which is a strong practical exclusion of low-degree MOV-style transfers.

Assumptions

The n-torsion embeds into a finite-field multiplicative group of tractable extension degree.; The relevant pairing is non-degenerate on available points.

Success gate

A proposal must state the exact pairing, available torsion points, extension degree, and finite-field DLP cost.

Stop condition

Reject low-degree-transfer claims inconsistent with the verified embedding-degree bound.

Next action

Keep the target-specific exclusion; defer a full pairing library unless a new route needs it.

Evidence files

Ecdlp/Proved/EmbeddingDegree.lean BARRIERS.md

Smart, Satoh-Araki, and Semaev anomalous-curve liftingR-ANOMALOUS-PADIC

Ruled out for target

P0 classical-single-target-plain

Applicability

inapplicable because secp256k1 is not anomalous

Known cost

Polynomial-time for the anomalous special case; the prerequisite fails here.

Current evidence

Lean proves the anomalous iff trace-one scope and that secp256k1 is ordinary and non-anomalous.

Assumptions

#E(F_p) = p, equivalently trace one in the relevant setting.

Success gate

A p-adic proposal must identify a different valid degeneracy and prove it holds for secp256k1.

Stop condition

Stop Smart/SSSA instantiation when #E(F_p) != p.

Next action

Retain the formal exclusion; do not build an elliptic formal-group stack for this target now.

Evidence files

Ecdlp/Proved/AnomalousScope.lean

Weil descent and GHS-style transferR-WEIL-DESCENT

Ruled out for target

P1 classical-single-target-plain

Applicability

the standard extension-field descent mechanism has no nontrivial degree to exploit over the prime field F_p

Known cost

Useful only for selected extension-field settings; degree one gives no descent gain.

Current evidence

Target-field structure rules out the standard GHS setting; no dedicated Lean theorem is claimed.

Assumptions

The curve is defined over an extension field with exploitable descent geometry.

Success gate

A proposal must provide a concrete alternative descent object over F_p and a lower resulting DLP cost.

Stop condition

Reject arguments that silently replace the prime-field target with an extension-field family.

Next action

Document as a target-applicability exclusion; no formal stack now.

Evidence files

data/attack_registry.json notes/SECURITY_SCOPE.md

Prime-field index calculusR-PRIME-FIELD-INDEX-CALCULUS

Open, parked

P1 classical-single-target-plain

Applicability

conceptually direct, with no validated subgeneric secp256k1 algorithm in the audited evidence

Known cost

No accepted plain-prime-field asymptotic improvement is established here; known toy systems encounter relation-yield, degree, and memory barriers.

Current evidence

S3/S4 foundations and limited toy measurements exist, but they do not establish a degree-of-regularity law or subgeneric scaling. WCC 2017 adds bounded m=2 practicality evidence on selected small primes and explicitly makes no asymptotic claim.

Assumptions

Efficient factor-base relation generation over a large prime field.; A tractable polynomial-system solving regime.; Linear algebra and descent costs that preserve any relation-generation gain.

Success gate

Provide an exact relation system, independent EC validation, a justified solving-cost model, and multi-size evidence consistent with o(sqrt(n)).

Stop condition

Park when gains rely only on factor-base constants, unvalidated Macaulay proxies, tiny fields, or hidden exhaustive enumeration.

Next action

Preserve evidence and prerequisites; wait for explicit route selection before any new experiment.

Evidence files

Ecdlp/Proved/SemaevThree.lean Ecdlp/Proved/SemaevFour.lean experiments/p1_petit_m3/RESULTS.md

GLV-symmetrized Semaev systemsR-GLV-SEMAEV

Open, parked

P1 classical-single-target-plain

Applicability

direct to the j=0 target structure, but only constant-factor evidence exists

Known cost

Finite GLV orbit compression is constant-factor. The proposed u_i=x_i^3 map is the coordinatewise C3^m quotient, not the diagonal C3 quotient, and generically merges 3^(m-1) diagonal orbits.

Current evidence

GLV-SEMAEV-ITER-001 exactly enumerates all 27 S3 and 81 S4 coordinatewise C3 scalings in the universal and primitive cube-root quotients and after secp256k1 specialization. Only the diagonal C3 is a scalar polynomial covariance. Certificate 2142e8d66a8422768b609e42f5ce09377d5f93609941139fc9fc4e5abe4dfe59 gives every rejected S3/S4 pair a coefficient +1 witness over Z[b], making the polynomial classification uniform across characteristics whenever a primitive cube root exists. The fixed-target certificate is S4-specific: 9db5e0375421659f9abb905c12ae77232ef9957867f7194baaf548d45a1f091d proves that every nonzero affine S4 target has only identity coordinate-scaling covariance in characteristic outside {2,3}; the r=0 slice has exactly the diagonal C3 stabilizer. Standard-library validators independently reconstruct S4 from the Sylvester determinant and replay both classifications. Lean separately proves secp256k1_seven_not_isSquare, secp256k1_x_ne_zero, and the diagonal corollary secp256k1_glv_affine_target_moves, so no F_p-rational affine secp256k1 target inhabits r=0. Exhaustiveness is still certificate-backed, not a Lean theorem; source-author independence is not established. The original 14-theorem covariance and point-group transport module passed the full Lean build, built-source no-sorry scan, and exhaustive axiom audit in workflow run 30163027316 at content head be7a4d8e7da94b33ef74b0c146d732314b293827. The affine closeout extension requires its own build and axiom audit; earlier P0-P4 evidence is retained unchanged.

Assumptions

Invariant coordinates reduce relation-generation complexity or solving degree, not only factor-base storage.; The quotient retains enough information to recover valid relations.

Success gate

Supply a materially different exact mechanism with explicit fixed-target behavior, recovery, and a theoretical reason for a lower asymptotic solving exponent, then validate it independently. Repackaging coordinatewise cubes is not a new premise.

Stop condition

The coordinatewise quotient and dependent m=3 scaling draft are stopped. Any successor also stops if its gain is bounded by orbit size or disappears after complete relation-generation and recovery costs are counted.

Next action

Keep GLV-SEMAEV-ITER-001 closed without a solver run. Accept only a materially different phase-preserving mechanism with an exact recovery map, orbit tags, excluded components, a falsifiable full-cost prediction, and an independent validator through TASK-008 before any new decision.

Evidence files

Ecdlp/Proved/GlvSemaevSymmetry.lean experiments/glv_diagonal_obstruction/artifact.json experiments/glv_semaev_symmetry/certificate.json experiments/glv_semaev_symmetry/fixed_target_certificate.json experiments/p0_glv_semaev/RESULTS.md experiments/p1_petit/RESULTS.md experiments/p1_petit_m3/RESULTS.md experiments/p3_sm_system/RESULTS.md experiments/p4_petit/RESULTS.md notes/GLV_SEMAEV_ITERATION_001.md

Petit-style composed rational mapsR-PETIT-COMPOSED-MAPS

Open, parked

P2 classical-single-target-plain

Applicability

source-grounded but target applicability remains unresolved: PKC 2016 specifies a p-1-smooth construction and a separate auxiliary-curve construction whose own self-isogeny defines the root map; neither has a validated secp256k1 full-cost bridge

Known cost

No reliable project estimate; the existing six-variable toy presentation is explicitly non-faithful and descriptive.

Current evidence

The official PKC 2016 primary source has now been inspected. It defines the faithful prime-field factor base F={(x,y):L(x)=0}, with L a composition of low-degree rational maps, and gives p-1-smooth-subgroup and auxiliary-curve realizations. In the second construction the auxiliary curve only shares the base field with the target; a self-isogeny of the auxiliary curve defines the root map. The paper explicitly leaves the asymptotic complexity of the resulting generalized root-finding problem open. WCC 2017 adds bounded m=2 practicality evidence on selected small primes and a distinct p-plus-one trace extension; it cannot be transferred quantitatively to m=16 or substituted for the auxiliary curve. Historical P4 did not implement either PKC construction and remains only an inconclusive negative control; it is not evidence against the faithful route. For nonsingular y^2=x^3+7 in characteristic not in {2,3,7}, TASK-017 independently replayed an exact set-theoretic homogeneous projective S3-tree bridge, every named exceptional lift and identity stratum, deterministic supplied-coordinate recovery, and raw and compressed secp256k1 GLV lift-sign checks. TASK-018 freezes the recursive projective S17 contract, including fixed degrees and the literal Sylvester determinant under the frozen coefficient, argument, and row order. TASK-019 kernel-checks the fixed-degree projective resultant common-root theorem, coefficient-map and algebraic-closure reflection variants, the literal TASK-018 Sylvester matrix and determinant with coefficient unit 1, and its end-to-end common-root corollary. Formal-degree drops, zero forms, affine witnesses, and [1:0] are retained without primitive/content, monic, or actual-degree normalization. The TASK-019 non-run binding is PKC-SMOOTH-M16-PROJECTIVE-RESULTANT-KERNEL-001 with SHA-256 0b9d8b48953aae2defa28ade67992084cecca3a01b43490bc338a0fd5ce97c5a and typed claim SC-PKC-M16-PROJECTIVE-RESULTANT-KERNEL-RESULT. TASK-020 kernel-checks the actual recursive frozen C_r family, exact same-field and coefficient-map successor specialization at formal degrees (2^(r-2),2), coefficient unit 1, affine [y:1] and infinity [1:0] output branches, the uniform predecessor output-degree bound, and the unconditional one-step resultant/common-projective-root equivalence. Its non-run binding is PKC-SMOOTH-M16-FROZEN-CR-SPECIALIZATION-001 with SHA-256 d025053b9f882c88086fd5f04bcbd9627c72987e263e9b55af6024794305acbe and typed claim SC-PKC-M16-FROZEN-CR-SPECIALIZATION-RESULT. TASK-021 kernel-checks exact declared-degree projective evaluation and the universal all-stage frozen witness-chain equivalence. At C16 the chain has fourteen valid intermediate projective slots, [1:0] is allowed throughout, and [0:0] is excluded. Its non-run binding is PKC-SMOOTH-M16-FROZEN-PROJECTIVE-WITNESS-001 with SHA-256 89c645545d89334473d51654a41ff7ec2364857d034c64ce08d505337fa1e2d4 and typed claim SC-PKC-M16-FROZEN-PROJECTIVE-WITNESS-RESULT. TASK-022 now kernel-checks an exact literal finite MvPolynomial family for the frozen stage-14 predicate after an injective source-to-target field map: one GuardVar assignment satisfies every GuardedEquation. This is exactly equivalent to the recursive chain, not a parallel recursive syntax. Four raw scalars U,V,A,B for each of fourteen projective witness slots give 56 variables; fifteen literal H equations and fourteen guards give 29 equation-family members; every equation has total degree at most four; [0:0] is excluded and [1:0] is retained. Its non-run binding is PKC-SMOOTH-M16-GUARDED-PROJECTIVE-SYSTEM-001 with SHA-256 3445da55b44a71d0f40ee60206c90f2ef1798c28abd125542ce3acbeeb8e1d46 and typed claim SC-PKC-M16-GUARDED-PROJECTIVE-SYSTEM-RESULT. The source binding is 37feeef48e77437b44b6ae6dd4750782e19ecd824e3ea2e73b657e2fb8296fb9. TASK-023 now kernel-checks the exact affine/infinity chart-polynomial cover: each fixed InfinityMask I uses exactly 14 - I.card affine variables, no guard equations, and fifteen literal H equations with degree ceilings 2/4/2. The existential cover is equivalent to the projective chain, guarded system, and source frozen stage-14 predicate after the existing injective base change; [1:0] is retained and [0:0] is never introduced. The 2^14 logical masks are not enumerated or materialized. Its non-run binding is PKC-SMOOTH-M16-EXACT-CHART-COVER-001 with SHA-256 934809fabbb8c98c5ed9356a0a1f3367a23f8fbc1bc86239069942537fd678ed and typed claim SC-PKC-M16-EXACT-CHART-COVER-RESULT. The TASK-023 source binding is 4f7b95453d8fafba3ec9cae0a9bbad5d8f782c6c0202f6e7cf37e17981b63019. TASK-024 kernel-checks necessary infinity-stratum pruning from 16384 masks to 987 separated masks and conditionally to 377 interior masks. Its binding is PKC-SMOOTH-M16-INFINITY-STRATA-001 with SHA-256 54b0f3c5f2f1880b1f805911df21b72e5427b18871f14907ac17a1d8b48bdd39 and typed claim SC-PKC-M16-INFINITY-STRATA-RESULT. TASK-025 kernel-checks explicit infinity propagation: the nested conditional mask counts are 377 to 129 to 69 to 36, while the independent boundary-only refinement is 129 to 60. It also proves over any field that internal infinity forces an explicit frozen prefix or suffix obstruction to vanish and that endpoint plus BalancedPropagatedRegular assumptions make the exact chart cover the single empty-mask affine chart. Its binding is PKC-SMOOTH-M16-INFINITY-PROPAGATION-001 with SHA-256 9330603ba1f0af9ee4902c263200709e2ec6f8c50d8d7eaab3b55bcba78e388f and typed claim SC-PKC-M16-INFINITY-PROPAGATION-RESULT. The TASK-025 source binding is 7f868aab5b946a55a213ce26a461477321d6387830eed218c414f1e62853b4b4. Its source-stage bridge requires injective base change into an algebraically closed target and mapped-target balanced regularity; source-field computation does not automatically establish that regularity. Symbolic nonzeroness, nonemptiness, density, probability, genericity, and witness uniqueness are not proved. Assurance is kernel_bound_non_run_certificate, source independence is not_established, calibration is excluded_nonexperimental, and retention is zero_retention_success. The M16 cell remains open_non_executable. The exact remaining blocker is symbolic nonzeroness and nonemptiness of a usable regular locus or orchestration of its exceptional complement, followed by relation yield, rank, solving, recovery, and total cost. CQ-SEMAEV-S17-SYSTEM-COST remains partial while relation yield, rank, and solving cost remain unpriced.

Assumptions

A correctly specified low-degree rational map yields a useful factor-base or relation system.; Composition, solving, and recovery costs improve the full attack.

Success gate

First reproduce the exact construction from a verified primary source, then compare it under the common evaluation contract.

Stop condition

Reject low-bit filters, redundant auxiliary variables, or presentation-only degree changes as substitutes for the cited construction.

Next action

Keep the route parked. TASK-023 through TASK-025 completed the exact chart cover, necessary infinity-stratum filters, and conditional single-affine-chart propagation. TASK-026 then consumed its one external synthetic-toy authorization: all 3000000 trials completed, 911 exact relations were accepted, 907 were affine regular, and all six curve-arm regularity gates passed. REO-2026-07-31-001 records the result. This supports the bounded enabling claim that the named regular locus is usable in the frozen toy construction. Matched orbit/plain controls retained no H_NEW qualifying size, so the GLV-specific explanation is bounded negative and the terminal is CLASSIFY_AS_KNOWN_LOCAL_SIMPLIFICATION. The result is not source-faithful PKC relation generation, rank, solver scaling, recovery, total cost, 256-bit persistence, or an ECDLP improvement. Only formulate and review a source-faithful, non-executable HYP-M16-SOLVER-SLOPE-001 proposal with end-to-end metrics and scaling death criteria. Keep every TASK-026 rerun, production mask sweep, solver, experiment, route rejection, route promotion, cost claim, and exact-target inference closed until a separate dated authorization. Keep the auxiliary-curve cell parked until a primary source supplies a finite family or search domain with a completeness criterion.

Evidence files

Elliptic divisibility sequences and division-polynomial re-encodingsR-EDS-DIVISION-POLYNOMIAL

Open, parked

P2 classical-single-target-plain

Applicability

structurally direct, with no known independent information source or subgeneric inversion method

Known cost

Known recurrences evaluate W_m for a supplied m; they do not cheaply find the unknown first zero or discrete logarithm.

Current evidence

Lean formalizes substantial division-polynomial and normEDS structure. Toy measurements confirm apparition/torsion equivalence and no advantage.

Assumptions

A sequence or polynomial observable can be inverted more cheaply than scalar multiplication or exhaustive apparition search.

Success gate

Identify an observable computable from (P,Q) whose inversion provably avoids equivalent ECDLP work.

Stop condition

Stop when the construction only re-encodes scalar multiplication or requires Theta(ord(P)) search.

Next action

Keep HYP_WARD_EDS_001 parked; finish no additional point-division bridge unless a selected route needs it.

Evidence files

Ecdlp/Proved/NormEDSSomos4.lean experiments/p2_ward_eds/RESULTS.md

Isogeny, endomorphism-ring, and Frobenius transferR-ISOGENY-ENDOMORPHISM-TRANSFER

Monitor

P3 classical-single-target-plain

Applicability

no concrete efficiently computable transfer to a weaker target is identified

Known cost

Unspecified without a concrete target and map; special endomorphisms currently support constant-factor GLV acceleration.

Current evidence

The repository has target endomorphism facts but no general isogeny stack or candidate weak codomain.

Assumptions

An efficiently computable map reaches a curve or representation where DLP is materially easier.; Kernel and degree do not erase the gain.

Success gate

Provide an explicit map, target, DLP advantage, and end-to-end cost.

Stop condition

Do not formalize a general stack in advance of a concrete route.

Next action

Monitor literature and reuse GLV facts; no build now.

Evidence files

Ecdlp/Proved/GlvTorsionAction.lean BARRIERS.md

Multi-target and reusable-precomputation tradeoffsR-MULTI-TARGET-PRECOMPUTATION

Conditional inputs

P1 classical-conditioned

Applicability

not applicable to the primary one-target/no-precomputation objective unless costs are explicitly amortized

Known cost

Can change amortized constants and time-memory tradeoffs; it does not by itself solve an arbitrary single target below the proper total-cost baseline.

Current evidence

Covered in the attack registry as a separate conditioned model.

Assumptions

Many targets share a group or base point.; Precomputation storage and setup are available and counted separately.

Success gate

State target count, online/offline split, memory, reuse horizon, and total amortized cost.

Stop condition

Reject comparisons that omit precomputation or compare an amortized online phase to a full single-target baseline.

Next action

Represent in the evaluation contract; no experiment in this phase.

Evidence files

data/attack_registry.json notes/SECURITY_SCOPE.md

Interval DLP, partial-key knowledge, and auxiliary-power algorithmsR-INTERVAL-AUXILIARY-INPUT

Conditional inputs

P2 classical-conditioned

Applicability

not applicable to an arbitrary full-range scalar without the promised interval or auxiliary data

Known cost

May reduce work relative to the conditioned search space; it does not alter the unconditioned n-sized instance.

Current evidence

The current target contract supplies neither an interval promise nor auxiliary powers.

Assumptions

k lies in a known small interval, or the attacker receives additional algebraic powers or relations involving k.

Success gate

Declare exactly how the auxiliary information is obtained and include its acquisition cost.

Stop condition

Reject any route that assumes the secret information it is meant to recover.

Next action

Keep as a scope category for future protocol or leakage analyses.

Evidence files

notes/SECURITY_SCOPE.md

Hidden-number and lattice attacks on biased or reused ECDSA noncesR-HNP-NONCE-LEAKAGE

Separate threat model

P1 implementation-leakage

Applicability

important for key security but not a plain ECDLP algorithm

Known cost

Depends on leakage quality, sample count, and lattice dimension; a valid instance can recover a signing key without solving arbitrary ECDLP.

Current evidence

The repository catalogs the attack family but lacks an LLL/BKZ and HNP formal stack.

Assumptions

Signatures leak nonce bits, reuse nonces, or have a statistically exploitable bias.

Success gate

Keep leakage acquisition, statistical model, lattice reduction, and key verification explicit.

Stop condition

Do not classify nonce failures as a mathematical break of secp256k1 ECDLP.

Next action

Preserve as a separate security track; no lattice foundation build for the primary objective now.

Evidence files

data/attack_registry.json notes/SECURITY_SCOPE.md

Invalid-curve, twist, fault, and side-channel routesR-PROTOCOL-FAULT-SIDECHANNEL

Separate threat model

P1 implementation-leakage

Applicability

relevant only when an implementation exposes attacker-controlled inputs or physical leakage

Known cost

Implementation-dependent and often far below generic DLP when the vulnerability exists.

Current evidence

Protocol algebra is formalized at an abstract level; implementation leakage is outside that proof model.

Assumptions

Missing point validation, unsafe scalar multiplication, fault injection, timing, power, cache, or electromagnetic leakage.

Success gate

Specify the concrete implementation, leakage channel, validation behavior, and key-recovery verification.

Stop condition

Keep mathematical protocol soundness separate from implementation hardening claims.

Next action

Record scope; do not expand the Lean substrate until a concrete implementation-verification goal exists.

Evidence files

notes/SECURITY_SCOPE.md ABSTRACT_SCOPE.md

Fault-tolerant quantum ECDLPR-QUANTUM-SHOR

Separate threat model

P1 fault-tolerant-quantum

Applicability

algorithmically direct given sufficiently capable fault-tolerant quantum hardware

Known cost

Polynomial-time quantum algorithm. The 2026 audited preprint reports 835 logical qubits and 2^30.63 Toffoli gates for secp256k1; physical resources and availability are not established by that estimate.

Current evidence

Shor gives the algorithmic route; Luo et al. provide the current project-tracked logical-resource estimate.

Assumptions

Large-scale error-corrected quantum computation.; A reversible elliptic-curve implementation with the quoted logical resources.; Physical error correction overhead is separately accounted for.

Success gate

Distinguish algorithm, logical circuit, error-correction overhead, physical hardware, runtime, and availability.

Stop condition

Do not turn a logical-resource estimate into a claim that present hardware can break secp256k1.

Next action

Update the registry estimate and monitor primary literature; do not build a quantum Lean stack now.

Evidence files

data/attack_registry.json notes/SECURITY_SCOPE.md