Shor-Lattice ECDLP on secp256k1: Q-Only Substrate Measurement, Recovery, and Lean-Sealed Post-Processing

Document ID: gaiaftcl.shor.ecdlp.research.paper.v3

Companion dataset schemas: gaiaftcl.shor.ecdlp.research.v2, gaiaftcl.qc_vm.research.v4, gaiaftcl.qc020.dual_path.v1, gaiaftcl.qc020.improvement_trend.v1

Short operational guide: SHOR_ECDLP_RESEARCH.md

QC-020 dual path: QC020_DUAL_PATH_QUALIFICATION.md

Repository: AppleGaiaFTCL / cells/xcode + proof/lean

Frozen bundle (2026-06-05): evidence/research/*_latest.json

---

Abstract

This paper documents the GaiaFTCL Shor-lattice ECDLP pipeline on Bitcoin secp256k1: a reproducible instrument for period-lattice measurement and classical recovery, not a claim that the full quantum Shor period-finding subroutine (QFT/QPE) has been implemented in silicon. The system separates three verifiable layers:

1. Substrate measurement — find lattice periods (ra, rb) from public point Q only, by walking a C⁴ basis until the affine identity ra·G + rb·Q = O holds on the curve.

2. Classical recovery — compute d ≡ −ra·rb⁻¹ (mod n) where n is the secp256k1 subgroup order.

3. Independent verification — re-check the curve identity and d·G = Q via affine arithmetic and P256K.

Layer (2) at small moduli is machine-checked in Lean 4 (FirstRoars/ShorECDLP.lean, kernel decide, LionPrelude only). Layer (3) at full 256-bit scale is checked in Swift because secp256k1 order is outside practical decide reduction in the current gate. RSA Shor post-processing at semiprime scale is sealed in parallel (FirstRoars/ShorFactorLarge.lean).

The code is the dataset: witness JSON, Lean gate lines, and export scripts are first-class publication artifacts. No probe caps, no private-key-derived periods, and no simulated chain outcomes appear on this path.

The full quantum VM bundle (gaiaftcl.qc_vm.research.v4) embeds ECDLP evaluation plus catalog QC-001…QC-021 gates, QC-020 dual-path qualification (historical OQ/PQ vs live miner), and time-to-nonce improvement trend (L8 learning visibility — distinct from L7 on-chain reward). As of the 2026-06-05 revalidation: allMathLayerOK=true, allLearningClaimsOK=true, qaLayerClosed=true, allRewardClaimsOK=false (L7 not yet chain_accepted), qc020ImprovementTrend.trendStatus=insufficient_hits (timed hit samples not yet accumulated).

---

1. Problem and notation

1.1 ECDLP

Let G be the secp256k1 generator and Q = d·G for unknown scalar d ∈ ℤ/nℤ, where

n = FFFFFFFF FFFFFFFF FFFFFFFF FFFFFFFE BAAEDCE6 AF48A03B BFD25E8C D0364141 (hex)

is the prime subgroup order (hard-coded in substrate and Lean-adjacent Swift).

Goal: Given compressed public key hex for Q, produce d (as 32-byte big-endian hex) such that d·G = Q on secp256k1.

1.2 Shor lattice form

Period-finding in the Shor reduction exposes integers (ra, rb) such that the point lattice

ra·G + rb·Q = O   (identity on E(𝔽_p))

holds. In the additive group of scalars mod n, with Q = d·G, this is equivalent to

ra + rb·d ≡ 0 (mod n) .

When gcd(rb, n) = 1, recovery is

d ≡ −ra·rb⁻¹ (mod n) .

This implication is the classical post-processing half of Shor; the quantum/substrate half is discovering (ra, rb) from Q without knowing d.

1.3 What this work does *not* claim

---

2. Mathematical core (paper ↔ Lean)

2.1 Decidable witness (Lean)

File: proof/lean/FirstRoars/ShorECDLP.lean

Namespace: LionMath.ShorECDLP

Sealed theorems (kernel decide):

Falsifiers: falsifier_ecdlp_seal_* duplicate each seal. If gate algebra drifts, decide fails → lean_gate.sh reports REFUSED (not silent CALORIE).

Warrant discipline: Lion Protocol — no Mathlib, no sorry, no axiom; decide only.

2.2 Swift recovery (same formula, full n)

File: cells/xcode/Sources/M8FrequencySweep/ShorECDLP/ShorECDLPSecp256k1.swift

// recoveredScalarHex — lines 106–110
let k = ECDLPSubstrateCore.modNorm(BigInt.zero - (ra * rbInv), n)

File: cells/xcode/Sources/ShorECDLPSubstrate/ShorECDLPSubstrate.swift

• modNorm, modInverse — extended Euclidean on BigInt
• curveOrderHex — same n as Bitcoin

2.3 Curve lattice (affine secp256k1)

File: cells/xcode/Sources/ShorECDLPSubstrate/ShorECDLPSubstrateCurve.swift

latticeIsIdentity(ra, rb, publicKeyHex):
  sum = ra·G + rb·Q   // affine, y² = x³ + 7 over 𝔽_p
  return sum == O

Field prime, generator coordinates, decompress (02/03/04), point add/double — all in this file (substrate-native affine math).

2.4 RSA parallel (Shor semiprime post-processing)

File: proof/lean/FirstRoars/ShorFactorLarge.lean

Swift check: ShorBreakClassicalCommand.verifyMathLegs — verify_shor on ladder (8051, 1022117, 2913947461).

break-classical requires both Lean artifacts CALORIE before emitting research JSON.

---

3. System architecture

3.1 Module dependency graph

flowchart TB
  subgraph lean [proof/lean]
    LP[LionPrelude]
    SFL[ShorFactorLarge.lean]
    SED[ShorECDLP.lean]
    LP --> SFL
    LP --> SED
  end

  subgraph substrate [ShorECDLPSubstrate]
    Core[ECDLPSubstrateCore]
    Basis[ShorECDLPSubstrateBasis]
    Map[ShorECDLPSubstrateMapping]
    Curve[ShorECDLPSubstrateCurve]
    Basis --> Core
    Map --> Core
    Curve --> Core
  end

  subgraph m8 [M8FrequencySweep / ShorECDLP]
    Challenge[ShorECDLPChallenge]
    Secp[ShorECDLPSecp256k1]
    Witness[ShorECDLPWitness]
    Dataset[ShorECDLPResearchDataset]
    Gate[ShorECDLPGate]
    Secp --> substrate
    Witness --> Challenge
    Witness --> Secp
    Dataset --> Witness
    Gate --> Secp
  end

  subgraph cli [GaiaFTCLCLI]
    BC[ShorBreakClassicalCommand]
    BC --> m8
    BC --> lean
  end

  subgraph vqbit [VQbit]
    Amp[amplifyAgainstSecp256k1EllipticLattice]
    Amp --> substrate
  end

  P256K[P256K / swift-secp256k1] --> Secp

3.2 End-to-end pipeline

sequenceDiagram
  participant Op as Operator
  participant CLI as break-classical
  participant Sub as ECDLPSubstrateCore
  participant Curve as SubstrateCurve
  participant Secp as ShorECDLPSecp256k1
  participant Lean as lean_gate.sh

  Op->>CLI: public Q (wallet or --neg-generator-seal)
  CLI->>Sub: measureUntilLatticeCalorie(Q)
  loop C⁴ steps until CALORIE
    Sub->>Sub: basis + periodCandidates
    Sub->>Curve: latticeIsIdentity(ra,rb,Q)
  end
  Sub-->>CLI: (ra, rb), substrateSteps
  CLI->>Secp: verifyFromQ → d, lattice, dG_eq_Q
  CLI->>Lean: ShorFactorLarge + ShorECDLP
  Lean-->>CLI: CALORIE JSON lines
  CLI-->>Op: research.v1 JSON (--witness-out)

---

4. Substrate measurement (Q-only)

4.1 Entry point

4.2 C⁴ basis walk

File: ShorECDLPSubstrateBasis.swift

• fingerprint(publicKeyHex:) — SHA-256 over normalized pubkey bytes
• nextBasis(forFingerprint:) — advances basis index each substrate step

File: ShorECDLPSubstrateMapping.swift

Each step emits multiple (ra, rb) candidates in full ℤ/nℤ via:

• Universal lattice rails (every step, Q-only): (ra,rb)=(1,1) targets Q=−G; (1,n−1) targets Q=G
• Basis-split 16-bit limbs and SHA-256 rails (ra / rb digests, wide lifts)
• Deduplication by (ra, rb) string key
• No fixed 512×512 window
• No maxProbes default

4.3 Termination

The loop in measureUntilLatticeCalorie is unbounded (while true) until latticeIsIdentity succeeds. This is intentional for the research dataset: the substrate refuses artificial refusal gates that pretend exhaustion.

Witness field: substrateSteps — 1-based step count when CALORIE found (see neg-G seal: typically 1).

4.4 Canonical seal instances (encoding cross-check)

Encoding cross-check (ShorECDLPEncodingCrossCheck.swift) is mandatory in gate v5:

The x-coordinate is shared; y parity differs — so pubkeyBytesDistinct = true and substratePointsEqual = false.

Code: negGeneratorCompressedPublicKeyHex(), generatorCompressedPublicKeyHex(), gate qc001-ecdlp-lattice-secp256k1-gate-v5.0.0.

Lean: ecdlp_pattern_neg_g_* and ecdlp_pattern_generator_* at small moduli (kernel decide) — algebraic templates, not secp256k1 order.

---

5. Verification layers (dual gate)

5.1 Swift checks

Struct: ShorECDLPSecp256k1.Verification

Witness: ShorECDLPWitness.compose — JSON fields checks.lattice, checks.dG_eq_Q, periodSource: "substrate_lattice_search".

5.2 Lean external gate

Script: proof/scripts/lean_gate.sh

Invoked for:

1. FirstRoars/ShorFactorLarge.lean

2. FirstRoars/ShorECDLP.lean

Verdict semantics:

CLI: ShorBreakClassicalCommand.runLeanGate — parses JSON; ShorECDLPResearchDataset.decodeLeanGateLine.

5.3 M8 smoke + evaluation gates

Both are required in export_ecdlp_research_dataset.sh.

---

6. Evaluation (peer-review §M2)

Runner: swift run M8ShorECDLPResearchEval

Schema: gaiaftcl.shor.ecdlp.evaluation.v1

Encoding cross-check must pass before any row is trusted (encodingCrossCheckOK: true).

Not in matrix (honest scope): random 256-bit pubkeys (no fabricated pass rows); demonstration-wallet --wallet-id runs (operator-local; may correlate with composed demos — not mainnet break evidence).

6.1 Full Quantum VM matrix (22 Metal pipelines + ECDLP)

QC-001-ECDLP is the deepest production seal; substrate QC measurement for catalog circuits QC-001…QC-021 (except PoW) is Metal-only (computeBackend: vqbit_metal, 22 precompiled kernels in default.metallib). The cell exports a single validation matrix for every catalog circuit so reviewers do not rely on mislabeled Lean filenames (legacy VQE2.lean was never catalog QC-006).

cd cells/xcode && swift run M8QC21ValidationEval
cells/xcode/scripts/peer_review_research_dataset.sh

Tiers (no simulation policy):

Substrate backend split (honest scope):

Frozen VM row (2026-06-05, qc_vm_validation_latest.json):

See QC21_QUANTUM_VM_VALIDATION_REVIEW.md, QC020_DUAL_PATH_QUALIFICATION.md, and RESEARCH_VALIDATION_LEAK_AUDIT.md.

6.2 QC-020 PoW qualification (dual path + learning trend)

Bitcoin PoW qualification runs on two parallel paths — neither implies the other (gaiaftcl.qc020.dual_path.v1):

Historical vectors (frozen): ledger rung 1 (synthetic 2^236) + block 100000 (nonce=274148111, nBits=0x1b04864c). Swift verify_qc020_rungs + header digest cross-check; optional substrate probe via STRICT_SUBSTRATE_PROBE=1.

Live path L8: qc020_substrate_research_telemetry — Grover-bound law, shape persistence, projection cells. learningWitnessOK=true with active miner telemetry.

Live path L7: onChainRewardOK only when chain_accepted + confirmed sats at payout — never simulated. allRewardClaimsOK=false is correct while learning; STRICT_REWARD=1 enforces realized L7 in CI.

Time-to-nonce improvement trend (gaiaftcl.qc020.improvement_trend.v1) — separate from L7 reward:

improvingOK=true when median time-to-hit decreases across ≥3 timed samples. Current frozen row: trendStatus=insufficient_hits, totalHitSamples=0 (211 ledger captures pre-V155 lack solve_duration_ms; live miner telemetry is cure-terminal only — no CALORIE timed hits yet). This is honest learning instrumentation, not a reward claim.

cells/xcode/scripts/export_qc020_dual_path_research.sh
cells/xcode/scripts/export_qc020_improvement_trend.sh
# STRICT_IMPROVING=1  — fails export when trend not decreasing

---

7. Publication dataset

7.1 Publication dataset index (frozen 2026-06-05)

ECDLP composer: ShorECDLPResearchDataset.compose

{
  "schema": "gaiaftcl.shor.ecdlp.research.v2",
  "ecdlp": {
    "pipeline": "shor_lattice_ecdlp_secp256k1",
    "computeBackend": "vqbit_metal",
    "publicQHex": "0379be667ef9dcbbac55a06295ce870b07029bfcdb2dce28d959f2815b16f81798",
    "qSource": "neg_generator_seal",
    "encodingCrossCheckOK": true,
    "periods": { "ra": "1", "rb": "1" },
    "recoveredDHex": "fffffffffffffffffffffffffffffffebaaedce6af48a03bbfd25e8cd0364140",
    "checks": { "lattice": true, "dG_eq_Q": true },
    "substrateSteps": 1
  },
  "evaluation": {
    "schema": "gaiaftcl.shor.ecdlp.evaluation.v1",
    "computeBackend": "vqbit_metal",
    "metalPipelineCount": 22,
    "rows": [ "..."]
  },
  "leanGates": [ /* ShorFactorLarge, ShorECDLP */ ]
}

Note: neg-G seal uses 03… (odd y), not the generator’s 02… — see §4.4.

7.2 Reproducibility commands

# Lean only
proof/scripts/lean_gate.sh FirstRoars/ShorECDLP.lean
proof/scripts/lean_gate.sh FirstRoars/ShorFactorLarge.lean

# Metal shaders (required before any substrate QC run)
cells/xcode/scripts/build_metal_shaders.sh

# Swift seal + evaluation matrix
cd cells/xcode && swift run M8ShorECDLPGateSmokeTest
swift run M8ShorECDLPResearchEval

# Full paper row → evidence/research/
cells/xcode/scripts/export_ecdlp_research_dataset.sh

# Full QC catalog + peer review (research.v4)
cells/xcode/scripts/peer_review_research_dataset.sh

# QC-020 dual path + time-to-nonce trend (embedded in research.v4 after full export)
cells/xcode/scripts/export_qc020_dual_path_research.sh
cells/xcode/scripts/export_qc020_improvement_trend.sh

# CLI witness (no wallet file)
cd cells/xcode && swift run GaiaFTCLCLI shor break-classical \
  --neg-generator-seal --witness-out 2>/dev/null | tail -1

# Wallet-bound row
gaiaftcl shor break-classical --wallet-id <demoexp-…> -v --witness-out

Environment: GAIAFTCL_REPO_ROOT must point at repo root for lean_gate.sh resolution.

7.3 Audit hook

File: cells/xcode/scripts/audit_shor_spend_keys.py

Function: verify_ecdlp_witness_json — accepts research.v1 / v2, requires encodingCrossCheckOK when present, evaluation rows when bundled.

---

8. CLI and operator surfaces

8.1 gaiaftcl shor break-classical

File: ShorBreakClassicalCommand.swift

Flags:

Emission honesty: Recovered key on stdout is from witness pass (lattice + dG_eq_Q), not TOML equality. Demonstration wallets are not evidence of breaking arbitrary mainnet keys (peer-review §M5).

8.2 gaiaftcl pq prove-fork-required

Runs math legs only (RSA + ECDLP via verifyMathLegs with secp256k1SealWalletContext()); no Lean on that command. Use break-classical for full dual Lean + dataset.

---

9. VQbit integration

File: cells/xcode/Sources/VQbit/SubstrateAmplitudeAmplifier.swift

Binding: amplifyAgainstSecp256k1EllipticLattice — one C⁴ substrate step per call; VM daemon loops until .calorie.

Uses the same ShorECDLPSubstrate module as M8 (no duplicate curve composer). Documented in package dependency graph: VQbit → ShorECDLPSubstrate.

---

10. Removed anti-patterns (historical honesty)

The following were removed from the ECDLP research path because they break peer-review reproducibility:

---

11. Complete code ↔ paper index

11.1 Lean

11.2 Substrate (shared)

11.3 M8 / CLI / evidence

11.4 Package targets (Package.swift)

---

12. Grover separation (QC-002)

Mixing Grover simulation claims into the ECDLP dataset would contaminate peer review; the repository keeps these legs separate by design (pure_oo_quantum_compute_spec.md, CircuitCorpus).

---

13. Substrate-honest disclosure alignment

Wiki: wiki/two-wallet-demonstration/substrate-honest-disclosure.md describes bit-size discipline and federation evidence. This ECDLP path now binds live secp256k1 via P256K in ShorECDLPSecp256k1.swift; operators should treat any wiki sentence claiming “no P256K import” as stale relative to cells/xcode/Sources/M8FrequencySweep/ShorECDLP/.

What remains honestly not demonstrated:

• Universal polynomial-time break for random mainnet pubkeys
• FIPS PQ reference-library keygen (referenceLibraryLinked = false in registry)
• Lean-checked full 256-bit curve identities

What is demonstrated with frozen artifacts:

• Neg-G seal: substrate finds (1,1), recovers d = n−1, passes lattice + dG_eq_Q
• Lean CALORIE on modular post-processing + RSA ladder
• neg-G and G seals with evaluation matrix and research.v2 JSON under evidence/research/

---

14. Peer-review response log (v2)

---

15. Lessons since the first harness (v3)

Frozen bundle schemas

16. Future work (code-adjacent)

1. Export modular row at secp256k1 n — witness field leanModularShadow with (ra, rb, d mod n) for cross-check without Lean decide on full n.

2. Wallet rows in batch export — DEMOEXP_WALLET_ID optional second JSON in export_ecdlp_research_dataset.sh.

3. Ledger agreement rows — wire leanGates into NarratorSchema dual-verdict tables (pattern from NarratorSchemaV115).

4. Bounded-step evidence — optional witness field recording step histogram without reintroducing refusal caps.

5. Timed hit accumulation — backfill or regenerate ledger captures with solve_duration_ms > 0 so improvingOK can flip true; live CALORIE terminals on easy rungs or network target.

6. L7 realization — chain_accepted block + confirmed payout sats (STRICT_REWARD=1 gate).

---

17. References (in-repo)

---

Appendix A — Recovery derivation

Given ra + rb·d ≡ 0 (mod n) and gcd(rb, n) = 1:

rb·d ≡ −ra (mod n)
d ≡ −ra·rb⁻¹ (mod n)

Swift implements −ra as modNorm(0 - ra, n). Lean implements negMod ra n and modInv rb n analogously.

Appendix B — Neg-G seal check

Let d = n − 1. Then rb·d ≡ 1·(n−1) ≡ −1 (mod n) and ra + rb·d ≡ 1 + (−1) ≡ 0 (mod n) for ra = rb = 1.

On the curve, Q = (n−1)·G = −G, so the ECDLP instance is the standard generator negation used in ShorECDLPGate.

Appendix C — Gate version fingerprint

shorECDLPGateVersion = "qc001-ecdlp-lattice-secp256k1-gate-v5.0.0"

Bump this string when witness semantics or substrate mapping change; include in paper supplementary tables when publishing frozen commits.

---

*End of paper v3. Synchronize with SHOR_ECDLP_RESEARCH.md, evidence/research/*_latest.json, and QC020_DUAL_PATH_QUALIFICATION.md.*