alphaRung_eq
plain-language theorem explainer
The equality fixes the recognition rung for the fine structure constant at 44. Researchers assembling the RS prediction of alpha inverse would cite this rung when building the 44 pi base factor from the gauge loop area. The proof reduces immediately by reflexivity to the definition of alphaRung as the natural number 44.
Claim. The recognition rung for the fine structure constant satisfies $r = 44$.
background
In the FineStructureConstantFromRS module the recognition ladder supplies a rung number that enters the inverse fine structure constant as the leading factor 44 pi. The module states that this rung equals gap(3) minus one and that the full prediction reads alpha inverse approximately 137.036 after a correction term. The upstream definition alphaRung simply sets the natural number 44.
proof idea
The proof is a one-line reflexivity reduction that matches the defining equation of alphaRung.
why it matters
This equality supplies the rung value to the fineStructureCert certificate that assembles the full fine structure constant prediction. It realizes the structural fact that the rung equals gap(3) minus one and contributes the 44 pi factor inside the Recognition Science derivation of the alpha band. The parent result is the fineStructureCert definition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.