equalZ_residue
plain-language theorem explainer
Fermions with equal Z-values under the charge-index map share the same anchor residue. Modelers of Standard Model mass hierarchies in the recognition framework cite this when grouping species for phi-power ratios. The proof is a one-line simp wrapper that unfolds the residue definition and substitutes the Z equality.
Claim. Let $f$ and $g$ be fermions. If $Z(f) = Z(g)$, where $Z$ is the integer $Z_i = q̃^2 + q̃^4$ (plus 4 for quarks) computed from the sector and charge index, then the anchor residues satisfy $r(f) = r(g)$, with $r(f)$ the gap function $F(Z(f)) = ln(1 + Z(f)/φ) / ln(φ)$.
background
The module defines Fermion as the inductive type enumerating the twelve Standard Model species (six quarks, three charged leptons, three neutrinos). ZOf maps each fermion to its integer via tildeQ and sectorOf, adding 4 for up/down quarks. residueAtAnchor is the noncomputable definition residueAtAnchor f := gap (ZOf f), where gap is the closed-form display function F(Z) = ln(1 + Z/φ) / ln(φ). This supplies the target value that the integrated RG residue from Physics/RGTransport is claimed to match at the anchor scale μ⋆ under the single-anchor phenomenology axiom.
proof idea
The proof is a one-line wrapper that applies simp to the definitions of residueAtAnchor and the hypothesis ZOf f = ZOf g, reducing both sides to gap(ZOf f) and gap(ZOf g) which coincide by substitution.
why it matters
The result ensures the anchor residue depends only on Z, enabling the anchor_ratio claim that equal-Z family members differ by pure phi-powers on the mass ladder. It directly supports the bridge to RGTransport residueAtAnchor and the display_identity_at_anchor axiom in AnchorPolicy.lean, closing the step from charge index to residue before mass formulas are applied. It touches the open numerical verification of the ~1e-6 tolerance between closed-form gap and integrated gamma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.