canonical_massRatio_21
plain-language theorem explainer
The theorem asserts that the second-to-first generation fermion mass ratio equals φ to the eleventh power in the canonical RS ledger, for any real φ and any sector. Researchers deriving discrete mass hierarchies from geometric torsion offsets would cite it. The proof is a one-line wrapper that specializes the general massRatio_21_canonical result to the canonical ledger via its torsion equality.
Claim. For any real number $φ$ and any fermion sector $S$, the mass ratio between second and first generations computed via rung differences in the canonical ledger equals $φ^{11}$.
background
The RSLedger encodes masses on the φ-ladder with rung = baseRung + τ_g. The canonical ledger sets torsion to generationTorsion (offsets 0, 11, 17) and baseRung to sectorBaseRung (2 for leptons, 4 for quarks). The massRatioFromRungs definition returns φ raised to the rung difference between two generations. The upstream massRatio_21_canonical theorem states that whenever a ledger's torsion equals generationTorsion the second-to-first ratio is exactly φ^{11}.
proof idea
This is a one-line wrapper that applies massRatio_21_canonical to canonicalRSLedger, supplying canonicalRSLedger_torsion as the required hypothesis that the ledger torsion matches generationTorsion.
why it matters
This supplies the explicit Gen 2 / Gen 1 ratio φ^{11} required by the RSLedger construction. It instantiates the rung-difference formula for the canonical torsion case, closing the derivation of inter-generation hierarchies from D=3 cube geometry. The module states that with torsions {0, 11, 17} the ratios are φ^{11}, φ^{17}, φ^6.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.