quarkScoreCardCert_holds
plain-language theorem explainer
The theorem asserts the existence of a QuarkScoreCardCert structure that bundles verified ZOf assignments for up-type quarks at 276, down-type at 24, and charged leptons at 1332, together with exact phi-power mass ratios for charm/up and top/charm. Researchers deriving discrete fermion masses from the Recognition Science phi-ladder would cite it to confirm generation structure and ratio predictions. The proof is a direct term-mode construction that assembles the certificate from sibling lemmas on ZOf values, ratio equalities, and positivity/ban
Claim. There exists a structure certifying that up-type quarks (u, c, t) share ZOf = 276, down-type quarks (d, s, b) share ZOf = 24, charged leptons share ZOf = 1332, the charm-to-up mass prediction ratio equals φ¹¹, and the top-to-charm ratio equals φ⁶.
background
The QuarkScoreCardCert structure records theorem-grade results on fermion ZOf assignments and mass ratios derived from the phi-ladder in the Recognition Science framework. The module consolidates Phase 0 facts from the physical derivation plan, including that equal-Z fermions have anchor mass ratios that are pure phi-powers of the rung difference. Upstream results include PhiForcingDerived.of for J-cost structures and LedgerFactorization.of for calibration of the recognition function J.
proof idea
The proof is a term-mode construction that directly instantiates the QuarkScoreCardCert record by supplying ZOf_up from ZOf_up_quarks, ZOf_down from ZOf_down_quarks, ZOf_lep from ZOf_charged_leptons, charm_up_ratio_eq from row_charm_up_ratio, top_charm_ratio_eq from row_top_charm_ratio, and the remaining positivity and band predicates from their respective row lemmas.
why it matters
This theorem consolidates the verified entries in the quark scorecard, feeding into broader mass predictions on the phi-ladder. It supports the framework claim that equal-Z fermions have anchor mass ratios as pure phi-powers, aligning with T6 (phi as self-similar fixed point) and the mass formula yardstick * phi^(rung - 8 + gap(Z)). It touches the open question of absolute mass matches pending the RSBridge.Anchor bridge equivalence between rs_mass_MeV and massAtAnchor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.