This repository was archived by the owner on Apr 10, 2026. It is now read-only.
FD v98 (b1196fb)
First Distinction b1196fb
Machine-verified derivation of spacetime structure from pure type theory.
Zero-Parameter Predictions
| Quantity | Value | Source |
|---|---|---|
| Spatial dimensions | d = 3 | K₄ Laplacian eigenvalue multiplicity |
| Lorentz signature | (−,+,+,+) | Drift irreversibility |
| Einstein coupling | κ = 8 | dim × χ = 4 × 2 |
| Fine structure | α⁻¹ = 137.036 | Operad arities |
| Cosmic age | τ = 13.7 Gyr | N = 5 × 4¹⁰⁰ |
Changes since v97
- Refactor: Interval arithmetic and structural derivations (b1196fb)
- Add Codebase Navigation map to README.md for the 14,000+ line Agda file (89447b4)
- Refine terminology: replace internal metaphors with professional academic language (877e7e7)
- Professionalize documentation and establish the 'Red Line of Necessity' narrative (c5b99d8)
Verify: agda --safe --without-K --no-libraries FirstDistinction.agda