born_rule_from_C

proof body

Tactic-mode proof.

  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-- ... 16 more lines elided ...