residueAtAnchor
plain-language theorem explainer
The definition residueAtAnchor assigns to each Standard Model fermion its closed-form RG residue at the anchor scale by composing the Z-index map with the gap display function. Researchers modeling fermion mass spectra via RG flow would reference this when stating the equality between integrated anomalous dimensions and the phi-based gap. It is realized as the direct substitution of gap applied to ZOf f.
Claim. For a fermion species $f$, the residue at the anchor is $F(Z(f))$, where $Z(f)$ is the charge-indexed integer (4 + $q^2$ + $q^4$ for quarks, $q^2$ + $q^4$ for charged leptons, and 0 for neutrinos) and $F(Z) = (1/2) (Z / phi) / ln phi$ wait, precisely $F(Z) = ln(1 + Z/phi) / ln phi$.
background
The RSBridge.Anchor module defines the bridge from the recognition framework to Standard Model fermions. Fermion is the inductive type enumerating the twelve species (six quarks, three charged leptons, three neutrinos). ZOf extracts the integer index Z_i from the tilde charge q and sector: quarks receive an extra +4, leptons use q^2 + q^4, and neutrinos map to zero. The gap function then supplies the display F(Z) = ln(1 + Z/phi) / ln phi, which the module doc states is the closed form that the integrated RG residue is claimed to equal at the anchor scale mu star.
proof idea
One-line wrapper that applies gap to the result of ZOf f.
why it matters
This definition supplies the closed-form target that anchorClaimHolds in Physics.RGTransport compares against the integrated anomalous dimension, and that mass_ratio_phi_power converts into phi-power mass ratios. It realizes the gap display from Gap45.Derivation inside the fermion sector, directly supporting the Single Anchor Phenomenology claim that f_residue f mu star equals residueAtAnchor f (verified numerically). The construction ties the phi-ladder mass formula to the eight-tick octave and D=3 spatial dimensions via the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.