top_up_equal_Z
plain-language theorem explainer
The declaration establishes that the recognition integer Z assigned to the up quark equals the value assigned to the top quark. Researchers consolidating the Recognition Science quark mass scorecard would cite it when grouping equal-Z fermions. The proof is a one-line wrapper that extracts the common value 276 from the upstream triple equality for up, charm and top quarks and substitutes directly.
Claim. Let $Z(f)$ be the recognition integer for fermion $f$ given by $Z(f)=4+q^2+q^4$ with $q=tilde{Q}(f)$ in the up sector. Then $Z(u)=Z(t)$.
background
The Quark Score Card module consolidates existing proofs for the quark sector and records which facts are theorem-grade. It states that u, c, t share the recognition integer ZOf=276 and that equal-Z fermions have anchor mass ratios given by pure phi-powers of the rung difference. The definition of ZOf appears in RSBridge.Anchor: for up-sector fermions it evaluates to 4 + qq + qqqq where q=tildeQ(f). The upstream theorem ZOf_up_quarks supplies the explicit triple Z(u)=Z(c)=Z(t)=276 by direct computation.
proof idea
The proof applies the upstream theorem ZOf_up_quarks to obtain the conjunction of three equalities, then rewrites using the first and third components to conclude the desired equality.
why it matters
This result supports the scorecard claim that u/c/t share ZOf=276, which underpins the statement that equal-Z fermions possess anchor mass ratios that are pure phi-powers of rung difference. It contributes to the Recognition framework mass formula (yardstick times phi to the power rung-8+gap(Z)) and the eight-tick octave structure. The module notes the remaining open question of absolute mass match within PDG bands, since the rs_mass_MeV formula still lacks the gap(ZOf f) correction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.