Axiom Status — formalization/
Date: 2026-03-23
Build Status: ✅ SUCCESS
Total Axioms: 19
Sorry count: 0
Summary
| Category | Count | Description |
|---|---|---|
| PRIMITIVE | 3 | Core LRT commitments — irreducible by design |
| EXTERNAL | 16 | Established mathematics — imported with citation |
| REMAINING | 0 | ✅ No remaining derivation targets |
PRIMITIVE (3) — The Ontological Foundation
These define LRT. They cannot be derived — they are the theory’s irreducible commitments.
| File | Axiom | Role |
|---|---|---|
| Step0_Primitives.lean | I : Type* |
Infinite Information Space I∞ |
| Step0_Primitives.lean | I_infinite : Infinite I |
I∞ is infinite |
| Step1_Constitution.lean | bridge_principle |
X constitutes A_Ω |
EXTERNAL (16) — Established Mathematics
Peer-reviewed results imported rather than re-proven. Standard methodology for reconstruction programs (Hardy 2001, CDP 2011, Masanes-Müller 2011 all proceed identically).
Quantum Reconstruction (3)
| File | Axiom | Source |
|——|——-|——–|
| Step3_LocalTomography.lean | hardy_reconstruction | Hardy 2001 |
| Step3_LocalTomography.lean | product_effects_separate_states | Hardy/CDP/MM — tomographic completeness |
| Step4/Purification.lean | cdp_purification_k2 | CDP 2011 — Purification → K=2 |
Hilbert Space (1)
| File | Axiom | Source |
|——|——-|——–|
| Step4/Purification.lean | no_hiding_theorem | Braunstein-Pati 2007 |
Born Rule / Entropy (4)
| File | Axiom | Source |
|——|——-|——–|
| Step6_BornRule.lean | gleason_theorem | Gleason 1957 |
| Step6_BornRule.lean | von_neumann_entropy | von Neumann 1932 |
| Step6_BornRule.lean | maxent_forces_pure_state | Jaynes 1957 |
| Step6_BornRule.lean | nonlinearity_implies_signaling | Torres Alegre 2025 |
Dynamics (5)
| File | Axiom | Source |
|——|——-|——–|
| Step9_EnergyAction.lean | stones_theorem | Stone 1932 |
| Step9_EnergyAction.lean | noether_theorem | Noether 1918 |
| Step9_EnergyAction.lean | planck_constant | Empirical |
| Step9_EnergyAction.lean | planck_constant_pos | Empirical |
| Step9_EnergyAction.lean | hamiltonian | Standard QM |
Physical Inputs (3)
| File | Axiom | Source |
|——|——-|——–|
| Step9_EnergyAction.lean | hamiltonian_isSelfAdjoint | Physical input (real energy spectrum) |
| Step10_Schrodinger.lean | schrodinger_from_stone | Stone’s theorem (unbounded ops) |
| Step3_LocalTomography.lean | product_effects_separate_states | (listed above) |
REMAINING (0) — None
All derivation targets have been resolved. No logical gaps remain.
Resolved 2026-03-23
| Axiom | Resolution |
|---|---|
QuantumStateSpace.ofCPH |
PROVEN — Module.Finite ℂ H → ProperSpace → CompleteSpace |
step4_hilbert_space |
REMOVED — side effect of CPH proof |
hamiltonian_generates_unitary |
DELETED — redundant over step7_unitarity |
hamiltonian_generates_group_mul |
DELETED — redundant over evolution_group_composition |
product_effects_separate_states |
RECLASSIFIED → EXTERNAL (Hardy/CDP/MM) |
hamiltonian_isSelfAdjoint |
RECLASSIFIED → EXTERNAL (physical input) |
schrodinger_from_stone |
RECLASSIFIED → EXTERNAL (Stone theorem) |
Reduction History
| Date | Total | PRIMITIVE | EXTERNAL | REMAINING | Sorries |
|---|---|---|---|---|---|
| 2025-11-01 | ~45 | — | — | — | — |
| 2026-03-17 | 31 | 3 | 14 | 14 | 0 |
| 2026-03-21 | 24 | 3 | 18 | 3 | 0 |
| 2026-03-23 | 19 | 3 | 16 | 0 | 0 |
Net reduction: −12 axioms in one session (2026-03-23).
HCAE — Human-Curated, AI-Enabled
Updated by Perplexity Computer + ThinxS collaboration, 2026-03-23