anchorEquality
plain-language theorem explainer
The equality states that the anchor residue for any of the twelve Standard Model fermions equals the gap function evaluated at the fermion's charge-derived integer Z. Model builders comparing phi-ladder predictions to RG flow would cite the result when substituting the closed-form display into mass hierarchies. The proof is immediate reflexivity from the direct definition of the residue.
Claim. For every fermion species $f$, the anchor residue satisfies $r(f) = F(Z(f))$ where $F(Z) = (1/2) (Z/phi) / ln phi$ and $Z(f)$ is the integer $q^2 + q^4$ (plus offset 4 for quarks) built from the tilde charge of $f$.
background
The RSBridge.Anchor module supplies the interface between the recognition framework and the Standard Model fermion spectrum. It enumerates the twelve fermions (six quarks, three charged leptons, three neutrinos) and equips each with a charge-derived integer Z via the ZOf map, which incorporates the squared and fourth-power tilde charges plus an offset of 4 for quarks. The gap function, written F(Z), is the explicit logarithmic expression ln(1 + Z/phi) / ln(phi). This expression is asserted to equal the integrated mass anomalous dimension at the anchor scale mu star, as stated in the module documentation. Upstream results include the gap definition in AnchorPolicy that performs the same computation for a sector and name, and the Gap45 derivation that produces the integer 45 from closure and Fibonacci factors.
proof idea
The proof applies reflexivity. The residue at the anchor is introduced by the direct equation residue(f) := gap(ZOf(f)), so the stated equality holds by construction with no further steps required.
why it matters
The theorem supplies the definitional bridge required by the Single Anchor Phenomenology claim in the module documentation. It enables substitution of the gap expression into mass formulas and supports the anchor ratio property for equal-Z species. The result is used in the same module for further equalities and connects to the broader forcing chain through the phi-ladder structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.