Where does the fine-structure constant come from?

permalink: https://pith.science/recognition/ask/where-does-the-fine-structure-constant-come-from-e0f533e6 · first asked 2026-08-13 · browse all asks

confidence: moderate in recognition cached

1. Phi-based exponential form for alpha-inverse The RS construction assembles α⁻¹ via the exponential form α⁻¹ = 44π · exp(−w₈ ln φ / (44π)) using the structure fine_structure_derived and bounds alphaLock_numerical_bounds.

2. Numerical window: (137.030, 137.039) The assembled expression is proved to lie in the interval (137.030, 137.039).

3. CODATA 137.036 lies inside the proved window The CODATA 2022 value 137.036 falls inside the proved interval.

4. What is theorem-grade vs empirical confirmation The interval (137.030, 137.039) is theorem-grade from the RS construction; exact numerical agreement with CODATA is empirical confirmation while the precise infrared value remains an open boundary condition.

5. Cited Lean anchors Load-bearing theorems are the MUST anchors fine_structure_derived and alphaLock_numerical_bounds together with alpha_seed_eq, fineStructureCert, and geometric_seed_eq.

cited recognition theorems

FineStructureConstant.fine_structure_derived MUST anchor required by retrieval contract for fine-structure derivation
FineStructureConstant.alphaLock_numerical_bounds MUST anchor required by retrieval contract providing numerical bounds
AlphaPrecision.alpha_seed_eq defines the 44π seed used in the exponential form
FineStructureConstantFromRS.fineStructureCert SHOULD cite for the 44π factor certificate
AlphaDerivation.geometric_seed_eq derives the geometric seed 4π·11 from cube geometry

outside recognition

Aspects Recognition does not yet address:

fine_structure_derived is deprecated and equals alphaLock_structure (ILG kernel exponent), not the EM fine-structure constant per module header retraction
exact α⁻¹(0) = 137.035999 is OPEN as a boundary condition; the interval is a construction, not a first-principles derivation of the measured value
the exponential form itself is a definition, not proved unique or forced from first principles

recognition modules consulted

The Recognition library is at github.com/jonwashburn/shape-of-logic. The model is restricted to the supplied Lean source and instructed not to invent theorem names. Treat output as a starting point, not a verified proof.