Every number is machine-checked.
TFPT is built like a compiler, and verified like one. Nothing is marked closed that is not re-derived from the two axioms by an independent script, and no dimensionful quantity is claimed as a derivation from pure numbers. The graph below shows exactly how each result is computed, on which inputs it depends, and which scripts check it — including the self-consistency loop that fixes the inputs themselves. Every script is runnable live in your browser — click one to execute the real Python (via Pyodide / WebAssembly) and watch the checks pass, step by step.
Four independent paths, one ledger
A claim is only as strong as the way it is checked. The dimensionless skeleton is verified three independent ways and typed in a single versioned ledger, so the papers, the suite and the ledger stay in lock-step.
One file per claim cluster; run_all.py ends ALL CHECKS PASSED. Exact sympy where possible, mpmath/numpy otherwise.
An independent second path for the exact algebraic / identity / lattice results, on the Wolfram Engine.
The P2 carrier algebra — hypercharge, anomaly-freedom, integer rigidity — formalised in Lean 4 with only kernel axioms.
status_ledger.csv types every claim (id, status, location, dependency, script) and is versioned. If the text and the ledger disagree, the ledger wins.
How each result is computed
Two axioms at the source, the E₈ compiler in the middle, the observables as sinks. Click any node to see what it is, its status marker, its inputs and outputs, how it can fail, and the scripts that machine-check it — then click a script to run it live in your browser. The dashed rose edges are the bootstrap: the E₈ closure feeds back and fixes the inputs.
E₈ — the μ₄ glue (audit hull)
[L] lattice theoremD₅ and A₃ share the discriminant group ℤ₄; their glue norms add to the root norm, q(D₅) + q(A₃) = 5/4 + 3/4 = 2. So E₈ = (D₅ ⊕ A₃) + μ₄ closes as a lattice theorem. E₈ is the unimodular audit hull, not a gauge group; 240 = 16·5·3 roots, 248 = 240 + 8.
- D₅
- A₃
- 240 roots, 248 = dim E₈
- Not even-unimodular; glue norms do not sum to 2.
Five commands, from the repository root
Dependencies: a LaTeX distribution, Python 3 with sympy / mpmath / numpy / matplotlib; optionally the Wolfram Engine and Lean 4. Every script cited in run_all.py is also cited inline in the documents, and the status heatmap is generated directly from the ledger.
# 1. Compile the 8 active documents -> "8 ok, 0 failed"
bash build.sh notes
# 2. Run the Python verification suite -> "ALL CHECKS PASSED"
cd verification && python run_all.py
# 3. Independent Wolfram path (optional) -> "101/101 passed"
wolframscript -file verification/wolfram/tfpt_readouts.wl
# 4. Lean carrier-rigidity proof (optional) -> "AUDIT: PASS"
cd experiments/lean4-carrier-rigidity && lake exe cache get && bash scripts/audit.sh
# 5. Regenerate the reproducibility manifests (run last)
python verification/make_manifest.pyWhat each script checks
The full verification suite, grouped by what it proves. Every script links to its source in the public repository.
The suite is organised by what it proves. Each script is one claim cluster, cited inline in the documents via \veri{vN} and registered in run_all.py, which ends ALL CHECKS PASSED. Click any script to run it live in your browser.
81 scriptsCompiler core & the E₈ glue
9Why the two axioms build E₈, why the carrier rank is forced, and the integer skeleton that follows.
Electromagnetic fixed point
2The fine-structure constant as the unique root of the boundary U(1) Ward identity.
Flavor matrix & operators
7The integer operator ladder (R, K, Q, L) and its spectral invariants — the flavor signature.
Masses, leptons & quark ratios
9The φ₀-ladder mass formula, the exact lepton coefficients, and the integer-Plücker quark ratios.
Neutrinos & the solar angle
3The Majorana texture, the dual anchor, and the previously open solar angle from the seam.
Gravity, inflation & cosmology
4The R + R² spectral-action shadow, the seam-fixed scalaron, and the cosmological readouts.
Horizon code & Origin Theory (self-consistency)
11The seam as the universal horizon code, the order-30 Coxeter cycle, and the gapped unique attractor that makes parameter-freeness a theorem.
Open gate (U_wall) — the flavor wall
11The parabolic wall-selection contract: the quark ratios are closed; only the absolute amplitude scale stays open.
Open gate (G_metric) & the frontier
25The quantum-gravity measure contract, the audit ledger, the data scorecard, and the honestly-typed frontier items.
Independent scrutiny is the point
These checks are reproducible by anyone — that is what “independent” means here: the same result falls out on your machine, on an independent Wolfram path, and (for the carrier) in Lean. We do not claim external endorsements; we invite review. Open questions and known limitations are tracked openly in the research contracts and the status ledger — disagreements go in the issue tracker.