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