massRatio_31_canonical
plain-language theorem explainer
The theorem states that the mass ratio between third-generation and first-generation fermions equals φ to the power 17 whenever the ledger carries the canonical generation torsion offsets. Physicists working on Recognition Science mass derivations cite this to fix the φ-ladder spacing for the three generations. The proof is a short term reduction that unfolds the rung-based mass ratio, rewrites via the canonical rung-difference lemma, and simplifies the torsion offset.
Claim. Let $L$ be a rich ledger whose generation torsion equals the canonical values derived from $D=3$ cube geometry. For any real number $φ$ and any fermion sector, the mass ratio between the third and first generations equals $φ^{17}$.
background
The module introduces the rich ledger structure that augments a minimal ledger with generation torsion offsets and sector base rungs. Torsion values are {0, 11, 17} for generations 1, 2, 3; these arise from cube combinatorics in three dimensions (edge and face contributions). Fermion sectors are leptons (base rung 2), up quarks (base 4), and down quarks (base 4). Mass ratios are then obtained directly from rung differences via the φ-ladder formula $m_f / m_g = φ^{r_f - r_g}$.
proof idea
The proof is a term-mode one-liner. It unfolds the mass-ratio-from-rungs definition, rewrites the rung difference using the canonical rung-difference lemma on the ledger (with the supplied torsion hypothesis), and simplifies the torsion difference to obtain the exponent 17.
why it matters
This lemma supplies one of the three canonical inter-generation ratios that feed the mass-ratios-from-tiers theorem. It realizes the Recognition Science mass formula on the φ-ladder with torsion offsets taken from D=3 cube geometry, completing the step from ledger structure to explicit φ-power ratios {φ^{11}, φ^{17}, φ^6}. The result is invoked inside the canonical mass-ratios theorem and the specialized canonical-mass-ratio-31 wrapper.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.