LeptonMassRatios
plain-language theorem explainer
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.
Claim. A 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.