rsAlphaFactor
plain-language theorem explainer
rsAlphaFactor supplies the 44π base factor for the Recognition Science derivation of the inverse fine structure constant. Researchers assembling α^{-1} from gauge loop areas in the recognition lattice cite this constant when building the full expression that approximates 137.036. It is introduced as a direct real-number assignment with no lemmas or computation steps.
Claim. The base factor in the Recognition Science expression for the inverse fine structure constant is defined as $44π$.
background
The module derives the fine structure constant from Recognition Science, stating that α^{-1} equals 44π times a correction factor and approximates 137.036. The 44π term is the gauge loop area in the recognition lattice, where the rung equals gap(3) minus 1. No upstream results are referenced; the definition stands as the initial numerical anchor for the module's positivity and magnitude theorems.
proof idea
The declaration is a direct definition that assigns 44 multiplied by the real constant pi, with no tactics or lemmas applied.
why it matters
This definition supplies the numerical core that alpha_rung_factor equates to alphaRung times pi and that FineStructureCert uses to certify positivity and the bound above 100. It realizes the 44π gauge loop area in the RS α^{-1} formula, consistent with the framework prediction that α^{-1} lies inside (137.030, 137.039). It anchors the base constant before any correction terms are introduced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.