GIFT Core

Structure

GIFT/ # Lean 4 formalization (root library)
├── Core.lean # Constants (dim_E8, b2, b3, H*, ...)
├── Certificate/ # Modular certificate system
│ ├── Core.lean # Master: Foundations ∧ Predictions ∧ Spectral
│ ├── Foundations.lean # E8, G2, octonions, K7, Joyce, NK cert (34 conjuncts)
│ ├── Predictions.lean # 33+ relations, ~50 observables (56 conjuncts)
│ └── Spectral.lean # Mass gap, TCS, computed spectrum, Weyl law (37 conjuncts)
├── Foundations/ # Mathematical foundations (23 files)
│ ├── RootSystems.lean # E8 roots in R8 (240 vectors)
│ ├── E8Lattice.lean # E8 lattice, Weyl reflection
│ ├── G2CrossProduct.lean # 7D cross product, Fano plane
│ ├── ExplicitG2Metric.lean # 169-param Chebyshev-Cholesky
│ ├── NewtonKantorovich.lean # NK cert: h < 0.5, decomposed
│ ├── NumericalBounds.lean # Taylor series bounds (axiom-free)
│ └── Analysis/ # G2 forms, Hodge theory, Sobolev
├── Geometry/ # Axiom-free DG infrastructure
│ ├── HodgeStarR7.lean # ⋆, ψ=⋆φ PROVEN, TorsionFree
│ └── HodgeStarCompute.lean # Explicit Hodge star (Levi-Civita)
├── Spectral/ # Spectral gap theory (17 files)
│ ├── PhysicalSpectralGap.lean # dim(G2)−h = 13 algebraic (zero axioms)
│ ├── ComputedSpectrum.lean # Q22 sig, SD/ASD gap, B-test
│ └── CheegerInequality.lean # Cheeger-Buser bounds
├── Algebraic/ # Octonion/G2 algebraic foundations
│ └── G2ThreeForm.lean # φ0 3-form, G2=Stab(φ0), g2=ker(L_φ0), dim=14
├── Relations/ # Physical predictions (22 files)
├── Observables/ # PMNS, CKM, quark masses, cosmology
├── Hierarchy/ # Dimensional gap, absolute masses
GIFTTest/ # Lean test files
blueprint/ # Leanblueprint dependency graph
contrib/ # Non-Lean assets
├── python/ # Python package (giftpy on PyPI)
│ └── gift_core/ # Certified constants export
├── homepage/ # GitHub Pages / Jekyll site
└── docs/ # Extended documentation

Quick Start

pip install giftpy

from gift_core import *
print(SIN2_THETA_W) # Fraction(3, 13)
print(GAMMA_GIFT) # Fraction(511, 884)
print(TAU) # Fraction(3472, 891)

Building Proofs

lake build

Documentation