gap_correction
plain-language theorem explainer
The gap-45 correction supplies the explicit numerical factor 1 + 45/(360*137) that adjusts the geometric seed of 137 when deriving the fine-structure constant from the RS forcing chain. Researchers computing RS-native alpha predictions or mass-rung scalings would cite this factor to incorporate the D=3 integration gap. The definition is a direct algebraic expression with no additional lemmas or tactics required.
Claim. The gap-45 correction factor is defined by $1 + 45/(360*137)$. This term adjusts the geometric seed for the fine-structure constant to account for the integration gap $D^2(D+2)=45$ at spatial dimension $D=3$.
background
Recognition Science derives constants from the composition law through the forcing chain: J-uniqueness yields phi as fixed point, eight-tick periodicity forces D=3, and ratios of native units produce c=1, hbar=phi^{-5}, G=phi^5/pi. The module shows alpha inverse near 137.036 emerges from a geometric seed of 137 plus a fractional correction from the D=3 gap. Upstream, gap_45 in DimensionForcing encodes the same integration gap D^2(D+2) evaluated at D=3, while the geometric seed appears in AlphaPrecision as 4pi11.
proof idea
This is a direct definition that evaluates the correction as one plus the ratio of the gap value 45 to the product of the denominator 360 and the seed 137. No lemmas are applied; the expression is written out explicitly.
why it matters
The definition supplies the explicit correction term required by the alpha derivation claim and feeds the AlphaPrecisionCert structure together with mass-law rung predictions. It closes the step from geometric seed plus gap-45 adjustment to the RS prediction alpha inverse approximately 137.036, directly implementing the T8 forcing of D=3 and the eight-tick octave in the constant-derivation chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.