quark_preds_pos
plain-language theorem explainer
All structural mass predictions for the up, charm, and top quarks are strictly positive. Mass verification code in the RS framework cites this to confirm signs on the phi-ladder before gap corrections or scorecard assembly. The term proof unfolds the three predicates and applies div_pos three times to powers of the positive golden-ratio constant.
Claim. $0 < m_u^pred ∧ 0 < m_c^pred ∧ 0 < m_t^pred$, where each $m^pred$ is the structural prediction obtained from the RS mass formula on the up-quark sector.
background
The Masses.Verification module supplies machine-checked comparisons of RS structural predictions against PDG values. Predictions are built from the phi-ladder mass formula (yardstick scaled by phi to an integer power involving rung and gap), with rung and gap supplied by AnchorPolicy and Gap45.Derivation. Constants.phi_pos asserts that the golden ratio is positive, which is the only non-trivial fact required here.
proof idea
Term-mode proof that unfolds up_quark_pred, charm_quark_pred and top_quark_pred, then builds the conjunction via three applications of div_pos (pow_pos Constants.phi_pos _) (by norm_num).
why it matters
Feeds directly into QuarkScoreCardCert and the derived row_quark_preds_pos theorem, closing the positivity check required for the absolute-mass rows of the quark scorecard. It supplies the sign guarantee that lets downstream statements such as charm_up_ratio_eq and top_charm_ratio_eq be stated without additional hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.