Run the claim. Diff the output.
Each lab is a self-contained script, a reference output from a fresh run, a chart drawn from the measured numbers, and an honest-scope box naming the tier and the kill condition. No API keys. No GPU. Seconds on a laptop. If your run disagrees with the reference output, that is a finding: tell us.
Regge triangulation
Chop Schwarzschild and de Sitter into up to 1.6M 4-simplices. Measure the h² deficit law and the h⁴ recognition correction. Flat-space null test built in.
Bekenstein spectrometer
Exact GF(2) capacity defects on strips, patches, and the torus. Integer seam gluing law; the kill condition is preregistered and the pressure on it is reported.
Lattice Lorentz
Cos-Laplacian dispersion matching Lean: quadratic, never linear, LV. MODEL estimate vs Fermi-LAT, IceCube, and clock bounds.
Six gravity numbers
SI bridge, black-hole log coefficient between LQG and string, Page time, vacuum rung, w(z) thawing drift. Post-audit, tiers per block.
The 3/8 crossing
SM and MSSM running to sin²θW = 3/8. The crossing value is exact; the SM scale misses the GUT window and the page says so.
Bit-exact mass ratio
Muon/electron between rungs 11 and 12 of the φ-ladder, certified with integer arithmetic only. Mirror of the Lean certificate.
PMNS χ²
Preregistered φ-harmonic neutrino mixing vs NuFIT 5.2. The θ₂₃ octant tension is shown; Lean δCP = 204.5° sits 0.45σ from NuFIT.
Galaxy rotation
RS causal-response gravity vs 99 SPARC rotation curves with zero per-galaxy parameters, against a MOND baseline on identical masks. The preregistered gate verdict is printed verbatim.
The Regge cubic
Third derivative of the Regge action by five-point stencil. Two symmetry nulls land at zero and the h² truncation / h⁻³ roundoff crossover is measured, not asserted.
Solar eigenvalues
The 4-site chain has eigenvalues exactly ±φ, ±1/φ (theorem). The stellar application is a hypothesis tested against BiSON and Kepler, and most tests miss.
Erdős–Straus
Recognition-cost guided search for 4/n unit-fraction splits over every hard-class n up to 250,000. Each solution re-verified in exact integer arithmetic.
The α construction
The canonical 44π·e^(−w₈lnφ/44π) with w₈ derived as a Lean theorem. It lands 5.6 ppm above CODATA, and our own theorems prove the miss at >30,000σ.
Download the script. Run it. Diff against the reference output. Read the honest-scope box before citing anything. THEOREM means proved in Lean with the axiom audit clean; MEASURED means a number from a run with a null test; MODEL means a definitional choice; HYPOTHESIS means a prediction with a named falsifier; OPEN means we have not derived it yet and say so. The weakest link sets the tag, and a lab that reports pressure against its own live bet (see Bekenstein) is working as designed.