alphaRung
plain-language theorem explainer
Recognition Science fixes the rung index for the inverse fine structure constant at the natural number 44. This supplies the base 44π gauge loop area in the lattice prediction α⁻¹ ≈ 137.036. The definition is a bare constant assignment with no reduction steps.
Claim. In the Recognition Science model the rung index for the inverse fine structure constant is the natural number 44.
background
The module FineStructureConstantFromRS assembles the RS prediction α⁻¹ = 44π × correction ≈ 137.036. The factor 44π is identified as the gauge loop area in the recognition lattice, with the rung set to gap(3) - 1 where 3 is the spatial dimension fixed by the eight-tick octave. The module documentation states the three structural facts: the rung equals 44, the factor is positive, and the factor exceeds 100.
proof idea
The declaration is a direct constant assignment of 44 to alphaRung.
why it matters
This definition supplies the integer rung required by the fine-structure theorems in the same module. It is used by alphaRung_eq to confirm equality with 44, by alpha_rung_factor to establish 44π as the gauge loop denominator, and by FineStructureCert to certify the base facts. It realizes the structural claim rung = gap(3) - 1 and anchors the RS α⁻¹ value inside the interval (137.030, 137.039).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.