ZOf
plain-language theorem explainer
ZOf maps each of the twelve Standard Model fermions to an integer Z built from its reduced charge index q̃. Mass-ratio derivations in the Recognition framework cite this map when placing a species on the phi-ladder at the anchor scale. The definition is a direct case split on sectorOf f that adds the constant 4 only for quarks and returns zero for neutrinos.
Claim. For a fermion $f$ with reduced charge index $q̃$, define $Z(f) = 4 + q̃^2 + q̃^4$ when $f$ is a quark, $Z(f) = q̃^2 + q̃^4$ when $f$ is a charged lepton, and $Z(f) = 0$ when $f$ is a neutrino.
background
The RSBridge.Anchor module supplies the interface between the recognition framework and the Standard Model fermion spectrum. Fermion is the inductive type that enumerates the six quarks, three charged leptons and three neutrinos. ZOf computes the integer label Z_i that enters the gap function F(Z) = ln(1 + Z/φ)/ln(φ) at the anchor scale μ⋆, where this F is the closed form claimed to equal the integrated RG residue f_i(μ⋆).
proof idea
The definition performs a direct case split on the sector returned by sectorOf f. For up and down sectors it adds the constant 4 to the quadratic and quartic terms in tildeQ f; for leptons it omits the constant; for neutrinos it returns zero. No lemmas are invoked; the expression is the explicit closed form.
why it matters
ZOf supplies the discrete index that appears in every anchor mass ratio and in the mass formula yardstick * φ^(rung - 8 + gap(Z)). It is invoked by the anchor_ratio theorem and by the Z_eq equalities in QuarkAnchorDerivation, thereby linking the eight-tick octave (T7) and the phi-ladder to the observed quark and lepton spectrum. The definition closes the structural step that converts equal-Z species into pure φ-powers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.