ZOf
plain-language theorem explainer
ZOf maps each Standard Model fermion to an integer Z built from its charge index q̃ as q̃² + q̃⁴, with an extra +4 for quarks. Mass-hierarchy calculations cite it to evaluate the gap function that fixes the anchor-scale residue for each species. The definition is a direct case split on sector after extracting the charge index, returning a concrete integer for every named fermion.
Claim. Let $f$ be a fermion and let $q̃(f)$ be its charge index. Define $Z(f)$ by cases on the sector of $f$ as $Z(f) = 4 + q̃(f)^2 + q̃(f)^4$ for quarks, $Z(f) = q̃(f)^2 + q̃(f)^4$ for charged leptons, and $Z(f) = 0$ for neutrinos.
background
The RSBridge.Anchor module defines the Fermion inductive type that enumerates the twelve Standard Model species and introduces ZOf as the charge-indexed integer map. The companion gap function is the closed-form display $F(Z) = ln(1 + Z/φ)/ln(φ)$, asserted to equal the integrated mass anomalous dimension at the anchor scale μ⋆. The local setting is Single Anchor Phenomenology, which equates the RG residue integral to gap(ZOf i) with tolerance ~1e-6.
proof idea
The definition extracts q := tildeQ f and matches on sectorOf f, returning the appropriate quartic polynomial or zero. It is a pure computational definition with no lemma applications or tactics beyond the match expression.
why it matters
ZOf supplies the Z-values that anchor_ratio theorems in QuarkAbsoluteBridgeScoreCard convert into exact φ-power mass ratios for equal-Z species. It realizes the module claim that the integrated RG residue at μ⋆ equals gap(ZOf i), closing the bridge from the recognition forcing chain (T5 J-uniqueness to T8 D=3) to the observed fermion mass ladders.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.