anchorEquality
plain-language theorem explainer
The equality states that the anchor residue for any Standard Model fermion equals the gap function evaluated at its Z-index. Researchers matching RG flow residues to the phi-ladder mass formula would cite this when closing the Single Anchor Phenomenology claim at scale μ⋆. The proof is immediate reflexivity on the definition of residueAtAnchor.
Claim. For every fermion species $f$, the anchor residue satisfies $r(f) = F(Z(f))$, where $Z(f)$ is the charge-indexed integer $4 + q^2 + q^4$ (quarks), $q^2 + q^4$ (charged leptons), or $0$ (neutrinos) with $q = $ tilde charge, and $F(Z) = $ ln$(1 + Z/φ)/$ln$φ$.
background
The module defines the 12 Standard Model fermions as an inductive type Fermion. ZOf maps each fermion to its integer Z via sector and tilde charge: 4 + q² + q⁴ for up/down quarks, q² + q⁴ for leptons, and 0 for neutrinos. The gap function is the closed-form display F(Z) = ln(1 + Z/φ)/ln(φ), which the integrated RG residue is claimed to equal at the anchor scale μ⋆ per the module doc.
proof idea
The proof is a one-line wrapper that applies reflexivity to the definition of residueAtAnchor, which is exactly gap composed with ZOf.
why it matters
This closes the definitional step linking residueAtAnchor to gap(ZOf), feeding the parent claim in RSBridge.Anchor that equates the RG-transport residue to the display function. It supports the mass formula yardstick * φ^(rung-8+gap(Z)) on the phi-ladder and the Single Anchor Phenomenology relation (1/ln φ) ∫ γ_i d(ln μ) ≈ gap(ZOf i) with tolerance ~1e-6.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.