Mass Spectrum on the Phi-Ladder

1. Setting

The RS mass law is the page every particle-physics reader needs first. Instead of 13 or more free Yukawa parameters, RS uses a yardstick, a rung, and a Z-dependent gap correction. The Lean theorem mass_rung_scaling proves the phi-power scaling law, while predict_mass_pos proves the spectrum stays positive. The empirical work is the assignment of electron, muon, tau, quark, neutrino, and boson masses to the correct rung plus gap.

2. Equations

(E1)

$$ m = m_0,\varphi^{,r-8+\mathrm{gap}(Z)} $$

Canonical RS mass law.

(E2)

$$ \frac{m_{r+1}}{m_r}=\varphi $$

Rung-to-rung scaling in the neutral-gap limit.

3. Prediction or structural target

• Mass positivity: predicted m > 0 for every assigned rung (mass); empirical All observed particle masses are positive. Source: PDG 2024
• Lepton ladder: predicted electron/muon/tau on phi-spaced rungs (MeV); empirical 0.511, 105.658, 1776.93. Source: CODATA / PDG

The existing Standard-Model masses are the empirical target set. The strongest checks are the dimensionless ratios, not SI mass units.

4. Formal anchor

The primary anchor is Masses.MassLaw..predict_mass.

    Predicts the mass of a species in a given sector. -/
noncomputable def predict_mass (sector : Sector) (rung : ℤ) (Z_val : ℤ) : ℝ :=
  yardstick sector * (phi ^ ((rung : ℝ) - 8 + gap_correction Z_val))

/-- Mass is positive for any valid configuration. -/
theorem predict_mass_pos (s : Sector) (r : ℤ) (Z_val : ℤ) :
    predict_mass s r Z_val > 0 := by
  unfold predict_mass
  apply mul_pos
  · -- yardstick is positive

5. What is inside the Lean module

Key theorems:

• predict_mass_pos
• mass_rung_scaling
• gap_zero_neutral

Key definitions:

• gap_correction
• predict_mass

6. Derivation chain

• predict_mass - Mass-law definition
• predict_mass_pos - Mass positivity
• mass_rung_scaling - Mass rung scaling
• gap_zero_neutral - Gap-zero neutrality

7. Falsifier

A stable elementary particle whose measured mass cannot be assigned to any phi-ladder rung within the RS gap window refutes the mass law. A fourth charged-lepton family would also force a new rung assignment and falsify the current finite-spectrum closure.

8. Where this derivation stops

Below this page the chain reduces to the RS forcing sequence: J-cost uniqueness, phi forcing, the eight-tick cycle, and the D=3 recognition substrate. If any upstream theorem changes, this page must be versioned rather than patched silently. The published URL is stable, but the version field is the contract.

10. Audit path

To audit mass-law-phi-ladder, start with the primary Lean anchor Masses.MassLaw.predict_mass. Then inspect the theorem names listed in the module-content section. The page is intentionally built so the public explanation is not a substitute for the proof object; it is a map into it. The mathematical dependency is the same in every case: reciprocal cost fixes J, J fixes the phi-ladder, the eight-tick cycle fixes the recognition clock, and the domain theorem listed above supplies the last step. If that last step is empirical, the falsifier section names what observation would break it. If that last step is formal, a Lean-checkable counterexample is the relevant failure mode.