IndisputableMonolith.Gravity.SevenGaps.StrainDynamicsKernelReach

   1import Mathlib
   2import IndisputableMonolith.Cost
   3import IndisputableMonolith.Cost.FunctionalEquation
   4import IndisputableMonolith.Cost.SymplecticAction
   5import IndisputableMonolith.Gravity.SevenGaps.DescentPrincipleUniversality
   6
   7/-!
   8# How far the recognition kernel reaches: it fixes the cost, not the motion
   9
  10## The question
  11
  12The C2 bridge's stationarity premise is reduced to its weakest sufficient
  13form: the substrate's strain dynamics is continuous and strictly lowers
  14recognition cost at every state other than the least-cost state
  15(`DescentPrincipleUniversality`). This module asks whether that residue is
  16forced by the recognition kernel, and answers: no, and for a reason that is
  17structural rather than accidental.
  18
  19## What the kernel says about cost
  20
  21The kernel's cost content is exactly the premise package of
  22`law_of_logic_forces_jcost`: a cost is reciprocal, normalized, satisfies the
  23recognition composition law, is calibrated to unit log curvature, and is
  24continuous on the positive ratios. Those five premises force the cost to be
  25`J`, and `J` satisfies all five (`jcost_kernelCostContent`).
  26
  27Every one of them is a statement about the cost assigned to a single ratio.
  28None quantifies over a map on the ratio ledger, over a sequence of postings,
  29or over anything that changes. The kernel fixes what a configuration costs.
  30It does not say how a configuration moves.
  31
  32## The reach wall
  33
  34That gap is not a formality, and the counterexample is not contrived: it is
  35the ledger's own reciprocal involution `x ↦ 1/x`, which in the strain
  36coordinate is `t ↦ -t`. Its invariance is precisely the reciprocity premise
  37that makes the cost `J` in the first place. It is continuous, it preserves
  38bare recognition cost exactly (`reciprocalInvolution_preserves_cost`), and
  39from any nonzero strain its orbit oscillates forever without ever reaching
  40the carrier (`reciprocalInvolution_never_reaches`). So the single most
  41canonical motion on the ratio ledger satisfies everything the kernel says
  42and refutes the residue
  43(`kernel_cost_content_does_not_entail_cost_spending`).
  44
  45## The named postulate
  46
  47What the C2 bridge adopts is therefore stated here as an explicit object,
  48the honest analog of an action principle:
  49
  50`CostSpendingSubstrate a` = a continuous map on the strain space that
  51strictly lowers the sourced cost at every state other than the least-cost
  52state.
  53
  54It is proved **consistent** (`costSpendingSubstrate_nonempty`: the banked
  55gradient step inhabits it, so the postulate is not empty and does not prove
  56everything), **sufficient** (`CostSpendingSubstrate.reaches_carrier`: every
  57orbit of every inhabitant reaches the sourced least-cost carrier), and
  58**not determining** (`residue_has_two_models`, `no_unique_dynamics_from_residue`:
  59it has at least two distinct models, so any principle naming a single flow,
  60steepest descent in a fixed metric included, is strictly stronger than what
  61the bridge needs).
  62
  63## What is proved (all THEOREM; 0 sorry, 0 admit, no new axiom, no
  64`native_decide`)
  65
  66* `jcost_kernelCostContent`: `J` satisfies the kernel's five cost premises.
  67* `reciprocalInvolution_preserves_cost`, `reciprocalInvolution_never_reaches`,
  68  `kernel_cost_content_does_not_entail_cost_spending`: the reach wall.
  69* `no_kernel_derivation_of_residue`: the wall in its exact logical form, that
  70  the implication from the kernel's cost premises to the residue is false.
  71* `costSpendingSubstrate_nonempty`, `CostSpendingSubstrate.reaches_carrier`,
  72  `residue_has_two_models`, `no_unique_dynamics_from_residue`: the postulate,
  73  consistent, sufficient, and not determining.
  74
  75## Scope, stated exactly
  76
  77The wall says the kernel's **cost** premises fix no motion on the strain
  78space. It does not say the kernel is silent about motion everywhere: the
  79tick update is a kernel object, and it is already known to be
  80reversal-conjugate and 8-periodic on its core, hence unable to descend
  81(`RecognitionUpdateDescentWall`). The two results agree and are
  82complementary: the kernel's cost layer says nothing about motion, and the
  83kernel's one motion layer provably cannot supply descent. A derivation of
  84the residue would need a recognition premise about how ledger ratios change
  85between postings, and no such premise is in the kernel's cost content.
  86-/
  87
  88namespace IndisputableMonolith
  89namespace Gravity
  90namespace SevenGaps
  91namespace StrainDescent
  92
  93open Real Set Filter
  94open scoped Topology
  95
  96noncomputable section
  97
  98/-! ## §1. The kernel's cost content -/
  99
 100/-- The recognition kernel's content about cost: exactly the premise package
 101that `law_of_logic_forces_jcost` consumes to force the cost to be `J`. Every
 102field is a property of the cost of a single ratio. -/
 103structure KernelCostContent (F : ℝ → ℝ) : Prop where
 104  reciprocal : Cost.FunctionalEquation.IsReciprocalCost F
 105  normalized : Cost.FunctionalEquation.IsNormalized F
 106  composition : Cost.FunctionalEquation.SatisfiesCompositionLaw F
 107  calibrated : Cost.FunctionalEquation.IsCalibrated F
 108  continuous : ContinuousOn F (Set.Ioi 0)
 109
 110/-- **THEOREM.** The recognition cost satisfies the kernel's cost content. -/
 111theorem jcost_kernelCostContent : KernelCostContent Cost.Jcost where
 112  reciprocal := by
 113    intro x hx
 114    have hx0 : x ≠ 0 := ne_of_gt hx
 115    unfold Cost.Jcost
 116    field_simp
 117    ring
 118  normalized := by
 119    unfold Cost.FunctionalEquation.IsNormalized Cost.Jcost
 120    norm_num
 121  composition := Cost.SymplecticAction.jcost_satisfiesCompositionLaw_via_symplectic
 122  calibrated := by
 123    have hG : Cost.FunctionalEquation.G Cost.Jcost = fun t => Real.cosh t - 1 :=
 124      funext Cost.FunctionalEquation.Jcost_G_eq_cosh_sub_one
 125    have h1 : deriv (fun t : ℝ => Real.cosh t - 1) = Real.sinh := by
 126      funext t
 127      exact ((Real.hasDerivAt_cosh t).sub_const 1).deriv
 128    have h2 : deriv Real.sinh = Real.cosh := by
 129      funext t
 130      exact (Real.hasDerivAt_sinh t).deriv
 131    unfold Cost.FunctionalEquation.IsCalibrated
 132    rw [hG, h1, h2, Real.cosh_zero]
 133  continuous := by
 134    apply ContinuousOn.sub _ continuousOn_const
 135    apply ContinuousOn.div _ continuousOn_const (by norm_num)
 136    apply ContinuousOn.add continuousOn_id
 137    apply ContinuousOn.inv₀ continuousOn_id
 138    intro x hx
 139    exact ne_of_gt hx
 140
 141/-! ## §2. The reach wall: the ledger's own involution refutes the residue -/
 142
 143/-- The ledger's reciprocal involution `x ↦ 1/x`, in the strain coordinate
 144`t = log x`. Its invariance is the reciprocity premise of the kernel's cost
 145content. -/
 146def reciprocalInvolution : ℝ → ℝ := fun t => -t
 147
 148theorem reciprocalInvolution_continuous : Continuous reciprocalInvolution :=
 149  continuous_neg
 150
 151/-- **THEOREM.** The reciprocal involution preserves bare recognition cost
 152exactly. It spends nothing, anywhere. -/
 153theorem reciprocalInvolution_preserves_cost (t : ℝ) :
 154    sourceCost1 0 (reciprocalInvolution t) = sourceCost1 0 t := by
 155  unfold sourceCost1 reciprocalInvolution
 156  rw [Real.cosh_neg]
 157  ring
 158
 159theorem reciprocalInvolution_iterate_even (t₀ : ℝ) (k : ℕ) :
 160    reciprocalInvolution^[2 * k] t₀ = t₀ := by
 161  induction k with
 162  | zero => simp
 163  | succ m ih =>
 164    have h : 2 * (m + 1) = 2 * m + 2 := by ring
 165    rw [h, Function.iterate_add_apply]
 166    have h2 : reciprocalInvolution^[2] t₀ = t₀ := by
 167      simp [reciprocalInvolution, Function.iterate_succ_apply]
 168    rw [h2, ih]
 169
 170/-- **THEOREM.** From any nonzero strain the involution's orbit never reaches
 171the carrier: it oscillates forever. -/
 172theorem reciprocalInvolution_never_reaches (t₀ : ℝ) (h : t₀ ≠ 0) :
 173    ¬ Tendsto (fun k => reciprocalInvolution^[k] t₀) atTop (𝓝 (Real.arsinh 0)) := by
 174  intro hcon
 175  rw [Real.arsinh_zero] at hcon
 176  have hidx : Tendsto (fun k : ℕ => 2 * k) atTop atTop :=
 177    tendsto_atTop_mono (fun k => by omega : ∀ k : ℕ, k ≤ 2 * k) tendsto_id
 178  have hsub := hcon.comp hidx
 179  rw [Function.comp_def] at hsub
 180  simp only [reciprocalInvolution_iterate_even t₀] at hsub
 181  have := tendsto_nhds_unique hsub (tendsto_const_nhds (x := t₀) (f := atTop))
 182  exact h this.symm
 183
 184/-- **THEOREM (the reach wall).** The kernel's cost content holds, while a
 185continuous map on the strain space fails the residue: the ledger's own
 186reciprocal involution, whose invariance is the reciprocity premise itself,
 187preserves recognition cost everywhere and never reaches the carrier. So the
 188residue is not entailed by what the kernel says about cost. -/
 189theorem kernel_cost_content_does_not_entail_cost_spending :
 190    KernelCostContent Cost.Jcost ∧
 191    ∃ S : ℝ → ℝ, Continuous S ∧
 192      (∀ t, sourceCost1 0 (S t) = sourceCost1 0 t) ∧
 193      ¬ (∀ t, t ≠ Real.arsinh 0 → sourceCost1 0 (S t) < sourceCost1 0 t) := by
 194  refine ⟨jcost_kernelCostContent, reciprocalInvolution,
 195    reciprocalInvolution_continuous, reciprocalInvolution_preserves_cost, ?_⟩
 196  intro hcon
 197  have h1 : (1:ℝ) ≠ Real.arsinh 0 := by
 198    rw [Real.arsinh_zero]
 199    norm_num
 200  have := hcon 1 h1
 201  rw [reciprocalInvolution_preserves_cost 1] at this
 202  exact lt_irrefl _ this
 203
 204/-- **THEOREM (the wall in its exact logical form).** There is no derivation
 205of the residue from the kernel's cost content: the implication "the kernel's
 206cost premises hold, therefore every continuous map on the strain space spends
 207cost off the least-cost state" is false. This is the precise statement the
 208reach question asked for, and the reciprocal involution refutes it. -/
 209theorem no_kernel_derivation_of_residue :
 210    ¬ (KernelCostContent Cost.Jcost →
 211        ∀ S : ℝ → ℝ, Continuous S →
 212          ∀ t, t ≠ Real.arsinh 0 → sourceCost1 0 (S t) < sourceCost1 0 t) := by
 213  intro hderiv
 214  have h1 : (1:ℝ) ≠ Real.arsinh 0 := by
 215    rw [Real.arsinh_zero]
 216    norm_num
 217  have h := hderiv jcost_kernelCostContent reciprocalInvolution
 218    reciprocalInvolution_continuous 1 h1
 219  rw [reciprocalInvolution_preserves_cost 1] at h
 220  exact lt_irrefl _ h
 221
 222/-! ## §3. The named postulate -/
 223
 224/-- **The C2 bridge's remaining adoption, named.** A cost-spending substrate
 225is a continuous map on a hinge channel's strain space that strictly lowers
 226the sourced recognition cost at every state other than the least-cost state.
 227
 228This is the whole of what the bridge assumes about motion. It names no
 229metric, no step law, no rate, and no gradient. -/
 230structure CostSpendingSubstrate (a : ℝ) where
 231  step : ℝ → ℝ
 232  step_continuous : Continuous step
 233  spends_cost : ∀ t, t ≠ Real.arsinh a → sourceCost1 a (step t) < sourceCost1 a t
 234
 235/-- **THEOREM (sufficiency).** Every cost-spending substrate reaches the
 236sourced least-cost carrier, from every initial strain. -/
 237theorem CostSpendingSubstrate.reaches_carrier {a : ℝ} (P : CostSpendingSubstrate a)
 238    (s₀ : ℝ) :
 239    Tendsto (fun k => P.step^[k] s₀) atTop (𝓝 (Real.arsinh a)) :=
 240  cost_decreasing_dynamics_converges' a P.step P.step_continuous P.spends_cost s₀
 241
 242/-- **THEOREM (consistency).** The postulate is inhabited: the banked gradient
 243step is a cost-spending substrate. So adopting it is not adopting a
 244contradiction. -/
 245theorem costSpendingSubstrate_nonempty (a : ℝ) : Nonempty (CostSpendingSubstrate a) := by
 246  refine ⟨⟨strainStep1 a, strainStep1_continuous a, ?_⟩⟩
 247  intro t ht
 248  apply descent_one_dim_lt a t
 249  intro hres
 250  apply ht
 251  exact (step_fixed_iff_arsinh a t).mp (by
 252    unfold strainStep1
 253    rw [hres]
 254    ring)
 255
 256/-- The map that collapses every strain straight to the least-cost state. -/
 257def collapseStep (a : ℝ) : ℝ → ℝ := fun _ => Real.arsinh a
 258
 259/-- The map that halves the distance to the least-cost state. -/
 260def halfwayStep (a : ℝ) : ℝ → ℝ := fun t => (t + Real.arsinh a) / 2
 261
 262def collapse_substrate (a : ℝ) : CostSpendingSubstrate a where
 263  step := collapseStep a
 264  step_continuous := continuous_const
 265  spends_cost := by
 266    intro t ht
 267    exact sourceCost1_lt_of_ne a t ht
 268
 269def halfway_substrate (a : ℝ) : CostSpendingSubstrate a where
 270  step := halfwayStep a
 271  step_continuous := by
 272    unfold halfwayStep
 273    fun_prop
 274  spends_cost := by
 275    intro t ht
 276    unfold halfwayStep
 277    rcases lt_or_gt_of_ne ht with hlt | hgt
 278    · -- t < arsinh a: the midpoint lies strictly between t and the minimum
 279      have hmid1 : t < (t + Real.arsinh a) / 2 := by linarith
 280      have hmid2 : (t + Real.arsinh a) / 2 ≤ Real.arsinh a := by linarith
 281      exact sourceCost1_strictAntiOn a (mem_Iic.mpr hlt.le) (mem_Iic.mpr hmid2) hmid1
 282    · have hmid1 : (t + Real.arsinh a) / 2 < t := by linarith
 283      have hmid2 : Real.arsinh a ≤ (t + Real.arsinh a) / 2 := by linarith
 284      exact sourceCost1_strictMonoOn a (mem_Ici.mpr hmid2) (mem_Ici.mpr hgt.le) hmid1
 285
 286/-- **THEOREM (the postulate does not name a dynamics).** The residue has at
 287least two distinct models. -/
 288theorem residue_has_two_models (a : ℝ) :
 289    ∃ P Q : CostSpendingSubstrate a, P.step ≠ Q.step := by
 290  refine ⟨collapse_substrate a, halfway_substrate a, ?_⟩
 291  intro hcon
 292  have h := congrFun hcon (Real.arsinh a + 2)
 293  simp only [collapse_substrate, halfway_substrate, collapseStep, halfwayStep] at h
 294  linarith
 295
 296/-- **THEOREM.** No single flow is determined by the residue, so every
 297principle that names one (steepest descent in a fixed metric included) is
 298strictly stronger than what the C2 bridge needs. -/
 299theorem no_unique_dynamics_from_residue (a : ℝ) :
 300    ¬ ∃ S₀ : ℝ → ℝ, ∀ P : CostSpendingSubstrate a, P.step = S₀ := by
 301  rintro ⟨S₀, hS₀⟩
 302  obtain ⟨P, Q, hne⟩ := residue_has_two_models a
 303  exact hne ((hS₀ P).trans (hS₀ Q).symm)
 304
 305end
 306
 307end StrainDescent
 308end SevenGaps
 309end Gravity
 310end IndisputableMonolith
 311