canonical_massRatiosFromTiers
plain-language theorem explainer
The result shows that the tier-derived lepton mass ratios from the standard recognition ledger equal the golden-ratio powers φ to the 11, 17 and 6. Researchers constructing lepton spectra inside the Recognition Science ledger framework would cite this to fix the canonical generation gaps. The proof is a direct one-line specialization of the general mass-ratios-from-tiers theorem to the canonical ledger instance.
Claim. Let $L$ be the canonical recognition ledger with torsion differences generated by cube geometry. Then the lepton mass ratios computed from its tier structure satisfy $m_μ/m_e = φ^{11}$, $m_τ/m_e = φ^{17}$, and $m_τ/m_μ = φ^6$.
background
The module derives the canonical LeptonMassRatios payload directly from the tier structure of an RSLedger. The ledger carries a torsion field and base rungs; mass ratios are obtained by applying massRatioFromRungs to the rung differences between lepton generations. Canonical semantics fix the payload as the triple {φ^{11}, φ^{17}, φ^6} corresponding to the torsion set {0, 11, 17}.
proof idea
One-line wrapper that applies the general massRatiosFromTiers_canonical theorem to the canonical ledger together with the equality of its torsion field to the generation torsion set.
why it matters
The declaration supplies the concrete canonical instance required by the mass-law-from-ledger construction. It confirms that the torsion differences forced by cube geometry translate into the expected φ-powers on the lepton ladder. The parent result is the general massRatiosFromTiers_canonical theorem; the step closes the canonical semantics paragraph in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.