tau_muon_ratio
plain-language theorem explainer
The theorem establishes that the RS-unit tau mass divided by the RS-unit muon mass equals phi to the sixth power. Physicists deriving lepton mass hierarchies from the phi-ladder would cite this to confirm the fixed rung spacing in the lepton sector. The proof is a term-mode algebraic reduction that unfolds the mass definitions and simplifies the exponent difference via field operations and norm_num.
Claim. $m_τ / m_μ = φ^6$ where the masses are the RS-unit values placed on the phi-ladder at rungs differing by six (m_τ at rung 19, m_μ at rung 13).
background
The module formalizes P-011: lepton masses from the phi-ladder, with m_e ∝ φ^2, m_μ ∝ φ^13, m_τ ∝ φ^19 in E_coh units. Ratios follow directly: m_μ/m_e = φ^11, m_τ/m_e = φ^17, hence m_τ/m_μ = φ^6. Upstream, mass_on_rung places particles on the ladder (as in m_e := mass_on_rung 2), phi_ne_zero justifies division, and the local setting derives from the Recognition Composition Law with phi as the self-similar fixed point from the forcing chain.
proof idea
Unfolds m_tau_rs and m_mu_rs to their mass_on_rung expressions, applies field_simp with phi_ne_zero to clear denominators, rewrites the power difference via Real.zpow_sub, and normalizes to obtain the exact exponent 6.
why it matters
Supplies the third conjunct of lepton_masses_from_ladder, which resolves P-011 by showing lepton masses follow from phi-ladder rungs with ratios fixed by cube geometry (spacing 11 and 17). It anchors the lepton sector in the RS framework, consistent with T6 (phi fixed point) and T7 (eight-tick octave). No open scaffolding is touched.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.