alpha_approx
plain-language theorem explainer
Recognition Science calculations of the Lamb shift employ the rational approximation 1/137 for the fine structure constant. This value is cited when establishing that fifth-order corrections remain below 10^{-8}. The definition consists of a direct constant assignment in the rationals.
Claim. Define the approximate fine structure constant by $α_{approx} := 1/137$ where $α_{approx} ∈ ℚ$.
background
The QFT-012 module derives the Lamb shift from vacuum J-cost fluctuations. Electron jiggle arises from J-cost-driven position uncertainty that modifies orbital J-cost and splits the degenerate 2S and 2P levels. The upstream SpinStatistics.value definition supplies the real-number spin as twice the integer divided by two, providing the half-integer representation required for fermionic statistics.
proof idea
The definition is introduced by direct assignment of the rational constant 1/137. No lemmas or tactics are invoked; the body is a simple constant expression.
why it matters
It supplies the input for the exact equality theorem alpha_value and the smallness bound alpha_fifth_small. This places the approximation inside the Recognition Science prediction for the reciprocal fine structure constant near 137, consistent with the interval (137.030, 137.039) obtained from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.