IndisputableMonolith.Foundation.DAlembert.FourthGate

   1import Mathlib
   2import Mathlib.Analysis.Calculus.MeanValue
   3import IndisputableMonolith.Cost
   4import IndisputableMonolith.Cost.FunctionalEquation
   5import IndisputableMonolith.Foundation.DAlembert.CurvatureGate
   6import IndisputableMonolith.Foundation.DAlembert.Counterexamples
   7
   8/-!
   9# The Fourth Gate: d'Alembert Structure
  10
  11This module formalizes the **Fourth Gate**: the d'Alembert structure condition.
  12
  13## Relation to Gate 3 (Curvature)
  14
  15In the Option~A formulation used in the paper, Gate~3 is a \emph{normalized} closure:
  16the hyperbolic branch is assumed directly as the ODE `G''(t) = G(t) + 1`.
  17Together with symmetry (evenness) and calibration, that already forces
  18`G(t) = cosh(t) - 1`. Consequently the shifted log-lift `H = G + 1 = cosh`
  19automatically satisfies the d'Alembert functional equation.
  20
  21So, in that formulation, ``Gate 4'' is not an additional restriction beyond Gate~3;
  22it is a derived structure and a convenient cross-check.
  23
  24We keep this module explicit because it packages the classical functional-equation
  25viewpoint (Aczél's classification theorem) as a compact certificate path in Lean.
  26
  27## Historical Note
  28
  29The d'Alembert functional equation `f(x+y) + f(x-y) = 2f(x)f(y)` was studied by
  30Jean le Rond d'Alembert in the 18th century. Its continuous solutions are exactly
  31`cosh(λx)` for λ ∈ ℝ. This is a classical result in functional equation theory.
  32-/
  33
  34namespace IndisputableMonolith
  35namespace Foundation
  36namespace DAlembert
  37namespace FourthGate
  38
  39open Real Cost CurvatureGate
  40
  41/-! ## Definition of the Fourth Gate -/
  42
  43/-- **d'Alembert Structure**: A function H satisfies the d'Alembert functional equation. -/
  44def SatisfiesDAlembert (H : ℝ → ℝ) : Prop :=
  45  (H 0 = 1) ∧ (∀ t u : ℝ, H (t + u) + H (t - u) = 2 * H t * H u)
  46
  47/-- The d'Alembert structure gate for a cost function F:
  48    The shifted log-lift H(t) = F(eᵗ) + 1 satisfies d'Alembert. -/
  49def HasDAlembert (F : ℝ → ℝ) : Prop :=
  50  SatisfiesDAlembert (fun t => F (Real.exp t) + 1)
  51
  52/-! ## Canonical Solutions -/
  53
  54/-- cosh satisfies the d'Alembert equation. -/
  55theorem cosh_satisfies_dAlembert : SatisfiesDAlembert Real.cosh := by
  56  constructor
  57  · exact Real.cosh_zero
  58  · intro t u
  59    have h1 := Real.cosh_add t u
  60    have h2 := Real.cosh_sub t u
  61    linarith
  62
  63/-- Jcost has d'Alembert structure. -/
  64theorem Jcost_has_dAlembert_structure : HasDAlembert Cost.Jcost := by
  65  unfold HasDAlembert SatisfiesDAlembert
  66  constructor
  67  · simp [Cost.Jcost, Real.exp_zero]
  68  · intro t u
  69    have hH : ∀ s, Cost.Jcost (Real.exp s) + 1 = Real.cosh s := by
  70      intro s
  71      simp only [Cost.Jcost]
  72      have hcosh : Real.cosh s = (Real.exp s + Real.exp (-s)) / 2 := Real.cosh_eq s
  73      have hneg : Real.exp (-s) = (Real.exp s)⁻¹ := Real.exp_neg s
  74      linarith
  75    simp only [hH]
  76    have hcosh := cosh_satisfies_dAlembert.2 t u
  77    exact hcosh
  78
  79/-! ## d'Alembert Classification Theorem -/
  80
  81/-- Differentiating the d'Alembert functional equation twice:
  82if `f(x+y) + f(x-y) = 2 f(x) f(y)`, then `f''(x) = f''(0) * f(x)`. -/
  83theorem dalembert_deriv_ode (f : ℝ → ℝ) (hf : ContDiff ℝ 2 f)
  84    (hDA : ∀ x y, f (x + y) + f (x - y) = 2 * f x * f y) :
  85    ∀ x, deriv (deriv f) x = deriv (deriv f) 0 * f x := by
  86  -- Proof: fix t. The functions u ↦ f(t+u)+f(t-u) and u ↦ 2·f(t)·f(u) agree pointwise
  87  -- (by hDA), so their second derivatives at u=0 agree.
  88  -- LHS: d²/du²[f(t+u)+f(t-u)]|_{u=0} = 2·f''(t)
  89  -- RHS: d²/du²[2·f(t)·f(u)]|_{u=0}   = 2·f(t)·f''(0)
  90  -- Therefore f''(t) = f''(0)·f(t).
  91  have hDiff : Differentiable ℝ f :=
  92    hf.differentiable (by decide : (2 : WithTop ℕ∞) ≠ 0)
  93  have hCDiff1_f' : ContDiff ℝ 1 (deriv f) := by
  94    rw [show (2 : WithTop ℕ∞) = 1 + 1 from rfl] at hf
  95    rw [contDiff_succ_iff_deriv] at hf
  96    exact hf.2.2
  97  have hDiffDeriv : Differentiable ℝ (deriv f) :=
  98    hCDiff1_f'.differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0)
  99  -- Shift helpers: HasDerivAt for affine shifts of u
 100  have hsh_add : ∀ (s v : ℝ), HasDerivAt (fun u => s + u) (1 : ℝ) v := fun s v => by
 101    have h := (hasDerivAt_id v).add_const s; simp only [id] at h
 102    rwa [show (fun u : ℝ => u + s) = fun u => s + u from funext fun u => add_comm u s] at h
 103  have hsh_sub : ∀ (s v : ℝ), HasDerivAt (fun u => s - u) (-1 : ℝ) v := fun s v => by
 104    have h1 : HasDerivAt (fun u : ℝ => -u) (-1 : ℝ) v := by
 105      have := (hasDerivAt_id v).neg; simp only [id] at this; exact this
 106    have h2 := h1.const_add s
 107    rwa [show (fun u : ℝ => s + -u) = fun u => s - u from funext fun u => by ring] at h2
 108  intro t
 109  -- Pointwise equality of the two sides of hDA, lifted to functions of u
 110  have h_feq : (fun u => f (t + u) + f (t - u)) = (fun u => 2 * f t * f u) :=
 111    funext (hDA t)
 112  have key : deriv (deriv (fun u => f (t + u) + f (t - u))) 0 =
 113             deriv (deriv (fun u => 2 * f t * f u)) 0 :=
 114    congr_arg (fun fn => deriv (deriv fn) 0) h_feq
 115  -- Compute LHS = 2 * f''(t)
 116  have lhs_eq : deriv (deriv (fun u => f (t + u) + f (t - u))) 0 = 2 * deriv (deriv f) t := by
 117    have h_plus : ∀ v, HasDerivAt (fun u => f (t + u)) (deriv f (t + v)) v := fun v => by
 118      have hcomp := (hDiff (t + v)).hasDerivAt.comp v (hsh_add t v)
 119      simp only [mul_one, Function.comp_apply] at hcomp; exact hcomp
 120    have h_minus : ∀ v, HasDerivAt (fun u => f (t - u)) (-deriv f (t - v)) v := fun v => by
 121      have hcomp := (hDiff (t - v)).hasDerivAt.comp v (hsh_sub t v)
 122      simp only [mul_neg, mul_one, Function.comp_apply] at hcomp; exact hcomp
 123    have hfirst_fun : deriv (fun u => f (t + u) + f (t - u)) =
 124        fun v => deriv f (t + v) - deriv f (t - v) := funext fun v => by
 125      have heq : (fun u => f (t + u)) + (fun u => f (t - u)) =
 126          fun u => f (t + u) + f (t - u) := by ext u; rfl
 127      have h12 : deriv (fun u => f (t + u) + f (t - u)) v =
 128          deriv f (t + v) + -deriv f (t - v) := by
 129        rw [← heq]; exact ((h_plus v).add (h_minus v)).deriv
 130      linarith [show deriv f (t + v) + -deriv f (t - v) =
 131          deriv f (t + v) - deriv f (t - v) from by ring]
 132    have hd2_plus : HasDerivAt (fun v => deriv f (t + v)) (deriv (deriv f) t) 0 := by
 133      have hDH : HasDerivAt (deriv f) (deriv (deriv f) (t + 0)) (t + 0) :=
 134        (hDiffDeriv (t + 0)).hasDerivAt
 135      have hcomp := hDH.comp 0 (hsh_add t 0)
 136      simp only [mul_one, add_zero, Function.comp_apply] at hcomp; exact hcomp
 137    have hd2_minus : HasDerivAt (fun v => deriv f (t - v)) (-deriv (deriv f) t) 0 := by
 138      have hDH : HasDerivAt (deriv f) (deriv (deriv f) (t - 0)) (t - 0) :=
 139        (hDiffDeriv (t - 0)).hasDerivAt
 140      have hcomp := hDH.comp 0 (hsh_sub t 0)
 141      simp only [mul_neg, mul_one, sub_zero, Function.comp_apply] at hcomp; exact hcomp
 142    rw [congr_fun (congr_arg deriv hfirst_fun) 0]
 143    have heq2 : (fun v => deriv f (t + v)) - (fun v => deriv f (t - v)) =
 144        fun v => deriv f (t + v) - deriv f (t - v) := by ext v; rfl
 145    have h : deriv (fun v => deriv f (t + v) - deriv f (t - v)) 0 =
 146        deriv (deriv f) t - -deriv (deriv f) t := by
 147      rw [← heq2]; exact (hd2_plus.sub hd2_minus).deriv
 148    linarith [show deriv (deriv f) t - -deriv (deriv f) t = 2 * deriv (deriv f) t from by ring]
 149  -- Compute RHS = 2 * f(t) * f''(0)
 150  have rhs_eq : deriv (deriv (fun u => 2 * f t * f u)) 0 = 2 * f t * deriv (deriv f) 0 := by
 151    have hfirst_fun : deriv (fun u => 2 * f t * f u) = fun v => 2 * f t * deriv f v :=
 152      funext fun v => ((hDiff v).hasDerivAt.const_mul (2 * f t)).deriv
 153    have hsecond := (hDiffDeriv 0).hasDerivAt.const_mul (2 * f t)
 154    rw [congr_fun (congr_arg deriv hfirst_fun) 0, hsecond.deriv]
 155  -- Conclude: f''(t) = f''(0) * f(t)
 156  rw [lhs_eq, rhs_eq] at key
 157  -- key : 2 * deriv (deriv f) t = 2 * f t * deriv (deriv f) 0
 158  calc deriv (deriv f) t
 159      = (2 * deriv (deriv f) t) / 2 := by ring
 160    _ = (2 * f t * deriv (deriv f) 0) / 2 := by rw [key]
 161    _ = deriv (deriv f) 0 * f t := by ring
 162
 163/-- **Theorem (d'Alembert Classification)**: If H is C², satisfies d'Alembert,
 164    H(0) = 1, H'(0) = 0, and H''(0) = λ², then H(t) = cosh(λt).
 165
 166    **Note**: This general λ version is not used in the main forcing chain.
 167    The framework only requires the λ = 1 case, which is proved in
 168    `dAlembert_with_unit_calibration`. The general case reduces to it by scaling:
 169    For λ ≠ 0, define K(s) = H(s/λ); then K'' = K, K(0)=1, K'(0)=0, so K = cosh,
 170    hence H(t) = cosh(λt). For λ = 0, H'' = 0 gives H = 1 = cosh(0).
 171    Formalizing the scaling argument requires careful chain-rule handling. -/
 172theorem dAlembert_classification :
 173    ∀ H : ℝ → ℝ, ∀ lam : ℝ,
 174    SatisfiesDAlembert H →
 175    ContDiff ℝ 2 H →
 176    deriv H 0 = 0 →
 177    deriv (deriv H) 0 = lam ^ 2 →
 178    ∀ t, H t = Real.cosh (lam * t) := by
 179  intro H lam hDA hSmooth hDeriv0 hCalib t
 180  have h_ode : ∀ x, deriv (deriv H) x = deriv (deriv H) 0 * H x :=
 181    dalembert_deriv_ode H hSmooth hDA.2
 182  by_cases hlam : lam = 0
 183  · -- λ = 0: H'' = 0, so H is constant; H(0)=1, H'(0)=0 ⇒ H = 1 = cosh(0)
 184    subst hlam
 185    have hode0 : ∀ x, deriv (deriv H) x = 0 := fun x => by
 186      rw [h_ode x, hCalib, zero_pow two_ne_zero]; exact zero_mul (H x)
 187    -- H''=0 ⇒ deriv H constant; deriv H 0 = 0 ⇒ deriv H = 0 ⇒ H constant; H 0 = 1 ⇒ H = 1
 188    have hd_deriv : Differentiable ℝ (deriv H) := hSmooth.differentiable_deriv_two
 189    have hH'0 : ∀ x, deriv H x = 0 := fun x => (is_const_of_deriv_eq_zero hd_deriv hode0 x 0).trans hDeriv0
 190    have hH_const : ∀ x, H x = 1 := fun x => (is_const_of_deriv_eq_zero (hSmooth.differentiable (by decide)) hH'0 x 0).trans hDA.1
 191    simp only [hH_const t, zero_mul, Real.cosh_zero]
 192  · -- λ ≠ 0: K(s) = H(s/λ) satisfies K'' = K, K(0)=1, K'(0)=0, K''(0)=1; apply unit calibration.
 193    let K := fun s => H (s / lam)
 194    have hK0 : K 0 = 1 := by simp [K, hDA.1]
 195    have hK_DA : SatisfiesDAlembert K := by
 196      constructor; exact hK0
 197      intro t u
 198      simp only [K]
 199      have ht : (t + u) / lam = t / lam + u / lam := by field_simp [hlam]
 200      have ht' : (t - u) / lam = t / lam - u / lam := by field_simp [hlam]
 201      rw [ht, ht']
 202      exact hDA.2 (t / lam) (u / lam)
 203    have hK_smooth : ContDiff ℝ 2 K :=
 204      ContDiff.comp hSmooth ((contDiff_id.div_const lam).of_le le_top)
 205    have hK'_0 : deriv K 0 = 0 := by
 206      have K_eq : K = fun s => H ((1/lam) * s) := by ext s; simp [K]; congr 1; field_simp [hlam]
 207      rw [K_eq, deriv_comp_mul_left (1/lam) H 0]
 208      rw [show (1/lam) * 0 = 0 from by ring, hDeriv0]; simp
 209    have hK''_0 : deriv (deriv K) 0 = 1 := by
 210      have K_eq : K = fun s => H ((1/lam) * s) := by ext s; simp [K]; congr 1; field_simp [hlam]
 211      have dK : deriv K = fun s => (1/lam) * deriv H (s/lam) := by
 212        ext s
 213        rw [K_eq, deriv_comp_mul_left (1/lam) H s, smul_eq_mul]
 214        rw [show (1/lam) * s = s / lam from by field_simp [hlam]]
 215      rw [dK, deriv_const_mul_field (1/lam)]
 216      rw [show (fun s => deriv H (s/lam)) = fun s => (deriv H) ((1/lam) * s) from by ext s; congr 1; field_simp [hlam]]
 217      rw [deriv_comp_mul_left (1/lam) (deriv H) 0, smul_eq_mul]
 218      rw [show (1/lam) * 0 = 0 from by ring, h_ode 0, hCalib, hDA.1]
 219      field_simp [hlam]
 220    have hK_ode : ∀ s, deriv (deriv K) s = K s := by
 221      intro s
 222      have K_eq : K = fun z => H ((1/lam) * z) := by ext z; simp [K]; congr 1; field_simp [hlam]
 223      have dK : deriv K = fun x => (1/lam) * deriv H (x/lam) := by
 224        ext x
 225        rw [K_eq, deriv_comp_mul_left (1/lam) H x, smul_eq_mul]
 226        rw [show (1/lam) * x = x / lam from by field_simp [hlam]]
 227      rw [dK, deriv_const_mul_field (1/lam)]
 228      rw [show (fun x => deriv H (x/lam)) = fun x => (deriv H) ((1/lam) * x) from by ext x; congr 1; field_simp [hlam]]
 229      rw [deriv_comp_mul_left (1/lam) (deriv H) s, smul_eq_mul]
 230      rw [show (1/lam) * s = s / lam from by field_simp [hlam], h_ode (s/lam)]
 231      simp only [K, hCalib]; field_simp [hlam]
 232    have hK_eq_cosh : ∀ s, K s = Real.cosh s :=
 233      Cost.FunctionalEquation.ode_cosh_uniqueness_contdiff K hK_smooth hK_ode hK0 hK'_0
 234    have h_eq : K (lam * t) = H t := by simp [K]; field_simp [hlam]
 235    rw [← h_eq, hK_eq_cosh (lam * t)]
 236
 237/-- **Corollary**: With calibration H''(0) = 1, we get H = cosh.
 238    Proof: dalembert_deriv_ode gives H''(t) = H''(0)·H(t); substituting H''(0) = 1
 239    gives H'' = H; ODE uniqueness (H(0)=1, H'(0)=0) then forces H = cosh. -/
 240theorem dAlembert_with_unit_calibration (H : ℝ → ℝ)
 241    (hDA : SatisfiesDAlembert H)
 242    (hSmooth : ContDiff ℝ 2 H)
 243    (hDeriv0 : deriv H 0 = 0)
 244    (hCalib : deriv (deriv H) 0 = 1) :
 245    ∀ t, H t = Real.cosh t := by
 246  -- Step 1: H''(t) = H''(0) · H(t) from d'Alembert + C²
 247  have hode_gen : ∀ x, deriv (deriv H) x = deriv (deriv H) 0 * H x :=
 248    dalembert_deriv_ode H hSmooth hDA.2
 249  -- Step 2: Substitute H''(0) = 1 to get the canonical ODE H'' = H
 250  have hode : ∀ t, deriv (deriv H) t = H t := fun t => by
 251    rw [hode_gen t, hCalib, one_mul]
 252  -- Step 3: H(0) = 1 (from SatisfiesDAlembert)
 253  have hH0 : H 0 = 1 := hDA.1
 254  -- Step 4: ODE uniqueness — the unique C² solution to H'' = H, H(0) = 1, H'(0) = 0 is cosh
 255  exact Cost.FunctionalEquation.ode_cosh_uniqueness_contdiff H hSmooth hode hH0 hDeriv0
 256
 257/-! ## d'Alembert Forces Canonical G -/
 258
 259/-- d'Alembert structure + calibration forces G = cosh - 1. -/
 260theorem dAlembert_forces_Gcosh (G : ℝ → ℝ)
 261    (hDA : SatisfiesDAlembert (fun t => G t + 1))
 262    (hSmooth : ContDiff ℝ 2 G)
 263    (_ : G 0 = 0)
 264    (hEven : ∀ t, G (-t) = G t)
 265    (hCalib : deriv (deriv G) 0 = 1) :
 266    ∀ t, G t = Real.cosh t - 1 := by
 267  let H := fun t => G t + 1
 268  have hHsmooth : ContDiff ℝ 2 H := hSmooth.add contDiff_const
 269  have hHderiv0 : deriv H 0 = 0 := by
 270    have hderivH : deriv H = deriv G := by ext t; simp [H, deriv_add_const]
 271    rw [hderivH]
 272    have hGeven : (fun t => G (-t)) = G := funext hEven
 273    have hcomp : deriv (fun t => G (-t)) 0 = deriv G 0 := by simp only [hGeven]
 274    have hchain : deriv (fun t => G (-t)) 0 = -(deriv G 0) := by
 275      have heq : (fun t => G (-t)) = G ∘ (fun t => -t) := rfl
 276      rw [heq]
 277      have hGdiff : DifferentiableAt ℝ G 0 := hSmooth.differentiable (by norm_num) |>.differentiableAt
 278      rw [deriv_comp (0 : ℝ) (by simp only [neg_zero]; exact hGdiff) differentiable_neg.differentiableAt]
 279      simp only [neg_zero, deriv_neg', mul_neg_one]
 280    rw [hchain] at hcomp
 281    linarith
 282  have hHcalib : deriv (deriv H) 0 = 1 := by
 283    have h1 : deriv H = deriv G := by ext t; simp [H, deriv_add_const]
 284    have h2 : deriv (deriv H) = deriv (deriv G) := by simp [h1]
 285    rw [h2, hCalib]
 286  have hHcosh := dAlembert_with_unit_calibration H hDA hHsmooth hHderiv0 hHcalib
 287  intro t
 288  have := hHcosh t
 289  simp only [H] at this
 290  linarith
 291
 292/-! ## The Counterexample Fails Gate 4 -/
 293
 294/-- The quadratic log-lift H(t) = t²/2 + 1 does NOT satisfy d'Alembert. -/
 295theorem Hquad_not_dAlembert : ¬ SatisfiesDAlembert (fun t => t^2/2 + 1) := by
 296  intro ⟨_, hda⟩
 297  have h11 := hda 1 1
 298  norm_num at h11
 299
 300/-- Fquad does NOT have d'Alembert structure. -/
 301theorem Fquad_not_dAlembert_structure : ¬ HasDAlembert Counterexamples.Fquad := by
 302  intro h
 303  unfold HasDAlembert at h
 304  have hH : (fun t => Counterexamples.Fquad (Real.exp t) + 1) = (fun t => t^2/2 + 1) := by
 305    ext t
 306    simp [Counterexamples.Fquad, Cost.F_ofLog, Counterexamples.Gquad, Real.log_exp]
 307  rw [hH] at h
 308  exact Hquad_not_dAlembert h
 309
 310/-! ## Fourth Gate Summary -/
 311
 312/-- **Fourth Gate Theorem**: Jcost satisfies d'Alembert structure; Fquad does not. -/
 313theorem fourth_gate_summary :
 314    HasDAlembert Cost.Jcost ∧
 315    ¬ HasDAlembert Counterexamples.Fquad :=
 316  ⟨Jcost_has_dAlembert_structure, Fquad_not_dAlembert_structure⟩
 317
 318/-! ## Full Inevitability with Four Gates -/
 319
 320/-- **Full Inevitability**: d'Alembert structure + structural axioms forces F = Jcost. -/
 321theorem dAlembert_forces_Jcost (F : ℝ → ℝ)
 322    (hNorm : F 1 = 0)
 323    (hSymm : ∀ x : ℝ, 0 < x → F x = F x⁻¹)
 324    (hSmooth : ContDiff ℝ 2 F)
 325    (hCalib : deriv (deriv (fun t => F (Real.exp t))) 0 = 1)
 326    (hDA : HasDAlembert F) :
 327    ∀ x : ℝ, 0 < x → F x = Cost.Jcost x := by
 328  intro x hx
 329  let G := fun t => F (Real.exp t)
 330  have hGsmooth : ContDiff ℝ 2 G := hSmooth.comp Real.contDiff_exp
 331  have hGnorm : G 0 = 0 := by simp [G, hNorm]
 332  have hGeven : ∀ t, G (-t) = G t := by
 333    intro t
 334    simp only [G, Real.exp_neg]
 335    exact (hSymm (Real.exp t) (Real.exp_pos t)).symm
 336  have hGcosh := dAlembert_forces_Gcosh G hDA hGsmooth hGnorm hGeven hCalib
 337  have hFx : F x = G (Real.log x) := by simp [G, Real.exp_log hx]
 338  rw [hFx, hGcosh (Real.log x)]
 339  simp only [Cost.Jcost]
 340  have hcosh : Real.cosh (Real.log x) = (x + x⁻¹) / 2 := by
 341    rw [Real.cosh_eq, Real.exp_log hx, Real.exp_neg, Real.exp_log hx]
 342  linarith [hcosh]
 343
 344end FourthGate
 345end DAlembert
 346end Foundation
 347end IndisputableMonolith
 348