equalZ_residue
plain-language theorem explainer
Fermions sharing the same charge-indexed integer Z have identical residues at the anchor scale, since the residue is defined directly as the gap function of Z. Model builders using the Recognition Science mass ladder would invoke this when assigning equal residues to species in the same Z-class for phi-power mass ratios. The proof is a one-line simplification that unfolds the residue definition and substitutes the Z-equality hypothesis.
Claim. Let $f$ and $g$ be fermions. If the charge-indexed integer $Z(f)$ equals $Z(g)$, then the anchor residue of $f$ equals the anchor residue of $g$, where the residue is the gap function applied to $Z$.
background
The module bridges Recognition Science to the Standard Model by defining the 12 fermions (6 quarks, 3 charged leptons, 3 neutrinos) as an inductive type. The function ZOf computes the integer $Z_i = q̃^2 + q̃^4$ (plus 4 for quarks) from the tilde charge and sector. The anchor residue is defined as the gap function of this Z-value, serving as the closed-form target for the integrated RG residue at the anchor scale μ⋆. Upstream results establish that the RG-transport residue equals this gap expression under the Single Anchor Phenomenology claim, with the gap given explicitly as ln(1 + Z/φ) / ln(φ).
proof idea
One-line wrapper that applies simp to unfold residueAtAnchor into gap(ZOf f) and substitute the hypothesis ZOf f = ZOf g.
why it matters
The result guarantees that anchor residues depend only on Z, enabling the mass formula to assign identical phi-ladder positions to equal-Z species. It supports the core claim in the RSBridge module that the RG-integrated residue matches gap(ZOf f) at the anchor, linking directly to the phi-ladder and eight-tick octave structure. The declaration closes a basic consistency step before numerical verification of the residue equality.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.