Z_up
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not derive the ZOf formula from the forcing chain T0-T8.
- Does not incorporate radiative corrections or anomalous dimensions.
- Does not compute a physical mass value, only the discrete index.
- Does not address flavor mixing or neutrino sectors.
formal statement (Lean)
107theorem Z_up : ZOf Fermion.u = 276 := by native_decide