born_rule_from_C

formal source

  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