probabilities_normalized

formal source

  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