ext
Two lepton mass ratio records coincide exactly when their muon-to-electron, tau-to-electron, and tau-to-muon components match. Modelers of lepton observables in Recognition Science invoke the result to substitute one record for another after verifying the three ratios. The argument is a one-line wrapper that cases on both records and simplifies the field equalities.
claimIf two lepton mass ratio structures $a$ and $b$ satisfy $a.μ/e = b.μ/e$, $a.τ/e = b.τ/e$, and $a.τ/μ = b.τ/μ$, then $a = b$.
background
The lepton mass ratio structure records the three dimensionless inter-generation lepton mass ratios: muon-to-electron, tau-to-electron, and tau-to-muon. The ObservablePayloads module supplies strongly typed records for these mass ratios and for CKM mixing angles, replacing prior raw List real encodings that carried position-dependent semantics. This extensionality theorem depends only on the structure definition of the lepton mass ratios and the parallel CKM structure.
proof idea
The proof is a one-line wrapper: it cases on both input structures and then applies simp_all to the resulting field equalities.
why it matters in Recognition Science
The declaration supplies the standard extensionality principle for the typed lepton mass ratio payload. It supports the module's replacement of untyped lists by structures that carry explicit semantics for the lepton sector. No parent theorems or downstream citations are recorded, but the result closes basic equality reasoning needed for observable data in the Recognition framework.
scope and limits
- Does not assert any specific numerical values for the mass ratios.
- Does not relate the lepton ratios to CKM mixing angles or other sectors.
- Does not invoke the forcing chain or Recognition Composition Law.
- Does not extend to quark mass ratios or higher structures.
formal statement (Lean)
51@[ext] theorem ext {a b : LeptonMassRatios}
52 (h1 : a.mu_over_e = b.mu_over_e)
53 (h2 : a.tau_over_e = b.tau_over_e)
54 (h3 : a.tau_over_mu = b.tau_over_mu) : a = b := by
proof body
One-line wrapper that applies cases.
55 cases a; cases b; simp_all
56