QuarkScoreCardCert
plain-language theorem explainer
QuarkScoreCardCert bundles the theorem-grade facts for the quark and lepton mass scorecard in Recognition Science. A physicist working on the mass ladder would cite this record to confirm that up-type quarks share ZOf=276, down-type share 24, leptons share 1332, and that the structural predictions satisfy charm/up = phi^11 and top/charm = phi^6 with top in the 10^4 to 10^6 range. The structure is assembled directly from prior lemmas on ZOf and the phi-power ratios without additional proof steps.
Claim. The certificate records that $ZOf(u)=ZOf(c)=ZOf(t)=276$, $ZOf(d)=ZOf(s)=ZOf(b)=24$, $ZOf(e)=ZOf(μ)=ZOf(τ)=1332$; the ratio of charm-quark to up-quark structural predictions equals $φ^{11}$; the top-quark to charm-quark ratio equals $φ^6$; the top-quark prediction lies in $(10^4,10^6)$; all three up-quark predictions are positive; and the relative errors of the $rs_mass_MeV$ predictions versus experimental values satisfy $|rs_mass_MeV(e)-m_e^{exp}|/m_e^{exp}<0.003$, $|rs_mass_MeV(μ)-m_μ^{exp}|/m_μ^{exp}<0.04$ and $|rs_mass_MeV(τ)-m_τ^{exp}|/m_τ^{exp}<0.03$.
background
In the Quark Score Card module the structure collects Phase 0 deliverables from the physical derivation plan. ZOf(f) is defined in RSBridge.Anchor as 4 + q² + q⁴ for up/down sectors where q = tildeQ(f), and simply q² + q⁴ for leptons. The phi-ladder mass formula appears in Verification via charm_quark_pred = phi^{45}/2e6 and similar for other rungs. The module consolidates existing proofs that equal-Z fermions have anchor mass ratios that are pure phi-powers of the rung difference. Upstream lemmas establish the specific ZOf numbers for each generation and the ratio equalities row_charm_up_ratio and row_top_charm_ratio. QuarkAbsoluteMassResidual names the missing bridge that would equate the structural rs_mass_MeV formula to the gap-corrected massAtAnchor expression.
proof idea
The declaration is a structure definition with no proof body. It is populated by the theorem quarkScoreCardCert_holds which constructs an instance using the lemmas ZOf_up_quarks, ZOf_down_quarks, ZOf_charged_leptons, row_charm_up_ratio, row_top_charm_ratio, row_top_quark_in_band and the three lepton percentage checks.
why it matters
This certificate closes the Phase 0 quark scorecard row by recording all currently theorem-grade facts in one place. It feeds the theorem quarkScoreCardCert_holds that asserts the structure is inhabited. In the Recognition framework it confirms the self-similar phi-power relations forced by T6 and the eight-tick octave structure, while leaving open the absolute mass match that requires the gap(ZOf) correction from the RSBridge.Anchor massAtAnchor formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.