gap_zero_neutral
plain-language theorem explainer
The gap correction vanishes at zero charge, fixing the neutral baseline for rung scaling in the master mass formula. Physicists deriving particle masses on the phi-ladder cite this when anchoring the zero point of the charge shift. The proof is a direct term-mode simplification that unfolds the gap definition and reduces via arithmetic and logarithm identities.
Claim. The recognition gap correction satisfies $gap(0)=0$, where $gap(Z)=log_φ(1+Z/φ)$.
background
The master mass law states that stable particle masses obey m = yardstick(Sector) * φ^{r-8+gap(Z)}, with r the species rung and gap(Z) the charge-induced correction to the exponent. The local gap_correction is defined by gap(Z) = log(1 + Z/φ) / log φ, which is the base-φ logarithm of the linear charge shift. This places the neutral sector (Z=0) at the exact integer rung without offset. Upstream results include the arithmetic identity n + zero = n and the separate gap-45 factor 1 + 45/(360*137) arising from the D=3 integration gap.
proof idea
The term-mode proof unfolds the local gap_correction definition, then applies simp with Int.cast_zero, zero_div, add_zero, Real.log_one and zero_div to reduce log(1 + 0/φ)/log φ directly to zero.
why it matters
This anchors the neutral baseline inside the master mass law, ensuring the exponent collapses to r-8 for Z=0 and supporting all subsequent mass predictions on the phi-ladder. It aligns with the eight-tick octave and D=3 geometry that generate the gap series. The result closes the zero-charge case before the full predict_mass machinery is applied.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.