residueAtAnchor
residueAtAnchor assigns each Standard Model fermion its closed-form RG residue at the anchor scale by applying the gap display function to the charge index ZOf f. Model builders comparing integrated anomalous dimensions to phi-ladder predictions cite this when stating the Single Anchor Phenomenology equality. The definition is a direct composition of the ZOf map and the logarithmic gap function.
claimFor a fermion $f$, the anchor residue equals $F(Z(f))$ where $Z(f)$ is the integer charge index of $f$ and $F(Z) = (1/2) ln(1 + Z/phi) / ln phi$.
background
The RSBridge.Anchor module defines the bridge from the recognition framework to the twelve Standard Model fermions. Fermion is the inductive type listing d, s, b, u, c, t, e, mu, tau, nu1, nu2, nu3. ZOf computes the charge index as 4 + q^2 + q^4 for quarks, q^2 + q^4 for charged leptons, and 0 for neutrinos, with q from tildeQ. The gap function is the display map F(Z) = ln(1 + Z/phi) / ln phi, which the module states is the closed form that the integrated RG residue is claimed to equal at the anchor scale mu star.
proof idea
This is a one-line definition that applies the gap function directly to the output of ZOf on the input fermion.
why it matters in Recognition Science
The definition supplies the closed-form target used by anchorClaimHolds in RGTransport and by the theorems anchorEquality and equalZ_residue. It fills the display_identity_at_anchor step of Single Anchor Phenomenology, linking the phi-ladder mass formula to the integrated anomalous dimension. It touches the open numerical verification that the RG integral matches this expression within 1e-6 tolerance.
scope and limits
- Does not evaluate the integrated anomalous dimension along any RG trajectory.
- Does not assert numerical equality to measured fermion masses.
- Does not apply to bosons or composite states.
- Does not encode the full RG flow equations or beta functions.
Lean usage
theorem anchorEquality (f : Fermion) : residueAtAnchor f = gap (ZOf f) := by rflformal statement (Lean)
86noncomputable def residueAtAnchor (f : Fermion) : ℝ := gap (ZOf f)
proof body
Definition body.
87