IndisputableMonolith.Gravity.SevenGaps.SourcedMinimizerSupDiameter

   1import IndisputableMonolith.Gravity.SevenGaps.HingeStationarityCore
   2
   3namespace IndisputableMonolith
   4namespace Gravity
   5namespace SevenGaps
   6namespace SourcedMinimizerSupDiameter
   7
   8open Set
   9
  10noncomputable section
  11
  12/-!
  13# Sourced-action approximate-minimizer sup-norm diameter
  14
  15MODEL flag (inherited from `HingeStationarityCore`): the deficit-source
  16coupling term `-(c/n) * sum_i t_i` inside `sourcedAction` is an explicit
  17constitutive MODEL input, not derived from the bare RecognitionLedger.
  18Everything proved ABOUT that action — including the diameter bound below —
  19is THEOREM.
  20-/
  21
  22/-- Helper: g(h) = sinh(s+h) - sinh s - h. -/
  23private noncomputable def g (s : ℝ) (h : ℝ) : ℝ :=
  24  Real.sinh (s + h) - Real.sinh s - h
  25
  26/-- Helper: F(h) = cosh(s+h) - cosh s - sinh s * h - h²/2. -/
  27private noncomputable def F (s : ℝ) (h : ℝ) : ℝ :=
  28  Real.cosh (s + h) - Real.cosh s - Real.sinh s * h - h ^ 2 / 2
  29
  30private theorem hasDerivAt_g (s h : ℝ) :
  31    HasDerivAt (g s) (Real.cosh (s + h) - 1) h := by
  32  have hsinh :
  33      HasDerivAt (fun x : ℝ => Real.sinh (s + x)) (Real.cosh (s + h)) h := by
  34    have hcomp :=
  35      (Real.hasDerivAt_sinh (s + h)).comp h ((hasDerivAt_id h).const_add s)
  36    simpa [Function.comp_def] using hcomp
  37  have hconst : HasDerivAt (fun _ : ℝ => Real.sinh s) 0 h := hasDerivAt_const h _
  38  have hid : HasDerivAt (fun x : ℝ => x) 1 h := hasDerivAt_id h
  39  have hsub := (hsinh.sub hconst).sub hid
  40  simpa [g] using hsub
  41
  42private theorem g_zero (s : ℝ) : g s 0 = 0 := by
  43  simp [g]
  44
  45private theorem g_monotone (s : ℝ) : Monotone (g s) := by
  46  refine monotone_of_deriv_nonneg (fun x => (hasDerivAt_g s x).differentiableAt) ?_
  47  intro x
  48  rw [(hasDerivAt_g s x).deriv]
  49  linarith [Real.one_le_cosh (s + x)]
  50
  51private theorem g_nonneg_of_nonneg (s h : ℝ) (hh : 0 ≤ h) : 0 ≤ g s h := by
  52  have := (g_monotone s) hh
  53  simpa [g_zero] using this
  54
  55private theorem g_nonpos_of_nonpos (s h : ℝ) (hh : h ≤ 0) : g s h ≤ 0 := by
  56  have := (g_monotone s) hh
  57  simpa [g_zero] using this
  58
  59private theorem hasDerivAt_F (s h : ℝ) : HasDerivAt (F s) (g s h) h := by
  60  have hcosh :
  61      HasDerivAt (fun x : ℝ => Real.cosh (s + x)) (Real.sinh (s + h)) h := by
  62    have hcomp :=
  63      (Real.hasDerivAt_cosh (s + h)).comp h ((hasDerivAt_id h).const_add s)
  64    simpa [Function.comp_def] using hcomp
  65  have hconst : HasDerivAt (fun _ : ℝ => Real.cosh s) 0 h := hasDerivAt_const h _
  66  have hlin : HasDerivAt (fun x : ℝ => Real.sinh s * x) (Real.sinh s) h := by
  67    simpa using (hasDerivAt_id h).const_mul (Real.sinh s)
  68  have hsq : HasDerivAt (fun x : ℝ => x ^ 2 / 2) h h := by
  69    have hpow := (hasDerivAt_pow 2 h).div_const 2
  70    convert hpow using 1
  71    ring
  72  have h1 := (hcosh.sub hconst).sub hlin
  73  have h2 := h1.sub hsq
  74  -- h2 : HasDerivAt (...fun form...) (sinh(s+h) - sinh s - h) h
  75  simpa [F, g] using h2
  76
  77private theorem F_zero (s : ℝ) : F s 0 = 0 := by
  78  simp [F]
  79
  80private theorem F_nonneg (s h : ℝ) : 0 ≤ F s h := by
  81  have hdiff : Differentiable ℝ (F s) := fun x => (hasDerivAt_F s x).differentiableAt
  82  have hcont : Continuous (F s) := hdiff.continuous
  83  have hmono : MonotoneOn (F s) (Ici (0 : ℝ)) := by
  84    refine monotoneOn_of_deriv_nonneg (convex_Ici 0) hcont.continuousOn
  85      hdiff.differentiableOn ?_
  86    intro x hx
  87    have hx0 : 0 < x := by
  88      have : x ∈ Ioi (0 : ℝ) := by rwa [interior_Ici] at hx
  89      exact this
  90    rw [(hasDerivAt_F s x).deriv]
  91    exact g_nonneg_of_nonneg s x hx0.le
  92  have hanti : AntitoneOn (F s) (Iic (0 : ℝ)) := by
  93    refine antitoneOn_of_deriv_nonpos (convex_Iic 0) hcont.continuousOn
  94      hdiff.differentiableOn ?_
  95    intro x hx
  96    have hx0 : x < 0 := by
  97      have : x ∈ Iio (0 : ℝ) := by rwa [interior_Iic] at hx
  98      exact this
  99    rw [(hasDerivAt_F s x).deriv]
 100    exact g_nonpos_of_nonpos s x hx0.le
 101  rcases le_total h 0 with hle | hge
 102  · -- h ≤ 0: antitone ⇒ F 0 ≤ F h
 103    have := hanti hle (le_rfl : (0 : ℝ) ≤ 0) hle
 104    -- this : F 0 ≤ F h? Wait AntitoneOn: x≤y → f y ≤ f x, so F 0 ≤ F h
 105    simpa [F_zero] using this
 106  · -- 0 ≤ h: monotone ⇒ F 0 ≤ F h
 107    have := hmono (le_rfl : (0 : ℝ) ≤ 0) hge hge
 108    simpa [F_zero] using this
 109
 110/-- Per-tick quadratic well at the stationary point s = arsinh a. -/
 111private theorem sourced_tick_quadratic_well (a t : ℝ) :
 112    Real.cosh t - 1 - a * t - (Real.cosh (Real.arsinh a) - 1 - a * Real.arsinh a)
 113      ≥ (1 / 2) * (t - Real.arsinh a) ^ 2 := by
 114  set s := Real.arsinh a
 115  set h := t - s with hh
 116  have hs : Real.sinh s = a := Real.sinh_arsinh a
 117  have hF := F_nonneg s h
 118  have ht : t = s + h := by simp [h]
 119  have hrewrite :
 120      Real.cosh t - 1 - a * t - (Real.cosh s - 1 - a * s)
 121        = Real.cosh (s + h) - Real.cosh s - Real.sinh s * h := by
 122    rw [ht, hs]
 123    ring
 124  have hge :
 125      Real.cosh (s + h) - Real.cosh s - Real.sinh s * h ≥ h ^ 2 / 2 := by
 126    have : F s h ≥ 0 := hF
 127    simp only [F] at this
 128    linarith
 129  calc
 130    Real.cosh t - 1 - a * t - (Real.cosh s - 1 - a * s)
 131        = Real.cosh (s + h) - Real.cosh s - Real.sinh s * h := hrewrite
 132    _ ≥ h ^ 2 / 2 := hge
 133    _ = (1 / 2) * (t - s) ^ 2 := by
 134          simp [h]
 135          ring
 136
 137/-- One-point distance from an eps-approximate minimizer to the well. -/
 138private theorem approx_tick_dist
 139    (n : ℕ) (c : ℝ) (eps : ℝ) (_heps : 0 ≤ eps)
 140    (u : Fin n → ℝ)
 141    (hu : sourcedAction n c u ≤ sourcedAction n c (sourcedMinimizer n c) + eps)
 142    (i : Fin n) :
 143    |u i - Real.arsinh (c / n)| ≤ Real.sqrt (2 * eps) := by
 144  set s := Real.arsinh (c / n)
 145  set a := c / n
 146  have hwell := sourced_tick_quadratic_well a (u i)
 147  have hexcess :
 148      sourcedAction n c u - sourcedAction n c (sourcedMinimizer n c) ≤ eps := by
 149    linarith [hu]
 150  have hsum :
 151      sourcedAction n c u - sourcedAction n c (sourcedMinimizer n c)
 152        = ∑ j : Fin n,
 153            ((Real.cosh (u j) - 1 - a * u j)
 154              - (Real.cosh s - 1 - a * s)) := by
 155    rw [sourcedAction_eq_sum, sourcedAction_eq_sum]
 156    simp only [sourcedMinimizer, a, s]
 157    rw [← Finset.sum_sub_distrib]
 158  have hterm_nonneg :
 159      ∀ j : Fin n,
 160        0 ≤
 161          (Real.cosh (u j) - 1 - a * u j)
 162            - (Real.cosh s - 1 - a * s) := by
 163    intro j
 164    have := sourced_pointwise_le a (u j)
 165    simp only [a, s] at this ⊢
 166    linarith
 167  have hsingle :
 168      (Real.cosh (u i) - 1 - a * u i) - (Real.cosh s - 1 - a * s)
 169        ≤ sourcedAction n c u - sourcedAction n c (sourcedMinimizer n c) := by
 170    rw [hsum]
 171    exact Finset.single_le_sum (fun j _ => hterm_nonneg j) (Finset.mem_univ i)
 172  have htick :
 173      (Real.cosh (u i) - 1 - a * u i) - (Real.cosh s - 1 - a * s) ≤ eps :=
 174    le_trans hsingle hexcess
 175  have hquad :
 176      (1 / 2 : ℝ) * (u i - s) ^ 2
 177        ≤ (Real.cosh (u i) - 1 - a * u i) - (Real.cosh s - 1 - a * s) := by
 178    simpa [s, a] using hwell
 179  have hsq : (u i - s) ^ 2 ≤ 2 * eps := by
 180    nlinarith [hquad, htick]
 181  exact Real.abs_le_sqrt hsq
 182
 183/-- **THEOREM (sourced-action approximate-minimizer sup-norm diameter).**
 184For any abstract global minimizer `m` of the sourced hinge action and any
 185two eps-approximate minimizers `u`, `v`, every tick satisfies
 186`|u i - v i| ≤ 2 * √(2ε)`. The deficit-source coupling inside
 187`sourcedAction` remains MODEL; the diameter bound is THEOREM. -/
 188theorem sourced_minimizer_sup_diameter
 189    (n : ℕ) (c : ℝ) (m : Fin n → ℝ)
 190    (hm : ∀ t, sourcedAction n c m ≤ sourcedAction n c t)
 191    (eps : ℝ) (heps : 0 ≤ eps)
 192    (u v : Fin n → ℝ)
 193    (hu : sourcedAction n c u ≤ sourcedAction n c m + eps)
 194    (hv : sourcedAction n c v ≤ sourcedAction n c m + eps)
 195    (i : Fin n) :
 196    |u i - v i| ≤ 2 * Real.sqrt (2 * eps) := by
 197  -- Step 1: parent uniqueness pins the abstract minimizer to the canonical well.
 198  have hparent := sourced_unique_minimizer n c m
 199  have hle_can : sourcedAction n c (sourcedMinimizer n c) ≤ sourcedAction n c m :=
 200    hparent.1
 201  have hle_m : sourcedAction n c m ≤ sourcedAction n c (sourcedMinimizer n c) :=
 202    hm (sourcedMinimizer n c)
 203  have heq_act :
 204      sourcedAction n c m = sourcedAction n c (sourcedMinimizer n c) :=
 205    le_antisymm hle_m hle_can
 206  have hm_eq : m = sourcedMinimizer n c := hparent.2 heq_act
 207  have hu' :
 208      sourcedAction n c u ≤ sourcedAction n c (sourcedMinimizer n c) + eps := by
 209    simpa [hm_eq] using hu
 210  have hv' :
 211      sourcedAction n c v ≤ sourcedAction n c (sourcedMinimizer n c) + eps := by
 212    simpa [hm_eq] using hv
 213  have bu := approx_tick_dist n c eps heps u hu' i
 214  have bv := approx_tick_dist n c eps heps v hv' i
 215  set s := Real.arsinh (c / n)
 216  have htri : |u i - v i| ≤ |u i - s| + |v i - s| := by
 217    calc
 218      |u i - v i| ≤ |u i - s| + |s - v i| := abs_sub_le (u i) s (v i)
 219      _ = |u i - s| + |v i - s| := by rw [abs_sub_comm s (v i)]
 220  have hsum : |u i - s| + |v i - s| ≤ Real.sqrt (2 * eps) + Real.sqrt (2 * eps) :=
 221    add_le_add bu bv
 222  have htwo :
 223      Real.sqrt (2 * eps) + Real.sqrt (2 * eps) = 2 * Real.sqrt (2 * eps) := by
 224    ring
 225  calc
 226    |u i - v i| ≤ |u i - s| + |v i - s| := htri
 227    _ ≤ Real.sqrt (2 * eps) + Real.sqrt (2 * eps) := hsum
 228    _ = 2 * Real.sqrt (2 * eps) := htwo
 229
 230end
 231
 232end SourcedMinimizerSupDiameter
 233end SevenGaps
 234end Gravity
 235end IndisputableMonolith
 236
 237#print axioms IndisputableMonolith.Gravity.SevenGaps.SourcedMinimizerSupDiameter.sourced_minimizer_sup_diameter
 238