IndisputableMonolith.RecogSpec.Core

   1import Mathlib
   2import IndisputableMonolith.RecogSpec.ObservablePayloads
   3
   4namespace IndisputableMonolith
   5namespace RecogSpec
   6
   7noncomputable section
   8
   9/-- Basic ledger carrier augmented with optional bookkeeping data so downstream
  10modules can project canonical states without introducing additional structure. -/
  11structure Ledger where
  12  Carrier : Type
  13  state : Option Carrier := none
  14  tick : Option (Carrier → ℕ) := none
  15
  16/-- Bridge over a ledger. -/
  17structure Bridge (L : Ledger) : Type where
  18  dummy : Unit := ()
  19
  20/-- Units equivalence relation over bridges. -/
  21structure UnitsEqv (L : Ledger) : Type where
  22  Rel   : Bridge L → Bridge L → Prop
  23  refl  : ∀ B, Rel B B
  24  symm  : ∀ {B₁ B₂}, Rel B₁ B₂ → Rel B₂ B₁
  25  trans : ∀ {B₁ B₂ B₃}, Rel B₁ B₂ → Rel B₂ B₃ → Rel B₁ B₃
  26
  27/-- Dimensionless predictions extracted from a bridge. -/
  28structure DimlessPack (L : Ledger) (B : Bridge L) : Type where
  29  alpha            : ℝ
  30  massRatios       : LeptonMassRatios
  31  mixingAngles     : CkmMixingAngles
  32  g2Muon           : ℝ
  33  strongCPNeutral  : Prop
  34  eightTickMinimal : Prop
  35  bornRule         : Prop
  36
  37/-- Absolute (SI) packaging for reference displays, distinct from dimensionless pack. -/
  38structure AbsolutePack (L : Ledger) (B : Bridge L) : Type where
  39  c_SI        : ℝ
  40  hbar_SI     : ℝ
  41  G_SI        : ℝ
  42  Lambda_SI   : ℝ
  43  masses_SI   : List ℝ
  44  energies_SI : List ℝ
  45
  46/-- Subfield generated by `φ`. -/
  47def phiSubfield (φ : ℝ) : Subfield ℝ :=
  48  Subfield.closure ({φ} : Set ℝ)
  49
  50/-- The value `x` is algebraic over the subfield generated by `φ` using field
  51operations. -/
  52def PhiClosed (φ x : ℝ) : Prop := x ∈ phiSubfield φ
  53
  54namespace PhiClosed
  55
  56variable {φ x y : ℝ}
  57
  58@[simp] lemma mem : PhiClosed φ x ↔ x ∈ phiSubfield φ := Iff.rfl
  59
  60lemma self (φ : ℝ) : PhiClosed φ φ := by
  61  change φ ∈ phiSubfield φ
  62  exact Subfield.subset_closure (by simp)
  63
  64lemma of_rat (φ : ℝ) (q : ℚ) : PhiClosed φ (q : ℝ) := by
  65  change ((algebraMap ℚ ℝ) q) ∈ phiSubfield φ
  66  simpa using (phiSubfield φ).algebraMap_mem q
  67
  68lemma zero (φ : ℝ) : PhiClosed φ (0 : ℝ) :=
  69  (phiSubfield φ).zero_mem
  70
  71lemma one (φ : ℝ) : PhiClosed φ (1 : ℝ) :=
  72  (phiSubfield φ).one_mem
  73
  74lemma add (hx : PhiClosed φ x) (hy : PhiClosed φ y) :
  75    PhiClosed φ (x + y) :=
  76  (phiSubfield φ).add_mem hx hy
  77
  78lemma sub (hx : PhiClosed φ x) (hy : PhiClosed φ y) :
  79    PhiClosed φ (x - y) :=
  80  (phiSubfield φ).sub_mem hx hy
  81
  82lemma neg (hx : PhiClosed φ x) : PhiClosed φ (-x) :=
  83  (phiSubfield φ).neg_mem hx
  84
  85lemma mul (hx : PhiClosed φ x) (hy : PhiClosed φ y) :
  86    PhiClosed φ (x * y) :=
  87  (phiSubfield φ).mul_mem hx hy
  88
  89lemma inv (hx : PhiClosed φ x) : PhiClosed φ x⁻¹ :=
  90  (phiSubfield φ).inv_mem hx
  91
  92lemma div (hx : PhiClosed φ x) (hy : PhiClosed φ y) :
  93    PhiClosed φ (x / y) :=
  94  (phiSubfield φ).div_mem hx hy
  95
  96lemma pow (hx : PhiClosed φ x) (n : ℕ) : PhiClosed φ (x ^ n) := by
  97  simpa using (phiSubfield φ).pow_mem hx n
  98
  99lemma pow_self (φ : ℝ) (n : ℕ) : PhiClosed φ (φ ^ n) :=
 100  pow (self φ) n
 101
 102lemma inv_self (φ : ℝ) : PhiClosed φ (φ⁻¹) :=
 103  inv (self φ)
 104
 105lemma inv_pow_self (φ : ℝ) (n : ℕ) : PhiClosed φ ((φ ^ n)⁻¹) :=
 106  inv (pow_self φ n)
 107
 108lemma of_nat (φ : ℝ) (n : ℕ) : PhiClosed φ (n : ℝ) := by
 109  simpa using of_rat φ n
 110
 111lemma half (φ : ℝ) : PhiClosed φ (1 / (2 : ℝ)) := by
 112  have htwo : PhiClosed φ ((2 : ℚ) : ℝ) := of_rat φ 2
 113  simpa using inv htwo
 114
 115end PhiClosed
 116
 117/-- Universal φ-closed targets RS claims are forced to take. -/
 118structure UniversalDimless (φ : ℝ) : Type where
 119  alpha0        : ℝ
 120  massRatios0   : LeptonMassRatios
 121  mixingAngles0 : CkmMixingAngles
 122  g2Muon0       : ℝ
 123  strongCP0     : Prop
 124  eightTick0    : Prop
 125  born0         : Prop
 126  alpha0_isPhi        : PhiClosed φ alpha0
 127  massRatios0_isPhi   : massRatios0.Forall (PhiClosed φ)
 128  mixingAngles0_isPhi : mixingAngles0.Forall (PhiClosed φ)
 129  g2Muon0_isPhi       : PhiClosed φ g2Muon0
 130
 131/-- "Bridge B matches universal U" (pure proposition). -/
 132def Matches (φ : ℝ) (L : Ledger) (B : Bridge L) (U : UniversalDimless φ) : Prop :=
 133  ∃ (P : DimlessPack L B),
 134    P.alpha = U.alpha0
 135      ∧ P.massRatios = U.massRatios0
 136      ∧ P.mixingAngles = U.mixingAngles0
 137      ∧ P.g2Muon = U.g2Muon0
 138      ∧ P.strongCPNeutral = U.strongCP0
 139      ∧ P.eightTickMinimal = U.eightTick0
 140      ∧ P.bornRule = U.born0
 141
 142end
 143
 144end RecogSpec
 145end IndisputableMonolith
 146