gap_zero_at_neutrino
plain-language theorem explainer
The gap correction vanishes for neutral fermions with charge index Z = 0. Researchers reconciling the structural rung mass formula with the gap-adjusted anchor mass in Recognition Science cite this to confirm neutrinos require no anomalous-dimension shift. The proof is a direct term-mode simplification that unfolds the gap definition and reduces log(1 + 0/phi) to zero via simp.
Claim. The gap function defined by $gap(Z) = log(1 + Z/phi) / log phi$ for integer charge index $Z$ satisfies $gap(0) = 0$.
background
The module compares two mass expressions: rs_mass_MeV (structural rung formula without gap) and massAtAnchor (rung formula multiplied by exp(gap(ZOf f) * log phi)). The gap term is the integrated mass anomalous dimension from anchor scale mu_* to physical scale mu_phys. Upstream results supply the gap definition in AnchorPolicy as the logarithmic ratio (Real.log (1 + (Z / phi))) / Real.log phi, with Z drawn from ChargeIndex.
proof idea
The proof is a one-line term-mode wrapper. It unfolds the gap definition to expose log(1 + 0/phi), then applies simp to reduce the argument of the logarithm to 1 and obtain zero.
why it matters
This result supplies the gap_at_zero field inside schemeReconciliationCert_holds, which certifies that gap corrections match the required signs and vanish at Z = 0. It closes the structural identity between the phi-ladder rung formula and the RGE-integrated mass correction in the Recognition Science framework, where the gap enters the mass formula as the adjustment phi^(rung - 8 + gap(Z)).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.