CkmMixingAngles

formal source

  23  tau_over_mu : ℝ
  24
  25/-- CKM mixing-angle magnitudes (dimensionless). -/
  26structure CkmMixingAngles where
  27  vus : ℝ
  28  vcb : ℝ
  29  vub : ℝ
  30
  31namespace LeptonMassRatios
  32
  33/-- Canonical list view: `[μ/e, τ/e, τ/μ]`. -/
  34def toList (m : LeptonMassRatios) : List ℝ :=
  35  [m.mu_over_e, m.tau_over_e, m.tau_over_mu]
  36
  37@[simp] theorem toList_length (m : LeptonMassRatios) : m.toList.length = 3 := rfl
  38
  39/-- Every field satisfies a predicate. -/
  40def Forall (P : ℝ → Prop) (m : LeptonMassRatios) : Prop :=
  41  P m.mu_over_e ∧ P m.tau_over_e ∧ P m.tau_over_mu
  42
  43theorem forall_iff_list (P : ℝ → Prop) (m : LeptonMassRatios) :
  44    m.Forall P ↔ ∀ r ∈ m.toList, P r := by
  45  simp only [Forall, toList, List.mem_cons, List.mem_nil_iff, or_false]
  46  constructor
  47  · rintro ⟨h1, h2, h3⟩ r (rfl | rfl | rfl) <;> assumption
  48  · intro h
  49    exact ⟨h _ (Or.inl rfl), h _ (Or.inr (Or.inl rfl)), h _ (Or.inr (Or.inr rfl))⟩
  50
  51@[ext] theorem ext {a b : LeptonMassRatios}
  52    (h1 : a.mu_over_e = b.mu_over_e)
  53    (h2 : a.tau_over_e = b.tau_over_e)
  54    (h3 : a.tau_over_mu = b.tau_over_mu) : a = b := by
  55  cases a; cases b; simp_all
  56