alpha_value
plain-language theorem explainer
The theorem sets the Recognition Science approximation to the fine-structure constant exactly equal to 1/137. Researchers modeling QED corrections or vacuum fluctuations via J-cost would cite this fixed value for Lamb-shift numerics. The proof is a direct reflexivity step confirming definitional equality in the preceding alpha_approx construction.
Claim. In the Recognition Science QFT model the approximated fine-structure constant satisfies $alpha_{approx} = 1/137$.
background
The module derives the Lamb shift from vacuum J-cost fluctuations, where J(x) = (x + x^{-1})/2 - 1 encodes the Recognition Composition Law and position uncertainty for the electron. Upstream structures supply the phi-ladder tiers (NucleosynthesisTiers), ledger factorization (DAlembert), J-cost convexity (PhiForcingDerived), and the emergence of SU(3) x SU(2) x U(1) from simplicial data (SpectralEmergence). The local setting treats the 2S-2P splitting as a modification of orbital J-cost induced by ledger fluctuations.
proof idea
The proof is a one-line term-mode reflexivity (rfl) that succeeds because alpha_approx is definitionally equal to 1/137 by its preceding definition.
why it matters
This anchors the fine-structure constant at the observed approximate value inside the Recognition Science framework and supplies the numerical input for the Lamb-shift fraction (lambShiftFraction). It sits downstream of the phi-forcing chain (T5 J-uniqueness through T8 D=3) and the alpha band (137.030-137.039) while feeding the QFT Lamb-shift derivation. The exact match closes the leading-order approximation for vacuum-fluctuation calculations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.