Forall
The Forall definition on LeptonMassRatios asserts that a predicate P holds simultaneously on the three lepton mass ratios mu_over_e, tau_over_e, and tau_over_mu. Researchers verifying uniform properties across lepton generations in Recognition Science cite this when checking predicates such as positivity on the canonical payload. It is realized as an immediate conjunction over the three structure fields.
claimLet $P : ℝ → Prop$ be any predicate and let $m$ be a LeptonMassRatios record with components $m_{μ/e}$, $m_{τ/e}$, $m_{τ/μ}$. Then $m.Forall(P)$ is defined by the conjunction $P(m_{μ/e}) ∧ P(m_{τ/e}) ∧ P(m_{τ/μ})$.
background
The Observable Payloads module supplies strongly typed records that replace earlier List ℝ encodings for dimensionless observables. LeptonMassRatios is the structure whose fields are the three lepton-sector inter-generation mass ratios (muon-electron, tau-electron, tau-muon). The Forall definition supplies a uniform predicate applicator over this fixed three-component record.
proof idea
One-line definition that directly unfolds to the conjunction of P applied to each of the three fields of LeptonMassRatios.
why it matters in Recognition Science
Forall is used inside UniversalDimless to package the massRatios0 component and inside massRatiosFromTiers_pos to prove that every entry is positive when φ > 0. It also appears in the equivalence forall_iff_list that relates the typed record to its list representation. In the Recognition Science setting this supports uniform checks on the lepton mass ratios that appear in the φ-closed targets.
scope and limits
- Does not apply to CKM mixing angles or other structures.
- Does not encode numerical values or compute ratios.
- Assumes the LeptonMassRatios record contains exactly the three declared real fields.
- Does not extend to predicates that depend on ordering or external context.
Lean usage
(massRatiosFromTiers L φ).Forall (0 < ·)formal statement (Lean)
40def Forall (P : ℝ → Prop) (m : LeptonMassRatios) : Prop :=
proof body
Definition body.
41 P m.mu_over_e ∧ P m.tau_over_e ∧ P m.tau_over_mu
42