equalZ_at_any
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.
claimIf 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 in Recognition Science
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.
scope and limits
- Does not prove the physical RG residue equality in the Standard Model.
- Does not depend on the numerical value of the renormalization scale $mu$.
- Does not extend beyond the explicit model definition $f_mathrm{residue_model} f mu = mathrm{gap}(ZOf f)$.
- Does not address multi-loop threshold corrections or numerical integration.
formal statement (Lean)
60theorem equalZ_at_any {f g : Fermion} (hZ : ZOf f = ZOf g) (mu : ℝ) :
61 f_residue_model f mu = f_residue_model g mu := by
proof body
Term-mode proof.
62 simp [f_residue_model, hZ]
63
64end AnchorPolicyModel
65end IndisputableMonolith.Physics