TwoBranchRotation

formal source

  19open Real
  20
  21/-- A two-branch quantum measurement rotation from angle θ_s to π/2 -/
  22structure TwoBranchRotation where
  23  θ_s : ℝ  -- starting angle (determines initial amplitude)
  24  θ_s_bounds : 0 < θ_s ∧ θ_s < π/2
  25  T : ℝ    -- duration of rotation
  26  T_pos : 0 < T
  27
  28/-- Residual action S = π/2 - θ_s (geodesic length on Bloch sphere) -/
  29noncomputable def residualAction (rot : TwoBranchRotation) : ℝ :=
  30  π/2 - rot.θ_s
  31
  32/-- Residual norm ||R|| = dθ/dt integrated over the rotation -/
  33noncomputable def residualNorm (rot : TwoBranchRotation) : ℝ :=
  34  residualAction rot
  35
  36/-- Rate action A = -ln(sin θ_s) from eq (4.7) of Local-Collapse -/
  37noncomputable def rateAction (rot : TwoBranchRotation) : ℝ :=
  38  - Real.log (Real.sin rot.θ_s)
  39
  40/-- Rate action is positive for θ_s ∈ (0, π/2) -/
  41lemma rateAction_pos (rot : TwoBranchRotation) : 0 < rateAction rot := by
  42  unfold rateAction
  43  apply neg_pos.mpr
  44  have ⟨h1, h2⟩ := rot.θ_s_bounds
  45  have hsin_pos : 0 < Real.sin rot.θ_s :=
  46    sin_pos_of_pos_of_lt_pi h1 (by linarith : rot.θ_s < π)
  47  -- sin θ < 1 for 0 < θ < π/2
  48  have hsin_lt_one : Real.sin rot.θ_s < 1 := by
  49    have hx1 : -(π / 2) ≤ rot.θ_s := by linarith
  50    have hlt : rot.θ_s < π / 2 := h2
  51    have : Real.sin rot.θ_s < Real.sin (π / 2) :=
  52      sin_lt_sin_of_lt_of_le_pi_div_two hx1 le_rfl hlt