charm_up_equal_Z
plain-language theorem explainer
The result establishes that the up and charm quarks carry identical ZOf labels of 276. Model builders checking generation spacing and anchor-mass ratios in the Recognition Science quark sector would cite the equality when confirming that equal-Z fermions differ only by phi-power rung steps. The proof extracts the relevant pair of equalities from the ZOf_up_quarks conjunction and substitutes them directly.
Claim. $Z(f_u) = Z(f_c)$ where $Z$ is the integer label $4 + q^2 + q^4$ for up-sector fermions and $q$ is the charge label of the fermion.
background
The Quark Score Card module records theorem-grade facts for the quark sector under phase 0 of the physical derivation plan. It consolidates existing results without introducing new physics and states that u/c/t share ZOf = 276 while d/s/b share ZOf = 24. The ZOf function is defined on fermions by sector: for up or down quarks it returns 4 plus the square plus the fourth power of the charge label q; the upstream ZOf_up_quarks theorem supplies the concrete value 276 for each of the three up-type quarks.
proof idea
The proof is a one-line wrapper that applies the ZOf_up_quarks theorem to obtain the triple of equalities, then rewrites the first two components to reach the desired equality between up and charm.
why it matters
The declaration supports the module-level claim that u/c/t share ZOf = 276 and therefore possess anchor-mass ratios given by pure phi-powers of their rung difference. It sits inside the equal-Z fermion theorem and the mass formula on the phi-ladder; the open question it touches is the absolute mass match within PDG bands once the gap(ZOf) correction from the RSBridge.Anchor bridge equivalence is supplied.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.