toList_length
The theorem asserts that the canonical list view of any lepton mass ratio record always contains exactly three entries. Researchers handling typed observables for dimensionless mass ratios in Recognition Science would cite it to enforce length invariants during data manipulations. The proof is a direct reflexivity reduction that unfolds the explicit three-element list constructor.
claimFor any record $m$ of lepton inter-generation mass ratios with components $mu/e$, $tau/e$, $tau/mu$, the associated list $[mu/e, tau/e, tau/mu]$ has length 3.
background
The module supplies strongly typed records for dimensionless mass-ratio and mixing-angle payloads, replacing earlier raw List ℝ encodings. LeptonMassRatios is the structure carrying the three real fields mu_over_e, tau_over_e, tau_over_mu. The companion toList definition returns the ordered list of those three values, establishing canonical semantics for the lepton sector.
proof idea
The proof is a one-line term-mode reflexivity that directly matches the length of the three-element list constructed by toList.
why it matters in Recognition Science
The result supplies a basic length invariant for the lepton mass-ratio payload, supporting simp-driven simplifications when these records appear in larger derivations. It fits the module's goal of precise, typed observables and aligns with the framework's use of fixed-length structures for dimensionless quantities. No downstream applications are recorded yet.
scope and limits
- Does not constrain the numerical values of the three mass ratios.
- Does not apply to CKM mixing-angle records.
- Does not derive or interpret the ratios physically.
formal statement (Lean)
37@[simp] theorem toList_length (m : LeptonMassRatios) : m.toList.length = 3 := rfl
proof body
Term-mode proof.
38
39/-- Every field satisfies a predicate. -/