massRatiosFromTiers
plain-language theorem explainer
The definition assembles the lepton mass ratio triple from any recognition ledger by invoking the rung-difference ratio extractor on the lepton sector for the fixed tier pairs. A physicist deriving generation mass hierarchies from ledger torsion in Recognition Science would cite it to obtain the phi-powered ratios without embedding the exponents. The body is a direct record constructor that applies the rung ratio function three times.
Claim. Let $L$ be a recognition ledger and $φ$ a real number. The lepton mass ratios are the triple $⟨ρ_{21}, ρ_{31}, ρ_{32}⟩$, where each $ρ_{ij}$ is the mass ratio obtained from the rung difference between lepton tiers $i$ and $j$ via the ledger ratio function scaled by powers of $φ$.
background
An RSLedger encodes generation structure through its torsion set. For leptons the canonical torsion is {0, 11, 17}, so the rung gaps are 11, 17 and 6. The rung ratio function converts any such gap into the corresponding power of $φ$ that sets the mass ratio. LeptonMassRatios is the record packaging the three inter-generation ratios (mu/e, tau/e, tau/mu). This module derives those ratios directly from ledger tier structure rather than postulating the exponents. The local setting is the derivation of the mass law from ledger tiers, with canonical semantics massRatios = {mu_over_e := $φ^{11}$, tau_over_e := $φ^{17}$, tau_over_mu := $φ^{6}$}.
proof idea
The definition is a one-line wrapper that applies the rung ratio function to the lepton sector for the three tier pairs (second-first, third-first, third-second) and packages the results into the LeptonMassRatios record.
why it matters
This definition supplies the mass-ratio payload that the downstream canonical theorems equate to the explicit $φ$ powers 11, 17 and 6. It realizes the mass formula step of the Recognition chain by converting ledger torsion gaps into observable lepton mass hierarchies. The gaps trace to the eight-tick octave and three-dimensional geometry in the forcing chain. It closes the link between the abstract ledger and the concrete ratios used throughout the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.