gap_zero
plain-language theorem explainer
The theorem shows that the structural residue function vanishes at zero argument. Mass-spectrum calculations in the Recognition framework cite it to anchor the lepton sector at Z=0. The proof is a direct simplification from the definition of the residue.
Claim. $gap(0) = 0$, where $gap(Z) := log(1 + Z/φ) / log φ$ for nonnegative integer $Z$.
background
The module supplies Lean-verified algebraic properties of the structural residue gap(Z), defined explicitly as log(1 + Z/φ) / log φ and serving as the zero-parameter Recognition-side residue f^{Rec} in the mass framework. This residue appears as the correction term on the phi-ladder mass formula. Upstream, the constant gap is introduced in Gap45.Derivation as the product of closure and Fibonacci factors, with the main theorem asserting that product equals 45.
proof idea
The proof is a one-line wrapper that applies the simp tactic to the definition of gap, which evaluates immediately to zero at argument 0 because log(1) = 0.
why it matters
This result supplies the gap_at_zero field inside the SchemeReconciliationCert structure for quark scheme reconciliation. It fixes the baseline of the zero-parameter residue at the neutrino-like Z=0 case before scaling to higher rungs such as Z=276, consistent with the phi-ladder and the eight-tick octave structure of the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.