IndisputableMonolith.Verification.BornRuleRouteB

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# Born Rule Route B: No-Signaling Uniqueness (Proposition 3.7)
   6
   7Formalizes the central theorem of the Born rule paper (Simons, Washburn,
   8Allahyarov): the premises (SA)+(NC)+(CS)+(PA)+(P5)₂ force f(r) = r².
   9
  10## Status: Zero sorry
  11-/
  12
  13namespace IndisputableMonolith.Verification.BornRuleRouteB
  14
  15open Real
  16
  17noncomputable section
  18
  19/-- Route B hypothesis bundle (Proposition 3.7(a)–(d), pre-processed). -/
  20structure RouteBHyp (f : ℝ → ℝ) : Prop where
  21  cont : Continuous f
  22  f_zero : f 0 = 0
  23  f_one : f 1 = 1
  24  no_sig : ∀ r s : ℝ, 0 < r → 0 < s → s < 1 →
  25    f (r * s) + f (r * Real.sqrt (1 - s ^ 2)) = f r
  26
  27/-! ## Steps 1–2: No-Signaling → Additive Cauchy Equation -/
  28
  29def hSub (f : ℝ → ℝ) (x : ℝ) : ℝ := f (Real.sqrt x)
  30
  31theorem hSub_zero {f : ℝ → ℝ} (H : RouteBHyp f) : hSub f 0 = 0 := by
  32  simp only [hSub, Real.sqrt_zero, H.f_zero]
  33
  34theorem hSub_one {f : ℝ → ℝ} (H : RouteBHyp f) : hSub f 1 = 1 := by
  35  simp only [hSub, Real.sqrt_one, H.f_one]
  36
  37theorem hSub_cont {f : ℝ → ℝ} (H : RouteBHyp f) : Continuous (hSub f) :=
  38  H.cont.comp continuous_sqrt
  39
  40theorem hSub_split {f : ℝ → ℝ} (H : RouteBHyp f)
  41    {R p : ℝ} (hR : 0 < R) (hp0 : 0 < p) (hp1 : p < 1) :
  42    hSub f (R * p) + hSub f (R * (1 - p)) = hSub f R := by
  43  unfold hSub
  44  set r := Real.sqrt R with hr_def
  45  set s := Real.sqrt p with hs_def
  46  have hr_pos : 0 < r := Real.sqrt_pos.mpr hR
  47  have hs_pos : 0 < s := Real.sqrt_pos.mpr hp0
  48  have hs_sq : s ^ 2 = p := Real.sq_sqrt (le_of_lt hp0)
  49  have hs_lt1 : s < 1 := by
  50    nlinarith [hs_sq]
  51  have : Real.sqrt (R * p) = r * s :=
  52    (Real.sqrt_mul (le_of_lt hR) p).symm ▸ by rw [hr_def, hs_def]
  53  rw [this]
  54  have h_1ms : 1 - s ^ 2 = 1 - p := by rw [hs_sq]
  55  have : Real.sqrt (R * (1 - p)) = r * Real.sqrt (1 - s ^ 2) := by
  56    rw [h_1ms, hr_def, ← Real.sqrt_mul (le_of_lt hR)]
  57  rw [this]
  58  exact H.no_sig r s hr_pos hs_pos hs_lt1
  59
  60theorem hSub_additive {f : ℝ → ℝ} (H : RouteBHyp f)
  61    {x y : ℝ} (hx : 0 < x) (hy : 0 < y) :
  62    hSub f (x + y) = hSub f x + hSub f y := by
  63  have hS : 0 < x + y := add_pos hx hy
  64  have hS_ne : x + y ≠ 0 := ne_of_gt hS
  65  have hp : 0 < x / (x + y) := div_pos hx hS
  66  have hp1 : x / (x + y) < 1 := by rwa [div_lt_one hS, add_comm, lt_add_iff_pos_left]
  67  have h1 : (x + y) * (x / (x + y)) = x := mul_div_cancel₀ x hS_ne
  68  have h2 : (x + y) * (1 - x / (x + y)) = y := by field_simp; linarith
  69  have := hSub_split H hS hp hp1
  70  rw [h1, h2] at this; linarith
  71
  72/-! ## Step 3: Cauchy Equation Solution (Bounded-Deviation Argument) -/
  73
  74private theorem additive_nat_mul
  75    {g : ℝ → ℝ} (g_add : ∀ x y : ℝ, 0 < x → 0 < y → g (x + y) = g x + g y)
  76    (g0 : g 0 = 0) (n : ℕ) {x : ℝ} (hx : 0 < x) :
  77    g (↑n * x) = ↑n * g x := by
  78  induction n with
  79  | zero => simp [g0]
  80  | succ k ih =>
  81    cases k with
  82    | zero => simp
  83    | succ m =>
  84      have hk : (0 : ℝ) < ↑(m + 1) * x := by positivity
  85      have : (↑(m + 2) : ℝ) * x = ↑(m + 1) * x + x := by push_cast; ring
  86      rw [this, g_add _ _ hk hx, ih]
  87      push_cast; ring
  88
  89private theorem additive_nat_zero
  90    {g : ℝ → ℝ} (g_add : ∀ x y : ℝ, 0 < x → 0 < y → g (x + y) = g x + g y)
  91    (g0 : g 0 = 0) (g1 : g 1 = 0) (n : ℕ) :
  92    g (↑n : ℝ) = 0 := by
  93  have := additive_nat_mul g_add g0 n one_pos
  94  simp only [mul_one] at this; rw [this, g1, mul_zero]
  95
  96private theorem additive_zero_on_unit
  97    {g : ℝ → ℝ} (gcont : Continuous g)
  98    (g_add : ∀ x y : ℝ, 0 < x → 0 < y → g (x + y) = g x + g y)
  99    (g0 : g 0 = 0) (g1 : g 1 = 0)
 100    {x : ℝ} (hx0 : 0 ≤ x) (hx1 : x ≤ 1) : g x = 0 := by
 101  rcases eq_or_lt_of_le hx0 with rfl | hx_pos; · exact g0
 102  rcases eq_or_lt_of_le hx1 with rfl | _; · exact g1
 103  obtain ⟨z, _, hz_max⟩ := isCompact_Icc.exists_isMaxOn
 104    (Set.nonempty_Icc.mpr (show (0 : ℝ) ≤ 2 by norm_num))
 105    ((continuous_abs.comp gcont).continuousOn)
 106  set M := |g z| + 1
 107  have hM_pos : (0 : ℝ) < M := by positivity
 108  have hM_bd : ∀ t ∈ Set.Icc (0 : ℝ) 2, |g t| ≤ M :=
 109    fun t ht => le_trans (hz_max ht) (le_of_lt (lt_add_one _))
 110  by_contra h_ne
 111  have h_gx_pos : 0 < |g x| := abs_pos.mpr h_ne
 112  obtain ⟨N, hN⟩ := exists_nat_gt (M / |g x|)
 113  have hN_pos : (0 : ℝ) < ↑N := lt_trans (div_pos hM_pos h_gx_pos) hN
 114  have hN_nat : 0 < N := Nat.pos_of_ne_zero (by exact_mod_cast ne_of_gt hN_pos)
 115  have h_scale := additive_nat_mul g_add g0 N hx_pos
 116  have h_Nx_nn : (0 : ℝ) ≤ ↑N * x := by positivity
 117  set frac := ↑N * x - ↑⌊↑N * x⌋₊ with frac_def
 118  have h_frac_nn : 0 ≤ frac := sub_nonneg.mpr (Nat.floor_le h_Nx_nn)
 119  have h_frac_lt : frac < 1 := by
 120    simp only [frac_def]
 121    have := Nat.lt_floor_add_one (↑N * x); push_cast at this ⊢; linarith
 122  have h_frac_le2 : frac ≤ 2 := by linarith
 123  have h_key : g (↑⌊↑N * x⌋₊ : ℝ) = 0 := additive_nat_zero g_add g0 g1 _
 124  have h_gNx : g (↑N * x) = g frac := by
 125    rcases eq_or_lt_of_le h_frac_nn with heq | h_frac_pos
 126    · have hfrac0 : frac = 0 := by linarith
 127      rw [show ↑N * x = (↑⌊↑N * x⌋₊ : ℝ) from by linarith [frac_def],
 128          h_key, hfrac0, g0]
 129    · rcases Nat.eq_zero_or_pos ⌊↑N * x⌋₊ with h0 | hpos
 130      · simp only [h0, Nat.cast_zero] at frac_def ⊢; simp [frac_def]
 131      · have h_fl_pos : (0 : ℝ) < (↑⌊↑N * x⌋₊ : ℝ) := by exact_mod_cast hpos
 132        have h_decomp : ↑N * x = frac + (↑⌊↑N * x⌋₊ : ℝ) := by
 133          simp only [frac_def]; ring
 134        rw [h_decomp, g_add _ _ h_frac_pos h_fl_pos, h_key, add_zero]
 135  rw [h_scale] at h_gNx
 136  have h_bd := hM_bd frac ⟨h_frac_nn, h_frac_le2⟩
 137  rw [← h_gNx] at h_bd
 138  rw [abs_mul, abs_of_pos hN_pos] at h_bd
 139  nlinarith [mul_lt_mul_of_pos_right hN h_gx_pos,
 140             div_mul_cancel₀ M (ne_of_gt h_gx_pos)]
 141
 142private theorem additive_zero_on_nonneg
 143    {g : ℝ → ℝ} (gcont : Continuous g)
 144    (g_add : ∀ x y : ℝ, 0 < x → 0 < y → g (x + y) = g x + g y)
 145    (g0 : g 0 = 0) (g1 : g 1 = 0)
 146    {x : ℝ} (hx : 0 ≤ x) : g x = 0 := by
 147  rcases le_or_gt x 1 with h | h
 148  · exact additive_zero_on_unit gcont g_add g0 g1 hx h
 149  · set frac := x - ↑⌊x⌋₊ with frac_def
 150    have h_frac_nn : 0 ≤ frac := sub_nonneg.mpr (Nat.floor_le hx)
 151    have h_frac_lt : frac < 1 := by
 152      simp only [frac_def]
 153      have := Nat.lt_floor_add_one x; push_cast at this ⊢; linarith
 154    have h_key : g (↑⌊x⌋₊ : ℝ) = 0 := additive_nat_zero g_add g0 g1 _
 155    rcases eq_or_lt_of_le h_frac_nn with heq | h_frac_pos
 156    · rw [show x = (↑⌊x⌋₊ : ℝ) from by linarith [frac_def]]; exact h_key
 157    · have hfl_pos : (0 : ℝ) < (↑⌊x⌋₊ : ℝ) := by
 158        rcases Nat.eq_zero_or_pos ⌊x⌋₊ with h0 | hp
 159        · simp only [h0, Nat.cast_zero] at frac_def; linarith
 160        · exact_mod_cast hp
 161      have h_decomp : x = frac + (↑⌊x⌋₊ : ℝ) := by simp only [frac_def]; ring
 162      rw [h_decomp, g_add _ _ h_frac_pos hfl_pos, h_key, add_zero]
 163      exact additive_zero_on_unit gcont g_add g0 g1 h_frac_nn (le_of_lt h_frac_lt)
 164
 165/-! ## Step 3 applied: h = id -/
 166
 167private def gDev (f : ℝ → ℝ) (x : ℝ) : ℝ := hSub f x - x
 168
 169theorem hSub_eq_id {f : ℝ → ℝ} (H : RouteBHyp f) {x : ℝ} (hx : 0 ≤ x) :
 170    hSub f x = x := by
 171  have h0 : gDev f x = 0 := additive_zero_on_nonneg
 172    ((hSub_cont H).sub continuous_id)
 173    (fun a b ha hb => show hSub f (a + b) - (a + b) = (hSub f a - a) + (hSub f b - b) by
 174      rw [hSub_additive H ha hb]; ring)
 175    (show hSub f 0 - 0 = 0 by rw [hSub_zero H]; ring)
 176    (show hSub f 1 - 1 = 0 by rw [hSub_one H]; ring)
 177    hx
 178  unfold gDev at h0; linarith
 179
 180/-! ## Step 4: f(r) = r² -/
 181
 182/-- **Proposition 3.7 (Route B)**: f(r) = r² for all r ≥ 0. -/
 183theorem born_rule_route_B {f : ℝ → ℝ} (H : RouteBHyp f)
 184    {r : ℝ} (hr : 0 ≤ r) : f r = r ^ 2 := by
 185  have : hSub f (r ^ 2) = r ^ 2 := hSub_eq_id H (sq_nonneg r)
 186  simp only [hSub, Real.sqrt_sq hr] at this; exact this
 187
 188/-- (MA) is a COROLLARY, not an axiom (Remark 3.6 of the paper). -/
 189theorem modulus_multiplicativity {f : ℝ → ℝ} (H : RouteBHyp f)
 190    {r₁ r₂ : ℝ} (h1 : 0 ≤ r₁) (h2 : 0 ≤ r₂) :
 191    f (r₁ * r₂) = f r₁ * f r₂ := by
 192  simp only [born_rule_route_B H (mul_nonneg h1 h2),
 193    born_rule_route_B H h1, born_rule_route_B H h2]; ring
 194
 195/-! ## Certificate -/
 196
 197/-- Route B Born Rule Certificate. -/
 198structure RouteBCert (f : ℝ → ℝ) : Prop where
 199  quadratic : ∀ r, 0 ≤ r → f r = r ^ 2
 200  mult : ∀ r₁ r₂, 0 ≤ r₁ → 0 ≤ r₂ → f (r₁ * r₂) = f r₁ * f r₂
 201
 202theorem route_B_certified {f : ℝ → ℝ} (H : RouteBHyp f) : RouteBCert f where
 203  quadratic := fun _r hr => born_rule_route_B H hr
 204  mult := fun _r₁ _r₂ h1 h2 => modulus_multiplicativity H h1 h2
 205
 206end
 207
 208end IndisputableMonolith.Verification.BornRuleRouteB
 209