IndisputableMonolith.Measurement.BornRule

   1import Mathlib
   2import IndisputableMonolith.Measurement.PathAction
   3import IndisputableMonolith.Measurement.C2ABridge
   4
   5/-!
   6# Born Rule from Recognition Cost
   7
   8This module derives Born's rule P(I) = |α_I|² from the recognition
   9cost functional J and the amplitude bridge 𝒜 = exp(-C/2)·exp(iφ).
  10-/
  11
  12namespace IndisputableMonolith
  13namespace Measurement
  14
  15open Real Complex
  16
  17/-- Two-outcome measurement probabilities from recognition weights -/
  18structure TwoOutcomeMeasurement where
  19  C₁ : ℝ  -- Recognition cost for outcome 1
  20  C₂ : ℝ  -- Recognition cost for outcome 2
  21  C₁_nonneg : 0 ≤ C₁
  22  C₂_nonneg : 0 ≤ C₂
  23
  24/-- Probability of outcome 1 -/
  25noncomputable def prob₁ (m : TwoOutcomeMeasurement) : ℝ :=
  26  Real.exp (-m.C₁) / (Real.exp (-m.C₁) + Real.exp (-m.C₂))
  27
  28/-- Probability of outcome 2 -/
  29noncomputable def prob₂ (m : TwoOutcomeMeasurement) : ℝ :=
  30  Real.exp (-m.C₂) / (Real.exp (-m.C₁) + Real.exp (-m.C₂))
  31
  32/-- Probabilities are non-negative -/
  33lemma prob₁_nonneg (m : TwoOutcomeMeasurement) : 0 ≤ prob₁ m := by
  34  unfold prob₁
  35  apply div_nonneg
  36  · exact (Real.exp_pos _).le
  37  · exact (add_pos (Real.exp_pos _) (Real.exp_pos _)).le
  38
  39lemma prob₂_nonneg (m : TwoOutcomeMeasurement) : 0 ≤ prob₂ m := by
  40  unfold prob₂
  41  apply div_nonneg
  42  · exact (Real.exp_pos _).le
  43  · exact (add_pos (Real.exp_pos _) (Real.exp_pos _)).le
  44
  45/-- Probabilities sum to 1 (normalization) -/
  46theorem probabilities_normalized (m : TwoOutcomeMeasurement) :
  47  prob₁ m + prob₂ m = 1 := by
  48  unfold prob₁ prob₂
  49  have hdenom : Real.exp (-m.C₁) + Real.exp (-m.C₂) ≠ 0 :=
  50    (add_pos (Real.exp_pos _) (Real.exp_pos _)).ne'
  51  set denom : ℝ := Real.exp (-m.C₁) + Real.exp (-m.C₂)
  52  have hadd :
  53      Real.exp (-m.C₁) / denom + Real.exp (-m.C₂) / denom = (Real.exp (-m.C₁) + Real.exp (-m.C₂)) / denom := by
  54    simpa [denom] using (add_div (Real.exp (-m.C₁)) (Real.exp (-m.C₂)) denom).symm
  55  -- Finish.
  56  simpa [denom, hadd] using (div_self hdenom)
  57
  58/-- Born rule: probabilities match quantum amplitude squares -/
  59theorem born_rule_from_C (α₁ α₂ : ℂ)
  60  (_hα : ‖α₁‖ ^ 2 + ‖α₂‖ ^ 2 = 1)
  61  (rot : TwoBranchRotation)
  62  (hrot₁ : ‖α₁‖ ^ 2 = complementAmplitudeSquared rot)
  63  (hrot₂ : ‖α₂‖ ^ 2 = initialAmplitudeSquared rot) :
  64  ∃ m : TwoOutcomeMeasurement,
  65    prob₁ m = ‖α₁‖ ^ 2 ∧
  66    prob₂ m = ‖α₂‖ ^ 2 := by
  67  -- Construct the measurement from the rate action
  68  -- From C_equals_2A, we have C = 2A where A = -ln(sin θ_s)
  69  -- So exp(-C) = exp(-2A) = sin²(θ_s) = |α₂|²
  70
  71  -- We use two costs:
  72  --   * `C_sin`: the RS path action cost (so exp(-C_sin) = sin² θ by the bridge),
  73  --   * `C_cos`: the complementary cost -2 log(cos θ) (so exp(-C_cos) = cos² θ).
  74  let C_sin := pathAction (pathFromRotation rot)
  75  let C_cos := -2 * Real.log (Real.cos rot.θ_s)
  76
  77  have hCsin_nonneg : 0 ≤ C_sin := by
  78    unfold C_sin pathAction
  79    -- pathAction is an integral of Jcost over positive rates
  80    -- Jcost(r) ≥ 0 for all r > 0 (proven in Cost module)
  81    refine intervalIntegral.integral_nonneg ?_ ?_
  82    · exact le_of_lt (pathFromRotation rot).T_pos
  83    · intro t ht
  84      apply Cost.Jcost_nonneg
  85      exact (pathFromRotation rot).rate_pos t ht
  86
  87  have hCcos_nonneg : 0 ≤ C_cos := by
  88    unfold C_cos
  89    have hneg2 : (-2 : ℝ) ≤ 0 := by norm_num
  90    have hlog : Real.log (Real.cos rot.θ_s) ≤ 0 := by
  91      apply Real.log_nonpos
  92      ·
  93        have hpi2 : (0 : ℝ) < Real.pi / 2 := by nlinarith [Real.pi_pos]
  94        have hneg : (-(Real.pi / 2) : ℝ) < rot.θ_s := lt_trans (neg_lt_zero.mpr hpi2) rot.θ_s_bounds.1
  95        exact le_of_lt (Real.cos_pos_of_mem_Ioo ⟨hneg, rot.θ_s_bounds.2⟩)
  96      · exact Real.cos_le_one _
  97    exact mul_nonneg_of_nonpos_of_nonpos hneg2 hlog
  98
  99  let m : TwoOutcomeMeasurement := {
 100    -- Convention: outcome 1 is the cos-branch (complement), outcome 2 is the sin-branch (initial).
 101    C₁ := C_cos
 102    C₂ := C_sin
 103    C₁_nonneg := hCcos_nonneg
 104    C₂_nonneg := hCsin_nonneg
 105  }
 106
 107  use m
 108  constructor
 109  · -- prob₁ m = ‖α₁‖²
 110    unfold prob₁
 111    -- Reduce to cos² / (cos² + sin²) = cos².
 112    rw [hrot₁]
 113    have hcos : Real.exp (-C_cos) = complementAmplitudeSquared rot := by
 114      -- exp(-(-2 log cos)) = cos²
 115      have hcos_pos : 0 < Real.cos rot.θ_s := by
 116        refine Real.cos_pos_of_mem_Ioo ?_
 117        refine ⟨?_, rot.θ_s_bounds.2⟩
 118        have hpi2 : (0 : ℝ) < Real.pi / 2 := by nlinarith [Real.pi_pos]
 119        linarith [rot.θ_s_bounds.1, hpi2]
 120      unfold C_cos complementAmplitudeSquared
 121      calc
 122        Real.exp (-(-2 * Real.log (Real.cos rot.θ_s)))
 123            = Real.exp (2 * Real.log (Real.cos rot.θ_s)) := by ring_nf
 124        _ = Real.exp (Real.log ((Real.cos rot.θ_s) ^ 2)) := by
 125            congr 1
 126            exact (Real.log_pow (Real.cos rot.θ_s) 2).symm
 127        _ = (Real.cos rot.θ_s) ^ 2 := Real.exp_log (pow_pos hcos_pos 2)
 128    have hsin : Real.exp (-C_sin) = initialAmplitudeSquared rot := by
 129      -- exp(-pathAction) = pathWeight = sin²
 130      have h := weight_equals_born rot
 131      simpa [pathWeight, C_sin] using h
 132    rw [hcos, hsin]
 133    simp [complementAmplitudeSquared, initialAmplitudeSquared, Real.cos_sq_add_sin_sq rot.θ_s]
 134  · -- prob₂ m = ‖α₂‖²
 135    unfold prob₂
 136    rw [hrot₂]
 137    -- Reduce to sin² / (cos² + sin²) = sin².
 138    have hcos : Real.exp (-C_cos) = complementAmplitudeSquared rot := by
 139      have hcos_pos : 0 < Real.cos rot.θ_s := by
 140        refine Real.cos_pos_of_mem_Ioo ?_
 141        refine ⟨?_, rot.θ_s_bounds.2⟩
 142        have hpi2 : (0 : ℝ) < Real.pi / 2 := by nlinarith [Real.pi_pos]
 143        linarith [rot.θ_s_bounds.1, hpi2]
 144      unfold C_cos complementAmplitudeSquared
 145      calc
 146        Real.exp (-(-2 * Real.log (Real.cos rot.θ_s)))
 147            = Real.exp (2 * Real.log (Real.cos rot.θ_s)) := by ring_nf
 148        _ = Real.exp (Real.log ((Real.cos rot.θ_s) ^ 2)) := by
 149            congr 1
 150            exact (Real.log_pow (Real.cos rot.θ_s) 2).symm
 151        _ = (Real.cos rot.θ_s) ^ 2 := Real.exp_log (pow_pos hcos_pos 2)
 152    have hsin : Real.exp (-C_sin) = initialAmplitudeSquared rot := by
 153      have h := weight_equals_born rot
 154      simpa [pathWeight, C_sin] using h
 155    -- The definition of `prob₂` uses exp(-C₂), and `m.C₂ = C_sin`.
 156    -- So we rewrite and conclude.
 157    -- (Note: `unfold` above expanded `C₁`/`C₂` fields of `m` to the right constants.)
 158    rw [hcos, hsin]
 159    simp [complementAmplitudeSquared, initialAmplitudeSquared, Real.cos_sq_add_sin_sq rot.θ_s]
 160
 161/-- Born rule normalized: from recognition costs to normalized probabilities -/
 162theorem born_rule_normalized (C₁ C₂ : ℝ) (α₁ α₂ : ℂ)
 163  (h₁ : Real.exp (-C₁) / (Real.exp (-C₁) + Real.exp (-C₂)) = ‖α₁‖ ^ 2)
 164  (h₂ : Real.exp (-C₂) / (Real.exp (-C₁) + Real.exp (-C₂)) = ‖α₂‖ ^ 2) :
 165  ‖α₁‖ ^ 2 + ‖α₂‖ ^ 2 = 1 := by
 166  have hdenom : Real.exp (-C₁) + Real.exp (-C₂) ≠ 0 :=
 167    (add_pos (Real.exp_pos _) (Real.exp_pos _)).ne'
 168  calc ‖α₁‖ ^ 2 + ‖α₂‖ ^ 2
 169      = Real.exp (-C₁) / (Real.exp (-C₁) + Real.exp (-C₂)) +
 170        Real.exp (-C₂) / (Real.exp (-C₁) + Real.exp (-C₂)) := by rw [← h₁, ← h₂]
 171      _ = (Real.exp (-C₁) + Real.exp (-C₂)) / (Real.exp (-C₁) + Real.exp (-C₂)) := by
 172        simpa using
 173          (add_div (Real.exp (-C₁)) (Real.exp (-C₂)) (Real.exp (-C₁) + Real.exp (-C₂))).symm
 174      _ = 1 := div_self hdenom
 175
 176end Measurement
 177end IndisputableMonolith
 178