IndisputableMonolith.Gravity.SevenGaps.DescentPrincipleUniversality

   1import Mathlib
   2import IndisputableMonolith.Gravity.SevenGaps.StrainDescent
   3
   4/-!
   5# The descent principle: the metric is a choice, and the choice cannot matter
   6
   7## The question
   8
   9The carrier dynamics is a theorem: the gradient step on a hinge link's
  10strain space converges to the sourced least-cost carrier
  11(`StrainDescent`). That reduced the C2 stationarity premise to one
  12dynamical principle, that the substrate's strain state follows the steepest
  13descent of its total recognition cost. This module asks what that principle
  14actually costs, and answers in two parts.
  15
  16## Part one: "steepest" names a family, not a map
  17
  18Steepest descent is defined only relative to a metric on the strain space:
  19the flow of a cost `Φ` under a metric with positive weight `w` is
  20`ṫ = -w(t)·Φ'(t)`. Every positive `w` gives a flow with the same rest point
  21and the same descent sign, and different weights give different flows
  22(`metric_not_forced`: the Euclidean weight and the cost's own Hessian weight
  23`cosh` differ). So no derivation can single out "the" steepest descent
  24without first forcing a metric, and the metric is not fixed by the cost.
  25
  26## Part two: the choice cannot matter
  27
  28The reason this does not matter is the module's main theorem
  29(`cost_decreasing_dynamics_converges'`). Let `Φ` be the per-channel sourced
  30cost and `t* = arsinh a` its least-cost point. For **any** continuous map
  31`S` on the strain space with
  32
  33* `Φ (S t) < Φ t` whenever `t ≠ t*` (the dynamics strictly spends cost off
  34  the least-cost state),
  35
  36**every** orbit `S^[k] s₀` converges to `t*`, from every initial state.
  37No metric, no step size, no gradient, no convexity of `S`, and no rate.
  38The proof is a Lyapunov argument: the cost is coercive
  39(`sourceCost1_coercive`), so an orbit that never raises its cost is trapped
  40in a compact set; every limit point of the orbit has the same cost as its
  41own image, which by the descent hypothesis forces it to be `t*`.
  42
  43That the least-cost state is a rest state is not a further assumption:
  44continuity plus descent forces it (`rest_state_forced`). Continuity is the
  45one hypothesis doing real work, and it is load-bearing rather than
  46decorative: `continuity_is_load_bearing` exhibits a discontinuous dynamics
  47that spends cost strictly off the least-cost state, yet abandons that state
  48and oscillates forever.
  49
  50## What is proved (all THEOREM; 0 sorry, 0 admit, no new axiom, no
  51`native_decide`)
  52
  53* `sourceCost1_hasDerivAt`, `deriv_sourceCost1`: the cost's derivative is
  54  the residual `sinh t - a`, that is the recognition phase minus the source.
  55* `self_le_sinh`, `one_add_sq_div_two_le_cosh`: the growth bounds, from the
  56  integral machinery of `StrainDescent`.
  57* `sourceCost1_strictAntiOn` / `sourceCost1_strictMonoOn` /
  58  `sourceCost1_lt_of_ne`: the cost falls to `t*` and rises after it, so
  59  `t*` is the strict global minimum.
  60* `sourceCost1_coercive`: an explicit `N` beyond which the cost exceeds any
  61  named level.
  62* `descentField_zero_iff`, `descentField_descends`, `metric_not_forced`:
  63  part one.
  64* `cost_decreasing_dynamics_converges` and its minimal form
  65  `cost_decreasing_dynamics_converges'`: part two, the main theorem.
  66* `rest_state_forced`, `continuity_is_load_bearing`: the hypothesis
  67  accounting for part two.
  68* `strainStep1_continuous` and `strainStep1_converges_by_universality`: the
  69  banked gradient step is an instance of the main theorem, so the theorem
  70  is not vacuous and its hypotheses are inhabited by a real dynamics.
  71* `descent_principle_residue`: the two hypotheses bundled as the exact
  72  remaining adoption.
  73
  74## The honest verdict for (A3)
  75
  76The premise the C2 bridge still adopts is not "steepest descent", and not a
  77metric, and not a rate. It is exactly this: **the substrate's dynamics is
  78continuous and spends recognition cost off the least-cost state.** Every
  79such dynamics reaches the sourced least-cost carrier. Whether that residue
  80is itself derivable from the recognition kernel, rather than adopted as the
  81framework's variational posture, is OPEN, and it is now stated in the
  82weakest form under which the bridge's conclusion still follows.
  83-/
  84
  85namespace IndisputableMonolith
  86namespace Gravity
  87namespace SevenGaps
  88namespace StrainDescent
  89
  90open Real Set Filter
  91open scoped Topology
  92
  93noncomputable section
  94
  95/-! ## §1. The per-channel cost: derivative, shape, growth -/
  96
  97/-- The cost's derivative is the residual: the recognition phase minus the
  98source. -/
  99theorem sourceCost1_hasDerivAt (a s : ℝ) :
 100    HasDerivAt (sourceCost1 a) (strainResidual a s) s := by
 101  have h1 : HasDerivAt (fun s : ℝ => Real.cosh s - 1) (Real.sinh s) s :=
 102    (Real.hasDerivAt_cosh s).sub_const 1
 103  have h2 : HasDerivAt (fun s : ℝ => a * s) a s := by
 104    simpa using (hasDerivAt_id s).const_mul a
 105  have h := h1.sub h2
 106  simpa [sourceCost1, strainResidual] using h
 107
 108theorem deriv_sourceCost1 (a : ℝ) : deriv (sourceCost1 a) = strainResidual a := by
 109  funext s
 110  exact (sourceCost1_hasDerivAt a s).deriv
 111
 112theorem sourceCost1_continuous (a : ℝ) : Continuous (sourceCost1 a) := by
 113  unfold sourceCost1
 114  fun_prop
 115
 116/-- For `x ≥ 0`, `x ≤ sinh x`: the integral of `cosh ≥ 1`. -/
 117theorem self_le_sinh {x : ℝ} (hx : 0 ≤ x) : x ≤ Real.sinh x := by
 118  have hrepr : Real.sinh x - x = ∫ t in (0:ℝ)..x, (Real.cosh t - 1) := by
 119    rw [intervalIntegral.integral_sub
 120        (Real.continuous_cosh.intervalIntegrable _ _)
 121        (continuous_const.intervalIntegrable _ _),
 122      integral_cosh, intervalIntegral.integral_const]
 123    simp
 124  have hnn : (0:ℝ) ≤ ∫ t in (0:ℝ)..x, (Real.cosh t - 1) := by
 125    apply intervalIntegral.integral_nonneg hx
 126    intro t _
 127    have h1 : (1:ℝ) ≤ Real.cosh t := Real.one_le_cosh t
 128    simp [h1]
 129  linarith [hrepr, hnn]
 130
 131/-- The quadratic lower bound `1 + x²/2 ≤ cosh x`, all `x`. -/
 132theorem one_add_sq_div_two_le_cosh (x : ℝ) : 1 + x ^ 2 / 2 ≤ Real.cosh x := by
 133  have main : ∀ y : ℝ, 0 ≤ y → 1 + y ^ 2 / 2 ≤ Real.cosh y := by
 134    intro y hy
 135    have hrepr : Real.cosh y - 1 = ∫ t in (0:ℝ)..y, Real.sinh t := (integral_sinh y).symm
 136    have hmono : ∫ t in (0:ℝ)..y, (t : ℝ) ≤ ∫ t in (0:ℝ)..y, Real.sinh t := by
 137      apply intervalIntegral.integral_mono_on hy
 138        (continuous_id.intervalIntegrable _ _)
 139        (Real.continuous_sinh.intervalIntegrable _ _)
 140      intro t ht
 141      exact self_le_sinh ht.1
 142    rw [integral_id_half_sq] at hmono
 143    linarith [hrepr, hmono]
 144  rcases le_or_gt 0 x with hx | hx
 145  · exact main x hx
 146  · have h0 : 0 ≤ -x := le_of_lt (neg_pos.mpr hx)
 147    have h := main (-x) h0
 148    rw [Real.cosh_neg] at h
 149    norm_num at h
 150    exact h
 151
 152/-- Every level of the cost is exceeded outside an explicit interval. -/
 153theorem sourceCost1_coercive (a c : ℝ) :
 154    ∃ N : ℝ, 0 ≤ N ∧ ∀ t : ℝ, N ≤ |t| → c < sourceCost1 a t := by
 155  refine ⟨2 * (|a| + |c| + 2), by positivity, ?_⟩
 156  intro t ht
 157  have hq : |t| ^ 2 / 2 - |a| * |t| ≤ sourceCost1 a t := by
 158    have h1 := one_add_sq_div_two_le_cosh t
 159    have h2 : a * t ≤ |a| * |t| := by
 160      rw [← abs_mul]
 161      exact le_abs_self _
 162    have h3 : t ^ 2 = |t| ^ 2 := (sq_abs t).symm
 163    unfold sourceCost1
 164    linarith [h1, h2, h3]
 165  have habs : (0:ℝ) ≤ |t| := abs_nonneg t
 166  have hc : c ≤ |c| := le_abs_self c
 167  nlinarith [hq, ht, habs, hc, abs_nonneg a, abs_nonneg c]
 168
 169/-- The cost strictly rises above the least-cost point. -/
 170theorem sourceCost1_strictMonoOn (a : ℝ) :
 171    StrictMonoOn (sourceCost1 a) (Ici (Real.arsinh a)) := by
 172  apply strictMonoOn_of_deriv_pos (convex_Ici _)
 173    (sourceCost1_continuous a).continuousOn
 174  intro x hx
 175  rw [interior_Ici] at hx
 176  rw [deriv_sourceCost1]
 177  unfold strainResidual
 178  have h : Real.sinh (Real.arsinh a) < Real.sinh x := Real.sinh_strictMono hx
 179  rw [Real.sinh_arsinh] at h
 180  linarith
 181
 182/-- The cost strictly falls up to the least-cost point. -/
 183theorem sourceCost1_strictAntiOn (a : ℝ) :
 184    StrictAntiOn (sourceCost1 a) (Iic (Real.arsinh a)) := by
 185  apply strictAntiOn_of_deriv_neg (convex_Iic _)
 186    (sourceCost1_continuous a).continuousOn
 187  intro x hx
 188  rw [interior_Iic] at hx
 189  rw [deriv_sourceCost1]
 190  unfold strainResidual
 191  have h : Real.sinh x < Real.sinh (Real.arsinh a) := Real.sinh_strictMono hx
 192  rw [Real.sinh_arsinh] at h
 193  linarith
 194
 195/-- **THEOREM.** `arsinh a` is the strict global minimum of the cost. -/
 196theorem sourceCost1_lt_of_ne (a t : ℝ) (h : t ≠ Real.arsinh a) :
 197    sourceCost1 a (Real.arsinh a) < sourceCost1 a t := by
 198  rcases lt_or_gt_of_ne h with hlt | hgt
 199  · exact sourceCost1_strictAntiOn a (mem_Iic.mpr hlt.le) (mem_Iic.mpr le_rfl) hlt
 200  · exact sourceCost1_strictMonoOn a (mem_Ici.mpr le_rfl) (mem_Ici.mpr hgt.le) hgt
 201
 202theorem sourceCost1_min_le (a t : ℝ) :
 203    sourceCost1 a (Real.arsinh a) ≤ sourceCost1 a t := by
 204  by_cases h : t = Real.arsinh a
 205  · rw [h]
 206  · exact (sourceCost1_lt_of_ne a t h).le
 207
 208/-! ## §2. Part one: the metric is a choice -/
 209
 210/-- The descent field of the cost under a metric with weight `w`:
 211`ṫ = -w(t)·Φ'(t)`. The Euclidean metric is `w = 1`; the cost's own Hessian
 212metric is `w = cosh`. -/
 213def descentField (w : ℝ → ℝ) (a : ℝ) : ℝ → ℝ :=
 214  fun t => -(w t) * strainResidual a t
 215
 216/-- Every positive weight gives a field resting exactly at the least-cost
 217point. -/
 218theorem descentField_zero_iff {w : ℝ → ℝ} (hw : ∀ t, 0 < w t) (a t : ℝ) :
 219    descentField w a t = 0 ↔ t = Real.arsinh a := by
 220  unfold descentField
 221  constructor
 222  · intro h
 223    have hres : strainResidual a t = 0 := by
 224      rcases mul_eq_zero.mp h with h1 | h2
 225      · exact absurd h1 (by simpa using (hw t).ne')
 226      · exact h2
 227    unfold strainResidual at hres
 228    have : Real.sinh t = Real.sinh (Real.arsinh a) := by
 229      rw [Real.sinh_arsinh]
 230      linarith
 231    exact Real.sinh_injective this
 232  · intro h
 233    rw [h]
 234    unfold strainResidual
 235    rw [Real.sinh_arsinh]
 236    simp
 237
 238/-- Every positive weight gives a field that never raises the cost: the
 239field and the cost's derivative always have opposite signs. -/
 240theorem descentField_descends {w : ℝ → ℝ} (hw : ∀ t, 0 < w t) (a t : ℝ) :
 241    deriv (sourceCost1 a) t * descentField w a t ≤ 0 := by
 242  rw [deriv_sourceCost1]
 243  unfold descentField
 244  have h : strainResidual a t * (-(w t) * strainResidual a t)
 245      = -(w t) * strainResidual a t ^ 2 := by ring
 246  rw [h]
 247  have h1 : (0:ℝ) ≤ w t * strainResidual a t ^ 2 :=
 248    mul_nonneg (hw t).le (sq_nonneg _)
 249  linarith
 250
 251/-- **THEOREM (part one).** The metric is not forced: two positive weights,
 252the Euclidean one and the cost's own Hessian, give genuinely different
 253descent fields. So "steepest descent" names a family of dynamics, not one
 254map, and no derivation can produce a unique flow without first fixing a
 255metric. -/
 256theorem metric_not_forced :
 257    ∃ w₁ w₂ : ℝ → ℝ, (∀ t, 0 < w₁ t) ∧ (∀ t, 0 < w₂ t) ∧
 258      descentField w₁ 0 ≠ descentField w₂ 0 := by
 259  refine ⟨fun _ => 1, Real.cosh, fun _ => one_pos,
 260    fun t => lt_of_lt_of_le one_pos (Real.one_le_cosh t), ?_⟩
 261  intro hcon
 262  have h := congrFun hcon 1
 263  unfold descentField strainResidual at h
 264  simp only [sub_zero, neg_one_mul] at h
 265  -- h : -sinh 1 = -cosh 1 * sinh 1
 266  have hs : 0 < Real.sinh 1 := by
 267    have := self_le_sinh (show (0:ℝ) ≤ 1 by norm_num)
 268    linarith
 269  have hc : (1:ℝ) < Real.cosh 1 := by
 270    have := one_add_sq_div_two_le_cosh 1
 271    norm_num at this
 272    linarith
 273  nlinarith [h, hs, hc]
 274
 275/-! ## §3. Part two: any cost-decreasing dynamics reaches the carrier -/
 276
 277/-- **THEOREM (the main result).** Let `S` be any continuous dynamics on the
 278strain space that rests at the least-cost point and strictly spends cost
 279everywhere else. Then every orbit converges to the least-cost point.
 280
 281No metric, no step size, no gradient structure, no rate, and no convexity
 282of `S` is assumed. This is what makes the metric choice of part one
 283irrelevant: every member of the steepest-descent family, and every other
 284cost-decreasing dynamics whatsoever, reaches the same carrier. -/
 285theorem cost_decreasing_dynamics_converges (a : ℝ) (S : ℝ → ℝ)
 286    (hcont : Continuous S)
 287    (hrest : S (Real.arsinh a) = Real.arsinh a)
 288    (hdesc : ∀ t, t ≠ Real.arsinh a → sourceCost1 a (S t) < sourceCost1 a t)
 289    (s₀ : ℝ) :
 290    Tendsto (fun k => S^[k] s₀) atTop (𝓝 (Real.arsinh a)) := by
 291  set tstar := Real.arsinh a with htstar
 292  set Φ := sourceCost1 a with hΦ
 293  set u : ℕ → ℝ := fun k => S^[k] s₀ with hu
 294  have hΦcont : Continuous Φ := sourceCost1_continuous a
 295  have hstep : ∀ k, u (k + 1) = S (u k) := by
 296    intro k
 297    simp [hu, Function.iterate_succ_apply']
 298  -- The cost never rises along an orbit.
 299  have hle : ∀ t, Φ (S t) ≤ Φ t := by
 300    intro t
 301    by_cases h : t = tstar
 302    · rw [h, hrest]
 303    · exact (hdesc t h).le
 304  have hanti : Antitone (fun k => Φ (u k)) := by
 305    apply antitone_nat_of_succ_le
 306    intro k
 307    rw [hstep k]
 308    exact hle (u k)
 309  have hlb : ∀ k, Φ tstar ≤ Φ (u k) := fun k => sourceCost1_min_le a (u k)
 310  have hbdd : BddBelow (range fun k => Φ (u k)) := ⟨Φ tstar, by
 311    rintro y ⟨k, rfl⟩
 312    exact hlb k⟩
 313  -- The cost along the orbit converges to some level L.
 314  set L := ⨅ k, Φ (u k) with hL
 315  have hconv : Tendsto (fun k => Φ (u k)) atTop (𝓝 L) :=
 316    tendsto_atTop_ciInf hanti hbdd
 317  -- The orbit is trapped in a compact interval.
 318  obtain ⟨N, hN0, hNc⟩ := sourceCost1_coercive a (Φ s₀)
 319  have hmem : ∀ k, u k ∈ Icc (-N) N := by
 320    intro k
 321    have hcost : Φ (u k) ≤ Φ s₀ := by
 322      have h0 : Φ (u 0) = Φ s₀ := by simp [hu]
 323      calc Φ (u k) ≤ Φ (u 0) := hanti (Nat.zero_le k)
 324        _ = Φ s₀ := h0
 325    have habs : |u k| < N := by
 326      by_contra hcon
 327      push_neg at hcon
 328      exact absurd hcost (not_le.mpr (hNc (u k) hcon))
 329    rw [mem_Icc]
 330    constructor
 331    · linarith [neg_abs_le (u k), habs]
 332    · linarith [le_abs_self (u k), habs]
 333  -- Every limit point of the orbit is the least-cost point.
 334  apply tendsto_of_subseq_tendsto
 335  intro ns hns
 336  obtain ⟨z, hzmem, ms, hms, hlim⟩ :=
 337    isCompact_Icc.tendsto_subseq (x := fun n => u (ns n)) (fun n => hmem (ns n))
 338  have hidx : Tendsto (fun n => ns (ms n)) atTop atTop :=
 339    hns.comp hms.tendsto_atTop
 340  -- The subsequence's cost tends to both Φ z and L, so Φ z = L.
 341  have hΦz : Tendsto (fun n => Φ (u (ns (ms n)))) atTop (𝓝 (Φ z)) :=
 342    (hΦcont.tendsto z).comp hlim
 343  have hΦL : Tendsto (fun n => Φ (u (ns (ms n)))) atTop (𝓝 L) := hconv.comp hidx
 344  have hzL : Φ z = L := tendsto_nhds_unique hΦz hΦL
 345  -- The shifted subsequence's cost tends to both Φ (S z) and L.
 346  have hshiftlim : Tendsto (fun n => u (ns (ms n) + 1)) atTop (𝓝 (S z)) := by
 347    have : (fun n => u (ns (ms n) + 1)) = fun n => S (u (ns (ms n))) := by
 348      funext n
 349      exact hstep (ns (ms n))
 350    rw [this]
 351    exact (hcont.tendsto z).comp hlim
 352  have hΦSz : Tendsto (fun n => Φ (u (ns (ms n) + 1))) atTop (𝓝 (Φ (S z))) :=
 353    (hΦcont.tendsto (S z)).comp hshiftlim
 354  have hΦSL : Tendsto (fun n => Φ (u (ns (ms n) + 1))) atTop (𝓝 L) := by
 355    apply hconv.comp
 356    exact tendsto_atTop_mono (fun n => Nat.le_succ (ns (ms n))) hidx
 357  have hSzL : Φ (S z) = L := tendsto_nhds_unique hΦSz hΦSL
 358  -- Equal cost before and after the step forces the least-cost point.
 359  have hz : z = tstar := by
 360    by_contra hcon
 361    have := hdesc z hcon
 362    rw [hSzL, hzL] at this
 363    exact lt_irrefl L this
 364  rw [hz] at hlim
 365  exact ⟨ms, hlim⟩
 366
 367/-! ## §3b. The rest state is not a separate assumption -/
 368
 369/-- **THEOREM.** A continuous dynamics that spends cost off the least-cost
 370state must rest at it. So the rest hypothesis of the main theorem is not an
 371extra adoption: it is a consequence of the other two. -/
 372theorem rest_state_forced (a : ℝ) (S : ℝ → ℝ)
 373    (hcont : Continuous S)
 374    (hdesc : ∀ t, t ≠ Real.arsinh a → sourceCost1 a (S t) < sourceCost1 a t) :
 375    S (Real.arsinh a) = Real.arsinh a := by
 376  set tstar := Real.arsinh a with htstar
 377  set Φ := sourceCost1 a with hΦ
 378  have hΦcont : Continuous Φ := sourceCost1_continuous a
 379  set p : ℕ → ℝ := fun n => tstar + 1 / (n + 1) with hp
 380  have hpne : ∀ n, p n ≠ tstar := by
 381    intro n hcon
 382    have hpos : (0:ℝ) < 1 / ((n : ℝ) + 1) := by positivity
 383    simp only [hp] at hcon
 384    linarith
 385  have hptend : Tendsto p atTop (𝓝 tstar) := by
 386    have h0 : Tendsto (fun n : ℕ => 1 / ((n : ℝ) + 1)) atTop (𝓝 0) :=
 387      tendsto_one_div_add_atTop_nhds_zero_nat
 388    simpa [hp] using (tendsto_const_nhds (x := tstar) (f := atTop)).add h0
 389  have hA : Tendsto (fun n => Φ (S (p n))) atTop (𝓝 (Φ (S tstar))) :=
 390    ((hΦcont.comp hcont).tendsto tstar).comp hptend
 391  have hB : Tendsto (fun n => Φ (p n)) atTop (𝓝 (Φ tstar)) :=
 392    (hΦcont.tendsto tstar).comp hptend
 393  have hle : Φ (S tstar) ≤ Φ tstar :=
 394    le_of_tendsto_of_tendsto' hA hB (fun n => (hdesc (p n) (hpne n)).le)
 395  by_contra hcon
 396  exact absurd hle (not_le.mpr (sourceCost1_lt_of_ne a (S tstar) hcon))
 397
 398/-- **THEOREM (the main result, minimal form).** Continuity plus strict cost
 399spending off the least-cost state is by itself enough: every orbit
 400converges to the sourced least-cost carrier. -/
 401theorem cost_decreasing_dynamics_converges' (a : ℝ) (S : ℝ → ℝ)
 402    (hcont : Continuous S)
 403    (hdesc : ∀ t, t ≠ Real.arsinh a → sourceCost1 a (S t) < sourceCost1 a t)
 404    (s₀ : ℝ) :
 405    Tendsto (fun k => S^[k] s₀) atTop (𝓝 (Real.arsinh a)) :=
 406  cost_decreasing_dynamics_converges a S hcont (rest_state_forced a S hcont hdesc)
 407    hdesc s₀
 408
 409/-- **THEOREM.** Continuity is load-bearing, not decoration. Dropping it
 410breaks both the rest state and the conclusion: this dynamics spends cost
 411strictly off the least-cost state, yet abandons that state and oscillates
 412forever. -/
 413theorem continuity_is_load_bearing :
 414    ∃ S : ℝ → ℝ,
 415      (∀ t, t ≠ Real.arsinh 0 → sourceCost1 0 (S t) < sourceCost1 0 t) ∧
 416      S (Real.arsinh 0) ≠ Real.arsinh 0 ∧
 417      ¬ Tendsto (fun k => S^[k] (Real.arsinh 0)) atTop (𝓝 (Real.arsinh 0)) := by
 418  classical
 419  have harsinh : Real.arsinh 0 = 0 := by
 420    simpa using Real.arsinh_zero
 421  refine ⟨fun t => if t = 0 then 5 else 0, ?_, ?_, ?_⟩
 422  · intro t ht
 423    rw [harsinh] at ht
 424    have h2 : (1:ℝ) < Real.cosh t := by
 425      have hq := one_add_sq_div_two_le_cosh t
 426      have hsq : 0 < t ^ 2 := by positivity
 427      linarith
 428    have hgoal : sourceCost1 0 (0:ℝ) < sourceCost1 0 t := by
 429      unfold sourceCost1
 430      rw [Real.cosh_zero]
 431      linarith
 432    simpa only [if_neg ht] using hgoal
 433  · rw [harsinh]
 434    norm_num
 435  · rw [harsinh]
 436    intro hcon
 437    -- the orbit alternates 0, 5, 0, 5, ... so it also tends to 5
 438    have hodd : ∀ k : ℕ, (fun t : ℝ => if t = 0 then 5 else 0)^[2 * k + 1] 0 = 5 := by
 439      intro k
 440      induction k with
 441      | zero => norm_num
 442      | succ m ih =>
 443        have h2 : 2 * (m + 1) + 1 = (2 * m + 1) + 2 := by ring
 444        have hff : (fun t : ℝ => if t = 0 then 5 else 0)^[2] 0 = 0 := by norm_num
 445        rw [h2, Function.iterate_add_apply, hff, ih]
 446    have hidx : Tendsto (fun k : ℕ => 2 * k + 1) atTop atTop :=
 447      tendsto_atTop_mono (fun k => by omega : ∀ k : ℕ, k ≤ 2 * k + 1) tendsto_id
 448    have hsub := hcon.comp hidx
 449    rw [Function.comp_def] at hsub
 450    simp only [hodd] at hsub
 451    have := tendsto_nhds_unique hsub (tendsto_const_nhds (x := (5:ℝ)) (f := atTop))
 452    norm_num at this
 453
 454/-! ## §4. The banked gradient step is an instance -/
 455
 456theorem strainResidual_continuous (a : ℝ) : Continuous (strainResidual a) := by
 457  unfold strainResidual
 458  fun_prop
 459
 460theorem strainEnvelope_continuous (a : ℝ) : Continuous (strainEnvelope a) := by
 461  unfold strainEnvelope
 462  have h := strainResidual_continuous a
 463  fun_prop
 464
 465theorem strainStepSize_continuous (a : ℝ) : Continuous (strainStepSize a) := by
 466  unfold strainStepSize
 467  exact (strainEnvelope_continuous a).inv₀ (fun s => (strainEnvelope_pos a s).ne')
 468
 469/-- The banked gradient step is continuous. -/
 470theorem strainStep1_continuous (a : ℝ) : Continuous (strainStep1 a) := by
 471  unfold strainStep1
 472  exact continuous_id.sub
 473    ((strainStepSize_continuous a).mul (strainResidual_continuous a))
 474
 475/-- **THEOREM.** The banked gradient step satisfies the main theorem's
 476hypotheses, so the theorem is inhabited by a real dynamics and its
 477conclusion reproduces the convergence proved directly in `StrainDescent`. -/
 478theorem strainStep1_converges_by_universality (a s₀ : ℝ) :
 479    Tendsto (fun k => (strainStep1 a)^[k] s₀) atTop (𝓝 (Real.arsinh a)) := by
 480  apply cost_decreasing_dynamics_converges a (strainStep1 a)
 481    (strainStep1_continuous a)
 482  · exact (step_fixed_iff_arsinh a (Real.arsinh a)).mpr rfl
 483  · intro t ht
 484    apply descent_one_dim_lt a t
 485    intro hres
 486    apply ht
 487    exact (step_fixed_iff_arsinh a t).mp (by
 488      unfold strainStep1
 489      rw [hres]
 490      ring)
 491
 492/-! ## §5. The residue: what the C2 bridge still adopts -/
 493
 494/-- **THEOREM (the exact remaining adoption).** The C2 stationarity premise
 495is discharged by exactly these three properties of the substrate's strain
 496dynamics: continuity, resting at least cost, and never gaining cost off
 497that rest state. Nothing about metrics, gradients, rates, or steepest
 498descent survives into the residue. -/
 499theorem descent_principle_residue (a : ℝ) (S : ℝ → ℝ)
 500    (hcont : Continuous S)
 501    (hrest : S (Real.arsinh a) = Real.arsinh a)
 502    (hdesc : ∀ t, t ≠ Real.arsinh a → sourceCost1 a (S t) < sourceCost1 a t) :
 503    ∀ s₀ : ℝ, Tendsto (fun k => S^[k] s₀) atTop (𝓝 (Real.arsinh a)) ∧
 504      (∀ k : ℕ, sourceCost1 a (S^[k + 1] s₀) ≤ sourceCost1 a (S^[k] s₀)) := by
 505  intro s₀
 506  refine ⟨cost_decreasing_dynamics_converges a S hcont hrest hdesc s₀, ?_⟩
 507  intro k
 508  rw [Function.iterate_succ_apply']
 509  by_cases h : (S^[k] s₀) = Real.arsinh a
 510  · rw [h, hrest]
 511  · exact (hdesc _ h).le
 512
 513/-- The link's componentwise reading: each channel of a hinge reaches the
 514sourced minimizer under any cost-decreasing dynamics on its strain. -/
 515theorem link_channels_converge (n : ℕ) (c : ℝ) (S : ℝ → ℝ)
 516    (hcont : Continuous S)
 517    (hrest : S (Real.arsinh (c / n)) = Real.arsinh (c / n))
 518    (hdesc : ∀ t, t ≠ Real.arsinh (c / n) →
 519      sourceCost1 (c / n) (S t) < sourceCost1 (c / n) t)
 520    (t : Fin n → ℝ) (i : Fin n) :
 521    Tendsto (fun k => S^[k] (t i)) atTop (𝓝 (sourcedMinimizer n c i)) :=
 522  cost_decreasing_dynamics_converges (c / n) S hcont hrest hdesc (t i)
 523
 524end
 525
 526end StrainDescent
 527end SevenGaps
 528end Gravity
 529end IndisputableMonolith
 530