canonical_massRatio_31
plain-language theorem explainer
The declaration establishes that the mass ratio between third and first generation fermions equals φ to the power 17 for the canonical recognition ledger, independent of sector. Researchers computing generation mass hierarchies from the φ-ladder in Recognition Science would cite this result. The proof is a one-line wrapper that invokes the general massRatio_31_canonical theorem after supplying the canonical ledger and its torsion equality.
Claim. For the canonical recognition ledger, the mass ratio between third-generation and first-generation fermions in any sector equals $m_3/m_1 = φ^{17}$.
background
In the RSLedger module, fermion masses occupy discrete rungs on the φ-ladder. The rung for a given generation and sector is baseRung(sector) plus torsion(generation), where torsion values derive from D=3 cube combinatorics: τ₁=0, τ₂=11, τ₃=17. The canonicalRSLedger is defined with torsion equal to generationTorsion and baseRung equal to sectorBaseRung (2 for leptons, 4 for quarks). The upstream theorem massRatio_31_canonical states that whenever a ledger L satisfies L.torsion = generationTorsion, then massRatioFromRungs L φ sector .third .first equals φ^{17}. The definition massRatioFromRungs itself is φ raised to the rung difference between the two generations.
proof idea
One-line wrapper that applies massRatio_31_canonical to canonicalRSLedger, the real φ, the given sector, and the theorem canonicalRSLedger_torsion that confirms the ledger torsion equals generationTorsion.
why it matters
This result supplies the concrete Gen 3 / Gen 1 mass ratio φ^{17} stated in the module documentation, which follows directly from the torsion set {0,11,17} obtained via cube geometry in D=3. It closes the specialization of the general rung-difference formula to the canonical ledger used throughout Recognition Science mass derivations. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.