toList_injective
plain-language theorem explainer
The theorem shows that the canonical list map from lepton mass ratio records is injective: equal lists of the three ratios force the records to be identical. Researchers encoding observable payloads in Recognition Science cite it to guarantee unique recovery from the list view. The proof simplifies the list definition then extracts each component equality via successive list cons injections before applying structure extensionality.
Claim. Let $a$ and $b$ be lepton mass ratio records with real components $a_1 = a.μ/e$, $a_2 = a.τ/e$, $a_3 = a.τ/μ$ (and likewise for $b$). If the lists $[a_1, a_2, a_3] = [b_1, b_2, b_3]$, then $a = b$.
background
LeptonMassRatios is the structure holding the three dimensionless lepton-sector ratios μ/e, τ/e, τ/μ. The toList definition converts any such record into the ordered list containing exactly those three values. The module supplies strongly typed records for both lepton mass ratios and CKM mixing angles, replacing earlier raw List ℝ fields with canonical semantics.
proof idea
The term proof first rewrites the hypothesis by unfolding toList. It then applies List.cons.inj three times to obtain the three component equalities. The final step invokes the structure extensionality lemma ext on those three equalities.
why it matters
Injectivity secures that the list representation uniquely determines the typed lepton record, supporting the canonical semantics of the observable payloads module. It underpins faithful conversion between record and list forms used in downstream mass-ratio and mixing-angle constraints. Within Recognition Science this contributes to the typed handling of dimensionless observables that enter the phi-ladder mass formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.