lepton_hierarchy_geometric
plain-language theorem explainer
The declaration establishes that the muon-to-electron mass ratio equals phi to the 11th power while the tau-to-muon ratio equals phi to the 6th, with masses taken from the phi-ladder rung formula. Physicists studying fermion hierarchies in Recognition Science cite the result to replace Yukawa couplings with deterministic rung spacings. The term-mode proof unfolds the rung assignments and mass formula then cancels common phi-powers via field simplification after invoking that phi is nonzero.
Claim. Let $m_e$, $m_μ$, and $m_τ$ be the masses of the electron, muon, and tau obtained from the rung formula on the φ-ladder. Then $m_μ / m_e = φ^{11}$ and $m_τ / m_μ = φ^6$.
background
The module formalizes P-002 on the fermion mass hierarchy. Each fermion occupies a rung on the φ-ladder with mass proportional to φ raised to the rung integer. The rung map r_lepton assigns the electron to rung 2, the muon to rung 13, and the tau to rung 19. These values arise from the generation torsion tau, where tau(1) = 11 and tau(2) = 17, taken from cube geometry in the Anchor module.
proof idea
The term proof first applies simp to expand mass_on_rung together with the concrete rung values for the electron, muon, and tau. It then records that the coherence energy factor is nonzero using phi_ne_zero, splits the conjunction with constructor, and finishes both goals with field_simp to cancel the nonzero powers of phi.
why it matters
This supplies the explicit ratios required by mass_ratio_geometric in HierarchyDissolution, which resolves P-013 by dissolving the hierarchy into geometry. It thereby closes P-002 in the Recognition framework: mass ratios follow directly from rung spacings on the φ-ladder with no free Yukawa parameters. The construction rests on the self-similar fixed point phi forced at T6.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.