Z_up
plain-language theorem explainer
The up quark receives anchor index 276 from the ZOf function in the Recognition Science fermion sector mapping. Researchers constructing the phi-ladder mass spectrum for Standard Model fermions cite this index to locate the up quark rung. The result follows from direct evaluation of the quadratic and quartic terms in the up-sector formula for ZOf.
Claim. Let $Z(f)$ be the integer anchor index for fermion $f$ given by $Z(f)=4+q^2+q^4$ in the up sector, where $q=tilde{Q}(f)$. Then $Z(u)=276$ for the up quark $u$.
background
The Single-Anchor RG Policy module supplies a Lean interface for single-anchor phenomenology in the mass framework. It reuses the Fermion inductive type and the ZOf definition from RSBridge.Anchor, where ZOf(f) equals 4 plus q squared plus q to the fourth for up or down quarks, q squared plus q to the fourth for leptons, and zero for neutrinos. The module wires this index to the gap function F(Z) and isolates hypotheses on anchor scale and stability for downstream mass formulas.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the ZOf definition on the up quark constructor.
why it matters
This supplies the concrete Z value for the up quark, enabling its placement on the phi-ladder via the mass formula yardstick times phi to the power (rung minus 8 plus gap(Z)). It supports the single-anchor phenomenology in the module documentation and connects to the Recognition Composition Law and eight-tick octave. No downstream uses appear yet, leaving open its integration with RG transport residues.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.