Our own theorems prove this construction misses α by 36,516σ. That is the point.
The fine-structure constant α sets the strength of electromagnetism, and deriving its measured value from pure theory has been an open dream since Eddington. Recognition Science has a construction with nothing fitted to data: a geometric seed 44π, a gap weight w₈ derived as a closed-form theorem, and an exponential dressing. Run the script: it lands at 137.03677, five parts per million above CODATA's 137.035999. Five ppm sounds close. It is also more than 30,000 standard deviations wrong, and the Lean formalization proves the miss as a theorem rather than hiding it. This page shows the derivation, the miss, and the audit that keeps us from calling α derived. Most physics websites would show you only the first third.
w₈ is derived, not stored
The gap weight is the Parseval-normalized 64-cell projection of the DFT-8 of the φ-pattern.
The script computes that projection from scratch and it matches the closed form to 10⁻¹⁴.
The equality is a Lean theorem (w8_projection_equality, 0 sorry): the integers 348, 210,
204, 130, 7 fall out of the algebra. Nothing in w₈ touches α.
Wrong by 36,516σ, by our own Lean
The assembled value sits in the certified band (137.030, 137.039) and overshoots CODATA by
+0.00077. The Lean proves the overshoot exceeds 0.0007 and that 0.0007 is more than 30,000
measurement sigma (MeasurementVerdict). A construction that lands 5.6 ppm from a famous
constant with zero fitted inputs demands explanation. It is still measurably, provably, not the
constant.
44π is an identification
Three quarantine modules settle the seed's status. The gauge-invariant photon count on the cube is
the cycle rank E−V+1 = 5, not the ledger count 11, so a genuine gauge seed would be
4π·5 ≈ 63 (U1Normalization). The genuine quadratic J-cost of the cube
curvature is π² ≈ 9.87, so reading 4π·11 as a cost is a category error
(CurvatureJCostVerdict). And the assembled value exceeds the Thomson ceiling, so it is
off the physical running curve at every scale (ScaleIdentification). Five derivation
routes for the seed were tested in 2026; all closed negative.
The construction vs the measurement, drawn to scale
Top: the certified band with the assembled value and CODATA. They look adjacent; the gap between them is 0.000767, and the CODATA error bar (±2.1×10⁻⁸) is thirty-six thousand times smaller than that gap, far below one pixel. Bottom: where w₈ comes from, mode by mode, in the DFT-8 projection. Every bar is forced; their sum is the theorem-grade 2.4906.
alphaInv_gt /
alphaInv_lt. The retired legacy pipeline's value (0.4 ppb from CODATA) is shown crossed
out; see the honest-scope box for why it was retired. Bottom: per-mode contributions
64·|cₖ|²·sin²(kπ/8)·φ⁻ᵏ/Etotal from
the run.What the script actually verifies
| Check | Result | Lean mirror |
|---|---|---|
| DFT-8 Parseval: total energy = (φ¹⁶−1)/φ | 1363.3826991487 both ways | phiDFTEnergyTotal_closed_form |
| w₈ projection = closed form | 2.4905692754537 vs 2.4905692754536 (10⁻¹⁴) | w8_projection_equality (THEOREM) |
| assembled α⁻¹ in certified band | 137.036766007 ∈ (137.030, 137.039) | alphaInv_gt, alphaInv_lt |
| overshoot above CODATA | +0.000767 = +5.60 ppm = 36,516σ | alphaInvGenesis_exceeds_CODATA_by_0007, margin_0007_gt_30000_sigma |
| gauge photon count on Q₃ | cycle rank = 5 ≠ 11 | cube_cycle_rank_eq_5, seed_channel_count_ne_gauge_dof |
| legacy w₈ certificate backward-solve | stored 2.488254398 vs required 2.488254276: it encoded CODATA | retired per GapWeight.lean |
Run it yourself
One file, numpy only, under a second, no files written. The script mirrors the Lean modules step for step and prints which theorem each check corresponds to.
$ python3 alpha_w8_construction.py w8 (projection): 2.4905692754537 w8 (closed form): 2.4905692754536 alpha^-1 assembled: 137.036766007 overshoot: +0.000766830 (+5.60 ppm, 36,516 sigma) VERDICT: the parameter-free construction lands 5.6 ppm ABOVE the measured alpha^-1 and is excluded as the exact value at >30,000 sigma, by our own Lean theorems.
Mixed tier, stated exactly. THEOREM: the gap weight w₈ closed form (the projection equality is proved in Lean with 0 sorry), the certified band (137.030, 137.039), and the measurement verdict that the assembled value exceeds CODATA by more than 30,000σ. IDENTIFICATION, not derivation: the seed 44π (the gauge-invariant count is 5, not 11; the genuine curvature J-cost is π²; five candidate derivation routes all closed negative). OPEN: the exact infrared α⁻¹(0), treated as an irreducible boundary condition in the present formalization. A history note this page owes you: an earlier version of this lab showed a legacy pipeline (a stored numeric w₈ = 2.488254398 in an additive assembly) landing 0.4 ppb from CODATA. Backward-solving shows that stored number simply encoded CODATA to within 10⁻⁷, so it was retired from the certified pipeline; the derived w₈ gives the honest 5.6 ppm miss instead. A construction that cannot miss is not evidence. This one can miss, does miss, and the formalization proves the size of the miss. That, and not the ppb coincidence, is what parameter-free means.