Fine-structure constant

Fine-structure constant

The fine-structure constant is the dimensionless number that sets the strength of electromagnetic interactions. Recognition Science fixes a kinematic contribution to its inverse, while the normalization that would set the measured value remains open. The retired 4π·11 construction is a model witness near CODATA, not a derivation of the measured fine-structure constant.

The expression for the inverse coupling is α⁻¹ = (4π·11) · exp(−(w₈·ln φ)/(4π·11)). The seed supplies the retired construction's scale, and the gap term supplies its exponential dressing. The source proves that alphaInv equals a seed times an exponential gap factor, with the seed equal to alpha_seed and the gap equal to f_gap. THEOREM

The seed 4π·11 is a retired model choice, not a derived electromagnetic normalization. Its 11 counts passive field edges after one active edge per tick is fixed, while the gauge-invariant cycle count is 5. The repeated appearance of 11 in other constructions is evidence for recurring structure, not a fitted normalization. The seed 4π·11 is retired and does not determine the electromagnetic normalization.

The forced kinematic value is 4π·φ⁵ − 5·ln φ, about 136.957, below the construction band (137.030, 137.039). The forced sector cannot derive the measured inverse coupling because it leaves the electromagnetic normalization free. The forced kinematic value lies below the construction band, leaving the gap to the measured inverse constant as free electromagnetic normalization.

CODATA 2022 gives 137.035999084(21) for the inverse fine-structure constant. The witness is about 5.6 parts per million from that value, while its certified band is roughly 429,000 times wider than the measurement resolution. The witness's central value is excluded by the measurement at more than 30,000 sigma. The overlap of the wide band with CODATA does not select the measured value.

The recognition framework therefore leaves the boundary datum explicit: a positive electromagnetic normalization can move the inverse coupling while preserving the forced closure. The retained seed is useful as a record of a near-match, and its status remains MODEL rather than a derivation of measured α.

THEOREM alphaInv_components_eq · IndisputableMonolith/Constants/Alpha.lean

MODEL alphaInv · IndisputableMonolith/Constants/Alpha.lean

MODEL alpha_seed · IndisputableMonolith/Constants/Alpha.lean

MODEL alpha · IndisputableMonolith/Constants/Alpha.lean

What this page does not claim

Not a derivation of the measured fine-structure constant. Not a prediction of the exact CODATA value. Not a claim that the seed 4π·11 is a derived gauge normalization.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Constants/Alpha.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: