row_quark_preds_pos
plain-language theorem explainer
All structural mass predictions for the up, charm, and top quarks are strictly positive. Researchers auditing the Recognition Science quark mass ladder or scorecard would cite this when confirming the phi-ladder outputs remain positive. The proof is a direct one-line application of the positivity lemma already established in the Verification module.
Claim. $0 < u$-quark prediction, $0 < c$-quark prediction, and $0 < t$-quark prediction.
background
The Quark Score Card module consolidates existing theorem-grade facts for the quark sector without introducing new physics. It records that charm/up equals phi^11, top/charm equals phi^6, all quark predictions are positive, and equal-Z fermions share pure phi-power anchor ratios. The local setting is phase 0 of the physical derivation plan, with zero sorry or axiom in the module. Upstream, the result rests on the positivity statement in Verification together with the J-cost structure from PhiForcingDerived and the ledger factorization from DAlembert.
proof idea
The proof is a one-line wrapper that applies the quark positivity result from the Verification module.
why it matters
This declaration feeds directly into the quarkScoreCardCert_holds theorem that assembles the full scorecard certificate. It supports the framework claim that quark masses occupy the phi-ladder with positive values, consistent with the T5 J-uniqueness, T6 phi fixed point, and T7 eight-tick octave. It touches the open question of absolute mass matching within PDG bands, which still requires the gap(ZOf) correction from the RSBridge.Anchor mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.