Staged research package for Fibonacci-anyon topological quantum computing, SHA-520 boundary analysis, and proof-directed search.
This is a mathematical formalization and simulation framework. Not a physical implementation. Not a claim that SHA is broken.
A formal model of topological quantum computing using the Fibonacci anyon category (SU(2)_3 Chern-Simons theory), connected to a Q-Lambda reversible oracle compiler and resource estimation backend.
The central question: does a Fibonacci-anyon topological quantum computer provide practical advantage for SHA-style cryptanalysis?
Current answer: No. Generic SHA preimage search has no advantage beyond Grover-style square-root speedup. Reversible oracle costs, braid compilation overhead, coherence requirements, and error-correction costs dominate long before full-round attack relevance. The negative result is the contribution.
| File | What it proves |
|---|---|
FibonacciAnyon.lean |
Fusion rules (tau x tau = 1 + tau), Fibonacci dimension counts, fusion theorem |
LogicalQubits.lean |
Encoding definitions (3-tau, 4-tau), physical anyon accounting theorems |
BraidCompilation.lean |
BraidOp structure, H/X/S/CNOT/CCX braid words, length theorems |
QuantumGates.lean |
QIR gate enum, braid cost function, cost theorems |
Main.lean |
Integration |
All theorems compile. The braid universality (density) theorem is cited to Freedman-Larsen-Wang (2002) -- not proved in this repo.
| Module | What it does |
|---|---|
qlambda/compiler.py |
Full Q-Lambda lexer, parser, QIR synthesizer, uncompute pass |
qlambda/arrays.py |
SHA-520 IV/K constants, falsification arrays, DSL primitives |
qlambda/programs.py |
SHA-520-r Q-Lambda source programs |
topological/braid_backend.py |
QIR-to-Fibonacci-braid gate compiler |
topological/resource_estimates.py |
Anyon and braid resource estimates |
quantum/quantum_sha520.py |
Reversible SHA-520 oracle construction |
quantum/grover_sha520.py |
Grover search implementation |
classical/sha520_ref.py |
SHA-520 reference (reduced-round) |
Four validation phases in experiments/:
- Classical validation -- SHA-520-r test vectors
- Quantum simulation -- reduced-round Grover (Qiskit Aer, optional)
- Resource validation -- estimated vs actual braid/anyon counts
- Topological compilation -- braid sequence generation (theory only)
Fibonacci anyon fusion:
tau x tau = 1 + tau
1 x tau = tau
1 x 1 = 1
Quantum dimension of tau: phi = (1+sqrt(5))/2
Braid costs (QuantumGates.lean):
- H: 5 braid ops
- T: 300 braid ops (Solovay-Kitaev approximation)
- CNOT: 5 braid ops
- CCX (Toffoli): 16 braid ops
Cryptanalytic result: Grover search on SHA-520 requires 2^260 oracle calls. Topological compilation adds overhead, no asymptotic advantage. Full-round attack is physically impractical.
| Claim | Status |
|---|---|
| Fibonacci anyons physically exist | UNPROVEN |
| Topological quantum computer can be built | UNPROVEN |
| This breaks SHA-520 | FALSE |
| All Lean proofs are closed | NO -- universality cites external proof |
| This beats surface codes | UNPROVEN |
Algorithm falsified if braid compilation overhead is superpolynomial in log(1/epsilon) or oracle cost dominates.
Architecture falsified if nu=12/5 FQH state not realized or interferometric visibility < 90%.
Status: all criteria open.
pip install -e .
python experiments/phase1_classical_validation.py
python experiments/phase2_quantum_simulation.py
python experiments/phase3_resource_validation.py
python experiments/phase4_topological_compilation.py
cd lean && lake buildtopological-quantum-computer/
├── lean/ # Lean 4 formal surfaces
│ ├── FibonacciAnyon.lean
│ ├── LogicalQubits.lean
│ ├── BraidCompilation.lean
│ ├── QuantumGates.lean
│ └── Main.lean
├── python/
│ ├── qlambda/ # Q-Lambda DSL + arrays + policy
│ ├── topological/ # QIR-to-braid backend
│ ├── classical/ # SHA-520 reference
│ ├── quantum/ # Reversible oracle + Grover
│ └── simulators/ # MPS + Qiskit
├── experiments/ # Four validation phases
├── docs/ # Architecture, falsification, threat model
├── ABOUT.md
├── CODEX_AUDIT.md
└── LICENSE.tri
- Kitaev, A. (2003). Fault-tolerant quantum computation by anyons. Annals of Physics.
- Freedman, M. H.; Larsen, M. J.; Wang, Z. (2002). The two-eigenvalue problem and density of Jones representation of braid groups. Communications in Mathematical Physics.
- Preskill, J. (2004). Lecture Notes on Topological Quantum Computation. Chapter 9.
Ahmad Ali Parr -- design, architecture, mathematical foundation
Tri-license: BSL-1.1 / AGPL-3.0 / MPL-2.0. See LICENSE.tri.
No license path authorizes claims of physical hardware, full theorem closure, full-round SHA cryptanalysis, or key recovery.
Falsifiable by design. Honest by construction.