Forall
plain-language theorem explainer
Defines Forall P m to mean that predicate P holds on each of the three lepton mass ratio components. Researchers stating uniform properties over dimensionless observables in Recognition Science cite this definition to avoid raw list indexing. The implementation is a direct conjunction over the record fields with no lemmas or tactics required.
Claim. Let $P : \mathbb{R} \to \mathrm{Prop}$ be any predicate and let $m$ be a lepton mass ratios record with components $\mu/e$, $\tau/e$, $\tau/\mu$. Then $\mathrm{Forall}(P, m)$ holds precisely when $P(\mu/e) \land P(\tau/e) \land P(\tau/\mu)$.
background
The ObservablePayloads module supplies strongly typed records for dimensionless mass-ratio and mixing-angle payloads that replace earlier raw List ℝ encodings. LeptonMassRatios is the structure whose fields are exactly the three inter-generation ratios mu_over_e, tau_over_e, tau_over_mu. The definition supplies a uniform way to assert that an arbitrary predicate holds on every component of such a record.
The two upstream structures are the LeptonMassRatios and CkmMixingAngles records themselves; both appear only to supply the typed payloads whose fields are referenced by the conjunction.
proof idea
One-line definition that expands directly to the conjunction P m.mu_over_e ∧ P m.tau_over_e ∧ P m.tau_over_mu. No lemmas are invoked and no tactics are used.
why it matters
The definition enables uniform component-wise statements inside the typed observable payloads of Recognition Science. It is invoked by UniversalDimless to package the massRatios0 field, by massRatiosFromTiers_pos to prove all three ratios are positive, and by forall_iff_list to equate the record predicate with list membership. It thereby supports the canonical semantics section of the module without exposing list operations to downstream RS claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.