up_Z_is_276
plain-language theorem explainer
The theorem asserts that the residue index ZOf for the up quark equals 276. Researchers auditing the Recognition Science mass ladder would cite this certificate to validate the up-sector rung assignment against experimental transport. The proof reduces to native evaluation of the sector formula for the up fermion.
Claim. Let $Z_{Of}$ be the residue function on fermions defined by $Z_{Of}(f) = 4 + q^2 + q^4$ where $q = tilde{Q}(f)$ for up-sector fermions. Then $Z_{Of}(u) = 276$, where $u$ is the up quark.
background
The module ResidueData supplies numerical certificates for the residues of fermions at the anchor scale. These verify the axiom display_identity_at_anchor from AnchorPolicy by bounding gap(Z) for each particle. The function ZOf, defined identically in both Masses.RSBridge.Anchor and RSBridge.Anchor, computes the residue index from the tilde charge: for up or down sector it is 4 + q² + q⁴, for leptons q² + q⁴, and zero for neutrinos.
proof idea
The proof is a direct native_decide tactic that evaluates the definition of ZOf on the up fermion u and confirms the integer result 276.
why it matters
This declaration forms part of the audit payload that quantifies the Quarter-Ladder vs Integer-Rung gap in the Recognition Science framework. It contributes to the residue data used to check consistency with the phi-ladder mass formula and the theoretical F(Z) targets. The module notes that up and top residues differ from each other and from the target F(276) ≈ 10.7, highlighting tension in the model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.