charm_up_equal_Z
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 in Recognition Science
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.
scope and limits
- Does not compute numerical masses in MeV.
- Does not include the gap(ZOf) correction term.
- Does not address down-type quarks or leptons.
- Does not prove the phi-power mass ratio itself.
formal statement (Lean)
58theorem charm_up_equal_Z : ZOf .u = ZOf .c := by
proof body
Term-mode proof.
59 obtain ⟨hu, hc, _⟩ := ZOf_up_quarks
60 rw [hu, hc]
61