IndisputableMonolith.Measurement.C2ABridge

   1import Mathlib
   2import IndisputableMonolith.Measurement.PathAction
   3import IndisputableMonolith.Measurement.TwoBranchGeodesic
   4import IndisputableMonolith.Measurement.KernelMatch
   5
   6/-!
   7# The C = 2A Measurement Bridge
   8
   9This module proves the central equivalence between recognition cost C
  10and the residual-model rate action A.
  11
  12Main theorem: For any two-branch geodesic rotation,
  13  C = 2A  (exactly)
  14
  15This establishes that quantum measurement and recognition are governed
  16by the same unique cost functional J.
  17-/
  18
  19namespace IndisputableMonolith
  20namespace Measurement
  21
  22open Real Cost
  23
  24/-! ## Improper Integral Axioms -/
  25
  26
  27/-- Construct recognition path from geodesic rotation using recognition profile -/
  28noncomputable def pathFromRotation (rot : TwoBranchRotation) : RecognitionPath where
  29  T := π/2 - rot.θ_s
  30  T_pos := by
  31    have ⟨_, h2⟩ := rot.θ_s_bounds
  32    linarith
  33  rate := fun ϑ => recognitionProfile (ϑ + rot.θ_s)
  34  rate_pos := by
  35    intro t ht
  36    apply recognitionProfile_pos
  37    have ⟨h1, h2⟩ := rot.θ_s_bounds
  38    constructor
  39    · -- 0 ≤ t + θ_s
  40      have := ht.1
  41      linarith
  42    · -- t + θ_s ≤ π/2
  43      have ht' : t ≤ π/2 - rot.θ_s := ht.2
  44      have := add_le_add_right ht' rot.θ_s
  45      simpa [add_comm, add_left_comm, add_assoc, sub_eq_add_neg] using this
  46
  47/-- The integral of tan from θ_s to π/2 equals -ln(sin θ_s) -/
  48theorem integral_cot_from_theta (θ_s : ℝ) (hθ : 0 < θ_s ∧ θ_s < π/2) :
  49  ∫ θ in θ_s..(π/2), Real.cot θ = - Real.log (Real.sin θ_s) := by
  50  -- Standard calculus result: ∫ cot θ dθ = log(sin θ) + C.
  51  -- We prove it via FTC on `f(θ) = log(sin θ)` over `[θ_s, π/2]`.
  52  let f : ℝ → ℝ := fun θ => Real.log (Real.sin θ)
  53
  54  have hpi2ltpi : (Real.pi / 2 : ℝ) < Real.pi := by nlinarith [Real.pi_pos]
  55
  56  have hsin_ne0_uIcc : ∀ x ∈ Set.uIcc θ_s (π/2), Real.sin x ≠ 0 := by
  57    intro x hx
  58    have hx' : θ_s ≤ x ∧ x ≤ π/2 := by
  59      rcases Set.mem_uIcc.mp hx with hx' | hx'
  60      · exact hx'
  61      · exfalso
  62        have : (π/2 : ℝ) ≤ θ_s := le_trans hx'.1 hx'.2
  63        exact (not_le_of_lt hθ.2) this
  64    have hxpos : 0 < x := lt_of_lt_of_le hθ.1 hx'.1
  65    have hxltpi : x < Real.pi := lt_of_le_of_lt hx'.2 hpi2ltpi
  66    exact ne_of_gt (Real.sin_pos_of_pos_of_lt_pi hxpos hxltpi)
  67
  68  have hderiv_eq_cot_uIoc : Set.EqOn (fun x => deriv f x) (fun x => Real.cot x) (Set.uIoc θ_s (π/2)) := by
  69    intro x hx
  70    have hx' : θ_s < x ∧ x ≤ π/2 := by
  71      rcases Set.mem_uIoc.mp hx with hx' | hx'
  72      · exact hx'
  73      · exfalso
  74        have : (π/2 : ℝ) ≤ θ_s := le_trans (le_of_lt hx'.1) hx'.2
  75        exact (not_le_of_lt hθ.2) this
  76    have hxpos : 0 < x := lt_of_lt_of_le hθ.1 (le_of_lt hx'.1)
  77    have hxltpi : x < Real.pi := lt_of_le_of_lt hx'.2 hpi2ltpi
  78    have hsx : Real.sin x ≠ 0 := ne_of_gt (Real.sin_pos_of_pos_of_lt_pi hxpos hxltpi)
  79    have hlog : HasDerivAt Real.log (Real.sin x)⁻¹ (Real.sin x) := Real.hasDerivAt_log hsx
  80    have hsin : HasDerivAt Real.sin (Real.cos x) x := Real.hasDerivAt_sin x
  81    have hcomp :
  82        HasDerivAt (fun t => Real.log (Real.sin t)) ((Real.sin x)⁻¹ * Real.cos x) x :=
  83      (HasDerivAt.comp x hlog hsin)
  84    -- Turn the computed derivative into `deriv f x = cot x`.
  85    have hderiv : deriv (fun t => Real.log (Real.sin t)) x = (Real.sin x)⁻¹ * Real.cos x := hcomp.deriv
  86    have hmul_to_div : (Real.sin x)⁻¹ * Real.cos x = Real.cos x / Real.sin x := by
  87      simp [div_eq_mul_inv, mul_comm, mul_left_comm, mul_assoc]
  88    calc
  89      deriv f x = (Real.sin x)⁻¹ * Real.cos x := by simpa [f] using hderiv
  90      _ = Real.cos x / Real.sin x := hmul_to_div
  91      _ = Real.cot x := by simpa using (Real.cot_eq_cos_div_sin x).symm
  92
  93  have hdiff : ∀ x ∈ Set.uIcc θ_s (π/2), DifferentiableAt ℝ f x := by
  94    intro x hx
  95    have hsx : Real.sin x ≠ 0 := hsin_ne0_uIcc x hx
  96    have hlog : HasDerivAt Real.log (Real.sin x)⁻¹ (Real.sin x) := Real.hasDerivAt_log hsx
  97    have hsin : HasDerivAt Real.sin (Real.cos x) x := Real.hasDerivAt_sin x
  98    have hcomp : HasDerivAt (fun t => Real.log (Real.sin t)) ((Real.sin x)⁻¹ * Real.cos x) x :=
  99      (HasDerivAt.comp x hlog hsin)
 100    -- `f` is definitionally the same function.
 101    simpa [f] using hcomp.differentiableAt
 102
 103  have hCotCont : ContinuousOn (fun x => Real.cot x) (Set.uIcc θ_s (π/2)) := by
 104    -- On `[θ_s, π/2]` we have `sin x ≠ 0`, so `cot x = cos x / sin x` is continuous.
 105    have hcos : ContinuousOn Real.cos (Set.uIcc θ_s (π/2)) :=
 106      (Real.continuous_cos.continuousOn)
 107    have hsin : ContinuousOn Real.sin (Set.uIcc θ_s (π/2)) :=
 108      (Real.continuous_sin.continuousOn)
 109    have hsin_ne0 : ∀ x ∈ Set.uIcc θ_s (π/2), Real.sin x ≠ 0 := hsin_ne0_uIcc
 110    have hdiv : ContinuousOn (fun x => Real.cos x / Real.sin x) (Set.uIcc θ_s (π/2)) :=
 111      (hcos.div hsin hsin_ne0)
 112    simpa [Real.cot_eq_cos_div_sin] using hdiv
 113
 114  have hCotInt : IntervalIntegrable (fun x => Real.cot x) MeasureTheory.volume θ_s (π/2) :=
 115    hCotCont.intervalIntegrable
 116
 117  have hDerivInt : IntervalIntegrable (fun x => deriv f x) MeasureTheory.volume θ_s (π/2) := by
 118    have hEq : Set.EqOn (fun x => Real.cot x) (fun x => deriv f x) (Set.uIoc θ_s (π/2)) := by
 119      intro x hx
 120      simpa using (hderiv_eq_cot_uIoc hx).symm
 121    exact (IntervalIntegrable.congr hEq) hCotInt
 122
 123  have hFTC :
 124      ∫ x in θ_s..(π/2), deriv f x = f (π/2) - f θ_s :=
 125    intervalIntegral.integral_deriv_eq_sub (a := θ_s) (b := (π/2)) hdiff hDerivInt
 126
 127  have hcongr :
 128      (∫ x in θ_s..(π/2), Real.cot x) = (∫ x in θ_s..(π/2), deriv f x) := by
 129    have h_ae :
 130        ∀ᵐ x ∂MeasureTheory.volume, x ∈ Set.uIoc θ_s (π/2) → Real.cot x = deriv f x := by
 131      refine Filter.Eventually.of_forall ?_
 132      intro x hx
 133      exact (hderiv_eq_cot_uIoc hx).symm
 134    simpa using
 135      (intervalIntegral.integral_congr_ae (μ := MeasureTheory.volume) (a := θ_s) (b := (π/2))
 136        (f := fun x => Real.cot x) (g := fun x => deriv f x) h_ae)
 137
 138  -- Finish: evaluate endpoints.
 139  have hsθ : Real.sin θ_s ≠ 0 := by
 140    have hθltpi : θ_s < Real.pi := lt_of_lt_of_le hθ.2 (le_of_lt hpi2ltpi)
 141    exact ne_of_gt (Real.sin_pos_of_pos_of_lt_pi hθ.1 hθltpi)
 142
 143  calc
 144    ∫ x in θ_s..(π/2), Real.cot x
 145        = ∫ x in θ_s..(π/2), deriv f x := hcongr
 146    _ = f (π/2) - f θ_s := hFTC
 147    _ = Real.log (Real.sin (π/2)) - Real.log (Real.sin θ_s) := by rfl
 148    _ = - Real.log (Real.sin θ_s) := by simp [Real.sin_pi_div_two]
 149
 150/-- Main C=2A Bridge Theorem:
 151    The recognition action for the constructed path equals twice the rate action -/
 152theorem measurement_bridge_C_eq_2A (rot : TwoBranchRotation) :
 153  pathAction (pathFromRotation rot) = 2 * rateAction rot := by
 154  unfold pathAction pathFromRotation rateAction
 155  simp
 156  have hkernel : ∫ ϑ in (0)..(π/2 - rot.θ_s),
 157                   Jcost (recognitionProfile (ϑ + rot.θ_s)) =
 158                2 * ∫ ϑ in (0)..(π/2 - rot.θ_s), Real.cot (ϑ + rot.θ_s) :=
 159    kernel_integral_match rot.θ_s rot.θ_s_bounds
 160  rw [hkernel]
 161  have h_subst :
 162      ∫ ϑ in (0)..(π/2 - rot.θ_s), Real.cot (ϑ + rot.θ_s)
 163        = ∫ θ in rot.θ_s..(π/2), Real.cot θ := by
 164    simpa [sub_eq_add_neg, add_comm, add_left_comm, add_assoc]
 165      using
 166        (intervalIntegral.integral_comp_add_right
 167          (a := (0 : ℝ)) (b := π/2 - rot.θ_s)
 168          (f := fun θ => Real.cot θ) (d := rot.θ_s))
 169  have hI := integral_cot_from_theta rot.θ_s rot.θ_s_bounds
 170  have htan :
 171      ∫ ϑ in (0)..(π/2 - rot.θ_s), Real.cot (ϑ + rot.θ_s)
 172        = - Real.log (Real.sin rot.θ_s) := by
 173    simpa [h_subst] using hI
 174  simp [htan, two_mul, mul_left_comm, mul_assoc]
 175
 176/-- Weight bridge: w = exp(-C) = exp(-2A) -/
 177theorem weight_bridge (rot : TwoBranchRotation) :
 178  pathWeight (pathFromRotation rot) = Real.exp (- 2 * rateAction rot) := by
 179  unfold pathWeight
 180  rw [measurement_bridge_C_eq_2A]
 181  congr 1
 182  ring
 183
 184/-- Weight equals Born probability: exp(-2A) = |α₂|² -/
 185theorem weight_equals_born (rot : TwoBranchRotation) :
 186  pathWeight (pathFromRotation rot) = initialAmplitudeSquared rot := by
 187  unfold pathWeight initialAmplitudeSquared
 188  rw [measurement_bridge_C_eq_2A]
 189  have h := Measurement.born_weight_from_rate rot
 190  have hWeight :
 191      Real.exp (-(2 * rateAction rot)) = initialAmplitudeSquared rot := by
 192    simpa [rateAction, Measurement.initialAmplitudeSquared] using h
 193  simpa using hWeight
 194
 195/-- Amplitude bridge modulus: |𝒜| = exp(-A) -/
 196theorem amplitude_modulus_bridge (rot : TwoBranchRotation) (φ : ℝ) :
 197  ‖pathAmplitude (pathFromRotation rot) φ‖ = Real.exp (- rateAction rot) := by
 198  unfold pathAmplitude
 199  have hExpReal :
 200      ‖Complex.exp (-(pathAction (pathFromRotation rot)) / 2)‖ =
 201        Real.exp (-(pathAction (pathFromRotation rot)) / 2) := by
 202    simpa using Complex.norm_exp_ofReal (-(pathAction (pathFromRotation rot)) / 2)
 203  have hExpI :
 204      ‖Complex.exp (φ * Complex.I)‖ = 1 := by
 205    simpa using Complex.norm_exp_ofReal_mul_I φ
 206  have hAction :
 207      -(pathAction (pathFromRotation rot)) / 2 = - rateAction rot := by
 208    have h := measurement_bridge_C_eq_2A rot
 209    calc
 210      -(pathAction (pathFromRotation rot)) / 2
 211          = -(2 * rateAction rot) / 2 := by simpa [h]
 212      _ = - rateAction rot := by ring
 213  calc
 214    ‖Complex.exp (-(pathAction (pathFromRotation rot)) / 2)
 215        * Complex.exp (φ * Complex.I)‖
 216        = ‖Complex.exp (-(pathAction (pathFromRotation rot)) / 2)‖ *
 217          ‖Complex.exp (φ * Complex.I)‖ := by simpa using norm_mul _ _
 218    _ = Real.exp (-(pathAction (pathFromRotation rot)) / 2) * 1 := by
 219        simpa [hExpReal, hExpI]
 220    _ = Real.exp (- rateAction rot) := by
 221        simpa [hAction]
 222
 223end Measurement
 224end IndisputableMonolith
 225