rg_residue_value
plain-language theorem explainer
A predicate that tags any real number val as the perturbative RG residue for a given fermion species f. Physicists comparing the phi-ladder mass formula against Standard Model beta-function integrals cite it when quantifying the gap that defines Recognition Strength. The body reduces to the constant true proposition, acting as an extensible placeholder for the integral.
Claim. For fermion species $f$ and real number $val$, the predicate holds that $val$ is the perturbative RG residue $f_{RG}$ of $f$.
background
The Recognition Coupling module formalizes the discrepancy between the geometric mass formula on the phi-ladder, which requires large residues F(Z) (electron at Z=1332 needs F approximately 13.95), and the small residues from perturbative RG integration of Standard Model beta functions (electron approximately 0.05). The predicate supplies the placeholder for the perturbative residue f_RG to set up the ratio called Recognition Strength. Upstream, the Fermion inductive type enumerates the species (electron, mu, tau, neutrinos, up/down-type quarks) and related modules supply the geometric residue and RG transport structures.
proof idea
The definition is a direct abbreviation that sets the predicate to the constant true proposition. No lemmas or tactics are invoked; it functions as a one-line scaffolding placeholder.
why it matters
The predicate anchors the comparison that produces Recognition Strength as the factor bridging geometric and perturbative contributions. It supports the framework landmarks T5 J-uniqueness and T6 phi fixed point by preparing the mass formula residue for later coupling to the forcing chain. The module leaves open whether a single universal ratio exists independent of scheme and endpoints.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.