predict_mass_pos
plain-language theorem explainer
The theorem establishes that the mass predicted by the master formula remains strictly positive for every sector, rung integer, and charge index. Particle physicists verifying fermion spectra in the Recognition Science framework would cite this when confirming all computed masses stay positive. The proof proceeds by unfolding the mass expression into a product of positive factors and invoking positivity of multiplication together with real powers of the golden ratio.
Claim. For any sector $S$, integer rung $r$, and charge index $Z$, the predicted mass $m(S,r,Z) = $ yardstick$(S) · φ^{r-8+gap(Z)} > 0$.
background
The master mass law states that every stable recognition state occupies a rung on the φ-ladder, with mass proportional to coherence energy scaled by sector yardstick and rung position: $m = $ yardstick$(Sector) · φ^{r-8+gap(Z)}$. Yardstick$(S)$ is the sector prefactor built from binary powers and φ-offsets. B_pow supplies the derived powers of two for each sector, obtained from cube edge counting. r0 supplies the sector-specific offset exponent. The local setting is the mass formula module, which formalizes the formula derived from first principles in Recognition Science.
proof idea
The term proof unfolds predict_mass, then applies mul_pos to separate the yardstick factor from the remaining φ power. It invokes zpow_pos on the positive bases given by B_pow and φ (with exponent -5), followed by zpow_pos on φ with exponent r0, and finally Real.rpow_pos_of_pos on the remaining real exponent.
why it matters
This result supplies the positivity step required by the downstream theorems all_fermion_masses_pos, electron_mass_pos, and the other specific fermion mass positivity statements in SMVerification. It closes the positivity requirement inside the master mass law, which rests on the φ-ladder construction and the eight-tick octave from the forcing chain. No open scaffolding remains in this declaration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.