rg_residue_value
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not compute any integral from beta functions.
- Does not assign a specific numerical value to the residue.
- Does not claim the residue is independent of renormalization scheme.
- Does not equate the perturbative residue to the geometric residue.
- Does not extend the predicate beyond the listed fermion species.
formal statement (Lean)
55def rg_residue_value (f : Fermion) (val : ℝ) : Prop :=
proof body
Definition body.
56 -- This is a predicate stating that the species f has perturbative residue 'val'.
57 True
58
59/-- The Recognition Strength for species f: the factor by which the geometric
60 structure exceeds the perturbative RG effect. -/