massRatiosFromTiers_canonical
plain-language theorem explainer
massRatiosFromTiers_canonical shows that any RSLedger whose torsion matches the generation set {0,11,17} yields lepton mass ratios exactly equal to the triple of phi-powers 11, 17 and 6. Workers deriving observable lepton hierarchies from Recognition ledger structure cite the result to obtain the explicit canonical payload. The term proof unfolds the general tier-derived definition and rewrites each ratio component via the three specialized canonical lemmas.
Claim. Let $L$ be an RSLedger whose torsion equals generationTorsion. Then the lepton mass ratios obtained from the tier differences of $L$ equal the triple consisting of the golden ratio raised to the 11th, 17th and 6th powers: $L$ produces mass ratios $mu/e = phi^{11}$, $tau/e = phi^{17}$, $tau/mu = phi^{6}$.
background
The module MassLawFromLedger derives the LeptonMassRatios payload directly from the tier structure of an RSLedger. The canonical semantics fix the three inter-generation lepton ratios as phi to the 11, 17 and 6, arising from the torsion differences {0,11,17} forced by cube geometry. The supporting definition massRatiosFromTiers computes these ratios by calling massRatioFromRungs on the lepton sector for the rung pairs second-first, third-first and third-second.
proof idea
The term proof first applies simp to unfold massRatiosFromTiers into its three massRatioFromRungs components. It then rewrites each component by invoking the three canonical lemmas massRatio_21_canonical, massRatio_31_canonical and massRatio_32_canonical, all specialized to the leptons sector and supplied with the torsion hypothesis hL.
why it matters
The theorem supplies the explicit phi-power values needed by canonical_massRatiosFromTiers to instantiate the payload on the canonical ledger and by massRatiosFromTiers_pos to prove positivity for phi > 0. It completes the step that converts the ledger torsion set {0,11,17} into the concrete lepton mass hierarchy inside the Recognition framework, consistent with the phi-ladder construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.