equalZ_at_any
plain-language theorem explainer
Fermions sharing the same Z-value yield identical residues under the anchor model at every renormalization scale. Residue modelers invoke this when substituting equivalent fermion anchors without altering the computed residue. The term proof reduces directly by unfolding the residue definition and applying the Z-equality hypothesis.
Claim. If fermions $f$ and $g$ satisfy $Z(f)=Z(g)$, then the model residue satisfies $f_mathrm{residue}(f,mu)=f_mathrm{residue}(g,mu)$ for every real $mu$, where the model residue is defined as $mathrm{gap}(Z(f))$.
background
The AnchorPolicyModel supplies a Lean-native computable stand-in for the RG residue, defined by $f_mathrm{residue_model}(f,mu):=mathrm{gap}(ZOf(f))$. This makes the residue constant in scale $mu$ and dependent only on the integer $ZOf(f)$. The inductive type Fermion enumerates the standard quarks and leptons; $ZOf$ assigns the integer via cases on sector and $tilde Q(f)$, yielding 0 for neutrinos, $q^2+q^4$ for leptons, and $4+q^2+q^4$ for up/down quarks.
proof idea
The proof is a one-line wrapper that applies simplification to the definition of $f_mathrm{residue_model}$ together with the hypothesis $ZOf(f)=ZOf(g)$.
why it matters
The result encodes the single-anchor closed-form property inside the model, guaranteeing that residue calculations depend only on $Z$ and remain invariant under fermion interchange at fixed $Z$. It supports downstream algebraic work on anchor identities without requiring the full multi-loop RG implementation. The construction aligns with the Recognition Science emphasis on definitional closure for residue functions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.