LeptonMassRatios
LeptonMassRatios packages the three dimensionless inter-generation lepton mass ratios into a single record. Physicists extracting observable predictions from Recognition Science ledgers cite it inside DimlessPack and UniversalDimless. The declaration is a bare structure definition that introduces three real-valued fields with no attached proof obligations.
claimA record whose fields are the muon-to-electron mass ratio $m_μ/m_e$, the tau-to-electron mass ratio $m_τ/m_e$, and the tau-to-muon mass ratio $m_τ/m_μ$.
background
ObservablePayloads replaces earlier raw List ℝ encodings with strongly typed records for dimensionless payloads. LeptonMassRatios supplies the lepton-sector component with the canonical field layout {mu_over_e, tau_over_e, tau_over_mu}. DimlessPack embeds this record to hold predictions extracted from any ledger-bridge pair, while UniversalDimless stores the corresponding φ-closed target values that Recognition Science claims must attain.
proof idea
Structure definition that directly declares three named real fields; no tactics, reductions, or lemmas are applied.
why it matters in Recognition Science
Supplies the lepton mass-ratio slot required by DimlessPack and UniversalDimless, and is constructed by massRatiosFromTiers via massRatioFromRungs on ledger tier differences. It implements the Recognition mass formula on the phi-ladder for the three lepton generations, feeding the eight-tick octave and the D=3 spatial structure. The record therefore closes one concrete interface between ledger data and the dimensionless observables demanded by the framework.
scope and limits
- Does not assign numerical values to any ratio.
- Does not enforce algebraic relations among the three fields.
- Does not derive the ratios from the J-cost or Recognition Composition Law.
- Does not connect the record to a specific ledger or bridge.
Lean usage
⟨ massRatioFromRungs L φ .leptons .second .first, massRatioFromRungs L φ .leptons .third .first, massRatioFromRungs L φ .leptons .third .second ⟩formal statement (Lean)
20structure LeptonMassRatios where
21 mu_over_e : ℝ
22 tau_over_e : ℝ
23 tau_over_mu : ℝ
24
25/-- CKM mixing-angle magnitudes (dimensionless). -/