gap_correction
plain-language theorem explainer
The gap correction computes log base phi of (1 + Z/phi) for integer charge index Z, shifting the effective rung in the phi-ladder mass formula. Particle physicists applying Recognition Science to species masses cite it when evaluating the master law m = yardstick(Sector) * phi^(r - 8 + gap(Z)). The definition is realized directly as the change-of-base logarithm expression.
Claim. gap(Z) = log_φ(1 + Z/φ) for integer Z.
background
The Master Mass Law module states that every stable recognition state occupies a rung r on the φ-ladder, with mass m = yardstick(Sector) * φ^(r - 8 + gap(Z)), where 8 is the fundamental cycle period and gap(Z) corrects for charge-induced skew. The gap term is defined as the base-φ logarithm log_φ(1 + Z/φ). Upstream results supply the discrete φ-tiers from NucleosynthesisTiers.of and the J-cost structure from PhiForcingDerived.of that underwrite the ladder construction.
proof idea
One-line definition that applies the change-of-base formula: Real.log(1 + (Z_val : ℝ)/phi) / Real.log phi.
why it matters
It supplies the charge correction inside the master mass formula, feeding predict_mass, mass_rung_scaling, and gap_zero_neutral in the same module plus AlphaPrecisionCert downstream. The term realizes the recognition gap series required by the eight-tick octave (T7) and D = 3 spatial dimensions in the forcing chain. It ensures neutral particles sit at exact integer rungs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.