mass_rung_scaling
plain-language theorem explainer
Recognition Science mass predictions scale exactly by the golden ratio φ when the rung index increases by one. Model builders checking fermion mass hierarchies or Yukawa couplings in the Standard Model would invoke this relation. The short tactic proof reduces the claim to exponent arithmetic on the real power function after unfolding the predict_mass definition and establishing additivity of the rung exponent.
Claim. For any sector $s$, rung integer $r$, and charge index $Z$, the predicted mass at rung $r+1$ equals $φ$ times the predicted mass at rung $r$, where the mass is given by the master formula yardstick$(s) · φ^{r-8 + gap(Z)}$.
background
The master mass law states that every stable recognition state occupies a rung on the φ-ladder with mass $m = $ yardstick(Sector) $· φ^{r-8 + gap(Z)}$. Sector is the inductive type with constructors Lepton, UpQuark, DownQuark, Electroweak. The gap term is supplied by gap_correction, which encodes the D=3 integration gap of 45 together with the fine-structure correction 1 + 45/(360·137). The function predict_mass applies the yardstick prefactor for the chosen sector and evaluates the indicated real power of φ.
proof idea
The tactic proof unfolds predict_mass, introduces the gap value via gap_correction, proves the exponent identity ((r+1)-8+gap) = 1 + (r-8+gap) by push_cast and ring, rewrites with Real.rpow_add using phi_pos, reduces the extra factor via Real.rpow_one, and finishes with ring.
why it matters
This theorem supplies the φ-scaling step required by sm_verification_cert and by the Yukawa scaling theorem yukawa_SM_phi_scaling. It realizes the self-similar fixed-point property (T6) inside the mass sector and closes one link in the eight-tick octave structure (T7). No open scaffolding remains for this particular scaling claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.