IndisputableMonolith.Foundation.DAlembert.CurvatureGate

   1import Mathlib
   2import IndisputableMonolith.Cost
   3import IndisputableMonolith.Foundation.DAlembert.Counterexamples
   4
   5/-!
   6# Curvature Gate: The Geometric Path
   7
   8This module formalizes the **Curvature Gate**: the requirement that the cost metric
   9has constant nonzero curvature.
  10
  11## Key Insight
  12
  13The log-coordinate representation G(t) = F(eᵗ) defines a 1D metric via ds² = G''(t) dt².
  14The curvature of this metric distinguishes:
  15- Flat (κ = 0): G(t) = t²/2 (the counterexample)
  16- Hyperbolic (κ = -1): G(t) = cosh(t) - 1 (the RCL)
  17- Spherical (κ = +1): G(t) = 1 - cos(t) (ruled out by F ≥ 0)
  18
  19## Physical Interpretation
  20
  21- Flat space: Comparisons are independent. No holistic structure.
  22- Hyperbolic space: Comparisons are entangled. Exponential divergence of nearby states.
  23- Spherical space: Comparisons are periodic. Violates non-negativity.
  24
  25The curvature gate says: "Recognition geometry is non-trivially curved."
  26-/
  27
  28namespace IndisputableMonolith
  29namespace Foundation
  30namespace DAlembert
  31namespace CurvatureGate
  32
  33open Real Cost
  34
  35/-! ## The Log-Lift Functions -/
  36
  37/-- The log-coordinate representation of a cost function. -/
  38noncomputable def G_of_F (F : ℝ → ℝ) (t : ℝ) : ℝ := F (Real.exp t)
  39
  40/-- The shifted log-lift (for d'Alembert form). -/
  41noncomputable def H_of_F (F : ℝ → ℝ) (t : ℝ) : ℝ := G_of_F F t + 1
  42
  43/-! ## Specific G Functions -/
  44
  45/-- The quadratic G from the counterexample. -/
  46noncomputable def Gquad (t : ℝ) : ℝ := t ^ 2 / 2
  47
  48/-- The hyperbolic G from the RCL. -/
  49noncomputable def Gcosh (t : ℝ) : ℝ := Real.cosh t - 1
  50
  51/-- The spherical G (eventually negative). -/
  52noncomputable def Gspher (t : ℝ) : ℝ := Real.cos t - 1
  53
  54/-! ## The ODE Characterization -/
  55
  56/-- The ODE G'' = G + 1 characterizes hyperbolic solutions. -/
  57def SatisfiesHyperbolicODE (G : ℝ → ℝ) : Prop :=
  58  ∀ t : ℝ, deriv (deriv G) t = G t + 1
  59
  60/-- The ODE G'' = 1 characterizes the quadratic/flat solution. -/
  61def SatisfiesFlatODE (G : ℝ → ℝ) : Prop :=
  62  ∀ t : ℝ, deriv (deriv G) t = 1
  63
  64/-- The ODE G'' = -(G + 1) characterizes spherical solutions. -/
  65def SatisfiesSphericalODE (G : ℝ → ℝ) : Prop :=
  66  ∀ t : ℝ, deriv (deriv G) t = -(G t + 1)
  67
  68/-! ## Verification of ODE Satisfaction -/
  69
  70/-- Gquad satisfies the flat ODE: G''(t) = 1. -/
  71theorem Gquad_satisfies_flat : SatisfiesFlatODE Gquad := by
  72  intro t
  73  -- G(t) = t²/2, G'(t) = t, G''(t) = 1
  74  have h1 : deriv Gquad = fun t => t := by
  75    ext s
  76    unfold Gquad
  77    have hd : HasDerivAt (fun t => t ^ 2 / 2) s s := by
  78      have := hasDerivAt_pow 2 s
  79      simp only [Nat.cast_ofNat, pow_one] at this
  80      have h := this.div_const 2
  81      convert h using 1
  82      ring
  83    exact hd.deriv
  84  have h2 : deriv (deriv Gquad) t = 1 := by
  85    rw [h1]
  86    simp only [deriv_id'']
  87  exact h2
  88
  89/-- Gcosh satisfies the hyperbolic ODE: G''(t) = G(t) + 1 = cosh(t). -/
  90theorem Gcosh_satisfies_hyperbolic : SatisfiesHyperbolicODE Gcosh := by
  91  intro t
  92  -- G(t) = cosh(t) - 1, G'(t) = sinh(t), G''(t) = cosh(t)
  93  have h1 : deriv Gcosh = Real.sinh := by
  94    ext s
  95    unfold Gcosh
  96    rw [deriv_sub_const, Real.deriv_cosh]
  97  have h2 : deriv (deriv Gcosh) t = Real.cosh t := by
  98    rw [h1, Real.deriv_sinh]
  99  rw [h2]
 100  unfold Gcosh
 101  ring
 102
 103/-- Gspher satisfies the spherical ODE: G''(t) = -(G(t) + 1) = -cos(t). -/
 104theorem Gspher_satisfies_spherical : SatisfiesSphericalODE Gspher := by
 105  intro t
 106  -- G(t) = cos(t) - 1, G'(t) = -sin(t), G''(t) = -cos(t)
 107  have h1 : deriv Gspher = fun t => -Real.sin t := by
 108    ext s
 109    unfold Gspher
 110    rw [deriv_sub_const, Real.deriv_cos]
 111  have h2 : deriv (deriv Gspher) t = -Real.cos t := by
 112    rw [h1]
 113    have hd : HasDerivAt (fun t => -Real.sin t) (-Real.cos t) t := by
 114      have := Real.hasDerivAt_sin t
 115      exact this.neg
 116    exact hd.deriv
 117  rw [h2]
 118  unfold Gspher
 119  ring
 120
 121/-! ## Key Distinctness Results -/
 122
 123/-- Gquad is NOT hyperbolic. -/
 124theorem Gquad_not_hyperbolic : ¬ SatisfiesHyperbolicODE Gquad := by
 125  intro h
 126  have h0 := h 0
 127  -- LHS: deriv (deriv Gquad) 0 = 1 (from flat ODE)
 128  have hflat := Gquad_satisfies_flat 0
 129  -- RHS: Gquad 0 + 1 = 0 + 1 = 1
 130  simp only [Gquad] at h0
 131  -- Actually both sides are 1 at t=0. Try t=1.
 132  have h1 := h 1
 133  have hflat1 := Gquad_satisfies_flat 1
 134  simp only [Gquad] at h1
 135  -- LHS = 1, RHS = 1/2 + 1 = 3/2
 136  rw [hflat1] at h1
 137  norm_num at h1
 138
 139/-- Gcosh is NOT flat. -/
 140theorem Gcosh_not_flat : ¬ SatisfiesFlatODE Gcosh := by
 141  intro h
 142  have h1 := h 1
 143  -- deriv (deriv Gcosh) 1 = cosh(1) ≈ 1.54
 144  have hhyp := Gcosh_satisfies_hyperbolic 1
 145  simp only [Gcosh] at hhyp
 146  rw [h1] at hhyp
 147  -- 1 = cosh(1) - 1 + 1 = cosh(1)
 148  -- But cosh(1) > 1
 149  have hcosh1 : Real.cosh 1 > 1 := Real.one_lt_cosh.mpr (by norm_num : (1 : ℝ) ≠ 0)
 150  linarith
 151
 152/-! ## Non-Negativity Rules Out Spherical -/
 153
 154/-- The spherical solution becomes negative (cos(t) - 1 ≤ 0, and < 0 for t ≠ 2πk). -/
 155theorem Gspher_nonpositive : ∀ t : ℝ, Gspher t ≤ 0 := by
 156  intro t
 157  simp only [Gspher]
 158  have : Real.cos t ≤ 1 := Real.cos_le_one t
 159  linarith
 160
 161/-- The spherical solution is negative at t = π. -/
 162theorem Gspher_negative_at_pi : Gspher Real.pi < 0 := by
 163  simp only [Gspher, Real.cos_pi]
 164  norm_num
 165
 166/-- A cost function in log-coordinates should be non-negative (G(t) ≥ 0). -/
 167def IsNonNegativeG (G : ℝ → ℝ) : Prop := ∀ t : ℝ, 0 ≤ G t
 168
 169/-- The spherical solution violates non-negativity. -/
 170theorem Gspher_violates_nonnegativity : ¬ IsNonNegativeG Gspher := by
 171  intro h
 172  have := h Real.pi
 173  have hneg := Gspher_negative_at_pi
 174  linarith
 175
 176/-! ## Curvature Type Classification -/
 177
 178/-- Curvature types for constant-curvature cost metrics. -/
 179inductive CurvatureType where
 180  | flat : CurvatureType      -- κ = 0, G'' = 1
 181  | hyperbolic : CurvatureType -- κ = -1, G'' = G + 1
 182  | spherical : CurvatureType  -- κ = +1, G'' = -(G + 1)
 183  deriving DecidableEq, Repr
 184
 185/-! ## The Main Classification -/
 186
 187/-- **Curvature Gate Theorem (Statement)**:
 188    Under structural axioms + constant curvature:
 189    1. Flat (κ = 0) ⟹ G = t²/2 (counterexample, no interaction)
 190    2. Hyperbolic (κ = -1) ⟹ G = cosh(t) - 1 (RCL)
 191    3. Spherical (κ = +1) ⟹ violates non-negativity
 192
 193    Therefore: Non-negativity + Interaction ⟹ Hyperbolic (RCL).
 194-/
 195theorem curvature_gate_main (G : ℝ → ℝ)
 196    (hSmooth : ContDiff ℝ 2 G)
 197    (hNorm : G 0 = 0)
 198    (hCalib : deriv (deriv G) 0 = 1)
 199    (hEven : ∀ t, G (-t) = G t)
 200    (hNonNeg : IsNonNegativeG G)
 201    (hConstCurv : SatisfiesFlatODE G ∨ SatisfiesHyperbolicODE G ∨ SatisfiesSphericalODE G) :
 202    -- Spherical is ruled out by non-negativity
 203    -- Flat corresponds to no interaction
 204    -- Hyperbolic is the RCL
 205    SatisfiesFlatODE G ∨ SatisfiesHyperbolicODE G := by
 206  rcases hConstCurv with hFlat | hHyp | hSpher
 207  · left; exact hFlat
 208  · right; exact hHyp
 209  · -- Spherical: show G = Gspher (up to scaling), which violates non-negativity
 210    -- The ODE G'' = -(G + 1) with G(0) = 0 has unique solution G = cos - 1
 211    -- But this is ≤ 0 everywhere and < 0 at π
 212    exfalso
 213    -- From the ODE and initial conditions, G must behave like cos - 1
 214    -- At t = 0: G(0) = 0, G''(0) = -(G(0) + 1) = -1
 215    -- But our calibration requires G''(0) = 1, contradiction!
 216    have hcalib_spher := hSpher 0
 217    rw [hNorm] at hcalib_spher
 218    simp at hcalib_spher
 219    -- hcalib_spher : deriv (deriv G) 0 = -1
 220    -- hCalib : deriv (deriv G) 0 = 1
 221    rw [hCalib] at hcalib_spher
 222    norm_num at hcalib_spher
 223
 224/-- The curvature gate: spherical is ruled out by calibration, leaving only flat or hyperbolic. -/
 225theorem curvature_gate_dichotomy (G : ℝ → ℝ)
 226    (hNorm : G 0 = 0)
 227    (hCalib : deriv (deriv G) 0 = 1)
 228    (hConstCurv : SatisfiesFlatODE G ∨ SatisfiesHyperbolicODE G ∨ SatisfiesSphericalODE G) :
 229    SatisfiesFlatODE G ∨ SatisfiesHyperbolicODE G := by
 230  rcases hConstCurv with hFlat | hHyp | hSpher
 231  · left; exact hFlat
 232  · right; exact hHyp
 233  · exfalso
 234    have hcalib_spher := hSpher 0
 235    rw [hNorm] at hcalib_spher
 236    simp at hcalib_spher
 237    rw [hCalib] at hcalib_spher
 238    norm_num at hcalib_spher
 239
 240/-! ## Summary Theorem -/
 241
 242/-- **Summary**: The curvature gate combined with structural axioms forces:
 243    - Spherical ruled out by calibration (G''(0) = 1 ≠ -1)
 244    - Flat corresponds to the counterexample (additive P, no interaction)
 245    - Hyperbolic corresponds to the RCL
 246
 247    The interaction gate then selects hyperbolic over flat.
 248-/
 249theorem curvature_gate_summary :
 250    -- Gquad is flat and satisfies structural axioms
 251    SatisfiesFlatODE Gquad ∧ Gquad 0 = 0 ∧ deriv (deriv Gquad) 0 = 1 ∧
 252    -- Gcosh is hyperbolic and satisfies structural axioms
 253    SatisfiesHyperbolicODE Gcosh ∧ Gcosh 0 = 0 ∧ deriv (deriv Gcosh) 0 = 1 ∧
 254    -- Gspher satisfies spherical ODE but FAILS calibration
 255    SatisfiesSphericalODE Gspher ∧ Gspher 0 = 0 ∧ deriv (deriv Gspher) 0 = -1 := by
 256  refine ⟨Gquad_satisfies_flat, ?_, ?_, Gcosh_satisfies_hyperbolic, ?_, ?_,
 257          Gspher_satisfies_spherical, ?_, ?_⟩
 258  · simp [Gquad]
 259  · have := Gquad_satisfies_flat 0; exact this
 260  · simp [Gcosh, Real.cosh_zero]
 261  · have := Gcosh_satisfies_hyperbolic 0
 262    simp [Gcosh, Real.cosh_zero] at this ⊢
 263    exact this
 264  · simp [Gspher, Real.cos_zero]
 265  · have := Gspher_satisfies_spherical 0
 266    simp [Gspher, Real.cos_zero] at this ⊢
 267    exact this
 268
 269end CurvatureGate
 270end DAlembert
 271end Foundation
 272end IndisputableMonolith
 273