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