IndisputableMonolith.Measurement.TwoBranchGeodesic

   1import Mathlib
   2import IndisputableMonolith.Measurement.PathAction
   3
   4/-!
   5# Two-Branch Quantum Measurement Geodesic
   6
   7This module formalizes the two-branch rotation geometry from
   8Local-Collapse §3 and Appendix A.
   9
  10Key results:
  11- Residual norm ||R|| = π/2 - θ_s (geodesic length)
  12- Rate action A = -ln(sin θ_s)
  13- Born weight: exp(-2A) = sin²(θ_s) = |α₂|²
  14-/
  15
  16namespace IndisputableMonolith
  17namespace Measurement
  18
  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
  53    simpa [Real.sin_pi_div_two] using this
  54  exact Real.log_neg hsin_pos hsin_lt_one
  55
  56/-- Born weight from rate action: exp(-2A) = sin²(θ_s) -/
  57theorem born_weight_from_rate (rot : TwoBranchRotation) :
  58  Real.exp (- 2 * rateAction rot) = (Real.sin rot.θ_s) ^ 2 := by
  59  unfold rateAction
  60  -- exp(-2*(-log(sin θ))) = exp(2 log(sin θ))
  61  have ⟨h1, h2⟩ := rot.θ_s_bounds
  62  have hsin_pos : 0 < Real.sin rot.θ_s :=
  63    sin_pos_of_pos_of_lt_pi h1 (by linarith : rot.θ_s < π)
  64  calc Real.exp (- 2 * (- Real.log (Real.sin rot.θ_s)))
  65      = Real.exp (2 * Real.log (Real.sin rot.θ_s)) := by ring_nf
  66      _ = Real.exp (Real.log ((Real.sin rot.θ_s) ^ 2)) := by
  67        congr 1
  68        exact (Real.log_pow (Real.sin rot.θ_s) 2).symm
  69      _ = (Real.sin rot.θ_s) ^ 2 := Real.exp_log (pow_pos hsin_pos 2)
  70
  71/-- Initial amplitude |α₂|² = sin²(θ_s) from geometry -/
  72noncomputable def initialAmplitudeSquared (rot : TwoBranchRotation) : ℝ :=
  73  (Real.sin rot.θ_s) ^ 2
  74
  75/-- Complement amplitude |α₁|² = cos²(θ_s) -/
  76noncomputable def complementAmplitudeSquared (rot : TwoBranchRotation) : ℝ :=
  77  (Real.cos rot.θ_s) ^ 2
  78
  79/-- Amplitudes sum to 1 (normalization) -/
  80theorem amplitudes_normalized (rot : TwoBranchRotation) :
  81  initialAmplitudeSquared rot + complementAmplitudeSquared rot = 1 := by
  82  unfold initialAmplitudeSquared complementAmplitudeSquared
  83  exact Real.sin_sq_add_cos_sq rot.θ_s
  84
  85/-- The geodesic is independent of time parameterization (reparameterization invariance) -/
  86theorem residual_action_invariant (rot : TwoBranchRotation) :
  87  residualAction rot = π/2 - rot.θ_s := rfl
  88
  89end Measurement
  90end IndisputableMonolith
  91