f_residue_model
plain-language theorem explainer
This definition supplies a scale-independent model for the RG residue of any fermion species by setting the value to the gap function at the species Z index. Researchers exploring algebraic consequences of the Recognition Science single-anchor closed form would cite it to obtain executable identities without axioms. The implementation is a direct substitution of the closed-form gap expression.
Claim. The model residue for fermion species $f$ at any scale parameter is defined by $f(f, mu) := gap(Z(f))$, where $gap(Z) = ln(1 + Z/phi)/ln(phi)$ and $Z(f)$ is the integer obtained from the sector and squared-charge rules for $f$.
background
The AnchorPolicyModel module supplies a Lean-native computable stand-in for the Standard-Model RG residue, which the parent module treats as an opaque axiom. In this model the residue equals the display function gap(Z) by construction. The gap function is the closed form F(Z) = ln(1 + Z/φ) / ln(φ) that the integrated mass anomalous dimension is claimed to match at the anchor scale. ZOf assigns to each fermion an integer Z via sector rules: 4 + q² + q⁴ for quarks, q² + q⁴ for charged leptons, and 0 for neutrinos. The upstream gap derivation establishes that the gap product equals 45 as the main theorem.
proof idea
The definition is a direct abbreviation that substitutes gap applied to ZOf f for the residue value. No tactics or lemmas are invoked beyond the referenced gap and ZOf definitions.
why it matters
This definition underpins the downstream results equalZ_at_any, stationary_at_any, and stability_bound_at_any, which establish degeneracy, vanishing first derivative, and bounded second derivative in the model. It realizes the single-anchor closed form as a definition rather than a phenomenology axiom, allowing algebraic consequences of the Recognition Science residue identity to be checked inside Lean. The construction closes the interface for the anchor policy while leaving the full multi-loop RG verification as an open question.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.