quark_mass_positive
plain-language theorem explainer
The theorem proves that the Recognition Science mass formula yields a strictly positive value in MeV for every quark sector and integer rung. Researchers checking consistency of the phi-ladder spectrum for up and down quarks would cite this result. The proof is a term-mode construction that unfolds the mass expression and chains the lemmas div_pos and mul_pos with zpow_pos on positive bases.
Claim. For every quark sector $s$ and integer rung $r$, the RS-computed mass $m(s,r)$ in MeV satisfies $m(s,r)>0$, where $m(s,r)$ is the explicit phi-ladder expression (phi to a sector-dependent power scaled by a power of 2 and divided by $10^6$).
background
The module treats experimental PDG values as imported constants while the RS mass function rs_mass_MeV encodes the phi-ladder formulas: up sector gives phi to the (30+r) over (2 times 10^6) MeV; down sector gives 2 to the 23 times phi to the (r-10) over 10^6 MeV. Sector is the type distinguishing these two cases, with rungs drawn from the discrete ladder anchored at specific integers. Upstream, Constants.phi_pos supplies the positivity of the golden ratio phi that appears in every power.
proof idea
The term proof first unfolds rs_mass_MeV to expose the quotient of a product of powers. It applies div_pos, reducing the goal to positivity of the numerator product and the constant denominator. The denominator is immediate by norm_num. The numerator is discharged by three nested mul_pos applications, each resolved by zpow_pos: one on base 2 via a norm_num fact and three on base phi via Constants.phi_pos.
why it matters
The result populates the all_masses_positive field inside the certificate constructed by quark_verification_cert_exists. It confirms that the phi-ladder mass formulas remain physically admissible across the quark rungs and sectors. The declaration supports the general mass formula landmark (yardstick times phi to a rung power) and the torsion-determined spacing {0,11,17} implicit in the generation structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.