geometricResidue
geometricResidue assigns to fermion f the gap value at its integer label ZOf(f). Unification researchers comparing phi-ladder masses to SM renormalization flows cite this when forming recognition strengths. It is a direct one-line composition of the upstream gap and ZOf maps.
claimFor fermion species $f$, the geometric residue is defined by $F(Z_f)$ where $Z_f$ is the integer label obtained from the charge index of $f$ by sector and $F(Z) = (1/2) (Z / phi) / log_phi$ in the logarithmic form supplied by the anchor residue.
background
The Unification.CouplingLaw module bridges geometric phi-ladder residues to perturbative RG running. The gap function supplies the closed-form residue $F(Z) = log(1 + Z/phi) / log(phi)$ at the anchor scale, while ZOf maps each Fermion (electron, quarks, neutrinos) to its integer Z via sector-dependent quadratic and quartic charge terms. Upstream Gap45.Derivation.gap states that the gap equals the product of closure and Fibonacci factors, and the RSBridge.Anchor version gives the explicit logarithmic display function used here.
proof idea
One-line definition that applies the gap function directly to the output of ZOf on the input fermion.
why it matters in Recognition Science
This definition supplies the geometric input to recognitionStrength and the theorems coupling_law_determines_strength and structural_dominance. It realizes the mass formula's yardstick on the phi-ladder for each species, as required by T5 J-uniqueness and the Recognition Composition Law that forces J = cosh - 1. The module resolves the O(10^2-10^3) ratio between geometric F(Z) and perturbative f_RG via the cosh enhancement S(t).
scope and limits
- Does not compute or reference any perturbative residue value.
- Does not fix numerical values of phi or other constants.
- Does not derive the gap function or prove its equality to 45.
- Does not address running-scale dependence beyond the anchor.
Lean usage
theorem strength_def (pr : PerturbativeResidue f) : recognitionStrength pr = geometricResidue f / pr.value := rflformal statement (Lean)
214def geometricResidue (f : Fermion) : ℝ := gap (ZOf f)
proof body
Definition body.
215
216/-- The perturbative residue packages a positive RG running value. -/