alpha_rung_factor
plain-language theorem explainer
The theorem equates the rung value 44 multiplied by π to the RS alpha factor in the fine structure constant derivation. Researchers deriving α^{-1} ≈ 137.036 from the recognition lattice would cite this to anchor the gauge loop area term. The proof is a one-line wrapper that unfolds the rsAlphaFactor definition and applies norm_cast to the natural-number coercion.
Claim. $44 π = rsAlphaFactor$, where rsAlphaFactor denotes the recognition-science gauge-loop factor in the α^{-1} formula.
background
In the Recognition Science module on the fine structure constant, alphaRung is the natural-number definition 44, obtained as gap(3) - 1 on the phi-ladder. rsAlphaFactor is the noncomputable real 44 * π that supplies the gauge-loop area denominator. The module states the RS prediction α^{-1} = 44π × correction ≈ 137.036 and records the structural facts that both 44π and the factor are positive.
proof idea
One-line wrapper that unfolds rsAlphaFactor (revealing 44 * Real.pi) and applies norm_cast to equate the coerced real value of alphaRung with the right-hand side.
why it matters
The declaration supplies the exact 44π identity required by the RS α^{-1} prediction, which falls inside the observed interval (137.030, 137.039). It directly supports the gauge-loop interpretation stated in the module and closes the structural link between the rung definition and the factor used in downstream certification. No open questions are addressed; the result is a proved identity with zero sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.