IndisputableMonolith.RecogSpec.ObservablePayloads

   1import Mathlib
   2
   3/-!
   4# Observable Payloads (Typed)
   5
   6Strongly typed records for the dimensionless mass-ratio and mixing-angle
   7payloads.  These replace the raw `List ℝ` fields that previously encoded
   8position-dependent semantics.
   9
  10## Canonical semantics
  11
  12  LeptonMassRatios : { mu_over_e, tau_over_e, tau_over_mu }
  13  CkmMixingAngles  : { vus, vcb, vub }
  14-/
  15
  16namespace IndisputableMonolith
  17namespace RecogSpec
  18
  19/-- Lepton-sector inter-generation mass ratios (dimensionless). -/
  20structure LeptonMassRatios where
  21  mu_over_e   : ℝ
  22  tau_over_e  : ℝ
  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
  57theorem toList_injective {a b : LeptonMassRatios} (h : a.toList = b.toList) : a = b := by
  58  simp only [toList] at h
  59  have h1 : a.mu_over_e = b.mu_over_e := List.cons.inj h |>.1
  60  have h23 := List.cons.inj h |>.2
  61  have h2 : a.tau_over_e = b.tau_over_e := List.cons.inj h23 |>.1
  62  have h3 : a.tau_over_mu = b.tau_over_mu := List.cons.inj (List.cons.inj h23 |>.2) |>.1
  63  exact ext h1 h2 h3
  64
  65@[simp] theorem mk_toList (a b c : ℝ) :
  66    (⟨a, b, c⟩ : LeptonMassRatios).toList = [a, b, c] := rfl
  67
  68end LeptonMassRatios
  69
  70namespace CkmMixingAngles
  71
  72/-- Canonical list view: `[V_us, V_cb, V_ub]`. -/
  73def toList (m : CkmMixingAngles) : List ℝ :=
  74  [m.vus, m.vcb, m.vub]
  75
  76@[simp] theorem toList_length (m : CkmMixingAngles) : m.toList.length = 3 := rfl
  77
  78/-- Every field satisfies a predicate. -/
  79def Forall (P : ℝ → Prop) (m : CkmMixingAngles) : Prop :=
  80  P m.vus ∧ P m.vcb ∧ P m.vub
  81
  82theorem forall_iff_list (P : ℝ → Prop) (m : CkmMixingAngles) :
  83    m.Forall P ↔ ∀ r ∈ m.toList, P r := by
  84  simp only [Forall, toList, List.mem_cons, List.mem_nil_iff, or_false]
  85  constructor
  86  · rintro ⟨h1, h2, h3⟩ r (rfl | rfl | rfl) <;> assumption
  87  · intro h
  88    exact ⟨h _ (Or.inl rfl), h _ (Or.inr (Or.inl rfl)), h _ (Or.inr (Or.inr rfl))⟩
  89
  90@[ext] theorem ext {a b : CkmMixingAngles}
  91    (h1 : a.vus = b.vus)
  92    (h2 : a.vcb = b.vcb)
  93    (h3 : a.vub = b.vub) : a = b := by
  94  cases a; cases b; simp_all
  95
  96theorem toList_injective {a b : CkmMixingAngles} (h : a.toList = b.toList) : a = b := by
  97  simp only [toList] at h
  98  have h1 : a.vus = b.vus := List.cons.inj h |>.1
  99  have h23 := List.cons.inj h |>.2
 100  have h2 : a.vcb = b.vcb := List.cons.inj h23 |>.1
 101  have h3 : a.vub = b.vub := List.cons.inj (List.cons.inj h23 |>.2) |>.1
 102  exact ext h1 h2 h3
 103
 104@[simp] theorem mk_toList (a b c : ℝ) :
 105    (⟨a, b, c⟩ : CkmMixingAngles).toList = [a, b, c] := rfl
 106
 107end CkmMixingAngles
 108
 109end RecogSpec
 110end IndisputableMonolith
 111