forall_iff_list
plain-language theorem explainer
The theorem equates the predicate-based Forall property on a lepton mass ratios record with universal quantification over its three-element list view. Researchers working with typed observable payloads in Recognition Science cite it when converting between structured records and list representations for mass ratios. The proof is a term-mode reduction that simplifies the definitions then splits the biconditional via constructor and matches on list membership cases.
Claim. Let $P : {R} {to} {Prop}$ be any predicate on the reals and let $m$ be a lepton mass ratios record whose three components are the dimensionless ratios $mu/e$, $tau/e$, $tau/mu$. Then $P$ holds on every component of $m$ if and only if $P(r)$ holds for every real $r$ belonging to the list $[mu/e, tau/e, tau/mu]$.
background
The module supplies strongly typed records that replace raw List R fields for dimensionless mass-ratio and mixing-angle payloads. LeptonMassRatios is the structure carrying the three lepton-sector inter-generation ratios mu_over_e, tau_over_e, tau_over_mu. Forall is the auxiliary definition asserting that a predicate P holds simultaneously on all three fields of such a record. toList is the function that returns the canonical list [mu_over_e, tau_over_e, tau_over_mu]. The local setting is therefore a typed interface layer that keeps semantic position explicit while still permitting list-based reasoning.
proof idea
The term proof first simplifies with the definitions of Forall and toList together with the list membership lemmas. Constructor then splits the biconditional. The forward direction uses rintro to unpack the three-fold conjunction and matches each list element via the Or.inl/Or.inr cases, discharging by assumption. The reverse direction applies the supplied hypothesis three times, once to each explicit element obtained from the Or constructors, and reassembles the conjunction.
why it matters
This utility equivalence bridges the predicate view Forall with the list view toList inside the typed ObservablePayloads layer, allowing downstream code to choose whichever representation is convenient without losing the canonical semantics of the lepton ratios. It supports consistent handling of the mass-ratio payload that Recognition Science uses to encode observable data. No parent theorems are recorded among the used-by edges, indicating it functions as a local interface lemma rather than a chain step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.