massRatioFromRungs
plain-language theorem explainer
The definition computes the mass ratio between two fermion generations in a given sector as φ raised to the rung difference stored in the RSLedger. Researchers deriving fermion mass hierarchies from Recognition Science geometry cite this when converting torsion offsets into observable ratios. It is realized as a direct one-line definition that applies exponentiation to the precomputed rung difference.
Claim. Let $L$ be an RSLedger, let $φ$ be a real number, let $s$ be a fermion sector, and let $g_1$, $g_2$ be generations. The mass ratio between generations $g_2$ and $g_1$ in sector $s$ is $φ$ raised to the power of the rung difference between $g_1$ and $g_2$ in $L$.
background
In Recognition Science, particle masses occupy discrete rungs on the φ-ladder. The RSLedger extends the minimal ledger with a generation torsion function and base rungs for each fermion sector (leptons, up quarks, down quarks). The full rung for a particle is baseRung(sector) plus torsion(generation), so the mass ratio between generations is φ to the power of their rung difference.
proof idea
This is a one-line definition that returns φ raised to the power of the rung difference computed by L.rungDiff for the given sector and generations.
why it matters
This definition supplies the core ratio extractor used by massRatiosFromTiers to populate lepton mass ratios and by the canonical theorems canonical_massRatio_21, canonical_massRatio_31, and canonical_massRatio_32 to establish the specific powers 11, 17, and 6. It realizes the mass formula on the φ-ladder within the Recognition framework, where ratios eliminate the overall scale and depend only on the torsion differences {0,11,17} from the D=3 cube combinatorics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.