Encyclopedia Foundation Foundation Dalembert Fourth Gate Cosh Satisfies D Alembert

ARTICLE 3 claims 3 theorems

Foundation Dalembert Fourth Gate Cosh Satisfies D Alembert

The hyperbolic cosine obeys a famous functional equation; in this framework, that equation is one of the gates any cost function must pass.

Verify this page

The d'Alembert equation

The d'Alembert functional equation is a classical relation from 18th-century mathematics. It asks for functions f that satisfy f(x+y) + f(x-y) = 2 f(x) f(y) for all real x and y. The standard continuous solutions are exactly the hyperbolic cosines, cosh(λx), for any real λ. The equation was studied by Jean le Rond d'Alembert, and its classification is a textbook result in functional equation theory.

The hyperbolic cosine itself, cosh(t) = (e^t + e^-t)/2, is the even part of the exponential function. It satisfies the equation with λ = 1. Its graph is a catenary, the shape a hanging chain takes under gravity. In this framework, the equation appears as the Fourth Gate: a condition on the shifted log-lift of a cost function, the function that assigns a recognition cost to a ratio. The shifted log-lift is H(t) = F(e^t) + 1, where F is the cost. The gate requires this H to satisfy d'Alembert's equation.

The declaration cosh_satisfies_dAlembert is a machine-checked theorem in the framework's library of formal theorems. It proves that Real.cosh, the hyperbolic cosine, satisfies the d'Alembert functional equation with the normalization H(0) = 1. The proof is direct: it uses the standard addition and subtraction formulas for cosh and verifies the equation algebraically. This is not a new mathematical discovery; it is a formal certificate that a known fact holds in the library's language.

What the declaration does not claim is more interesting. It does not claim that cosh is the only solution, nor that it is the solution selected by the framework. The classification theorem, also in the library, states that all C² solutions are cosh(λx). The framework's forcing chain then uses a specific calibration, H''(0) = 1, to select λ = 1 and thus H = cosh. The declaration cosh_satisfies_dAlembert only establishes that cosh is one solution, not that it is the unique one. It also does not claim that the d'Alembert equation alone forces the cost function; the full inevitability result requires the structural axioms and calibration alongside it.

The practical consequence is a cross-check. The framework's cost function J(x) = (x + 1/x)/2 - 1 has a shifted log-lift that equals cosh. The theorem confirms this in the library, so the Fourth Gate is satisfied by the canonical cost. It also provides a compact certificate path: the classical d'Alembert classification theorem, packaged as a formal result, supports the framework's derivation without adding new assumptions.

THEOREM cosh_satisfies_dAlembert · IndisputableMonolith/Foundation/DAlembert/FourthGate.lean
cosh_satisfies_dAlembert · IndisputableMonolith/Foundation/DAlembert/FourthGate.lean:54 
/-- cosh satisfies the d'Alembert equation. -/
theorem cosh_satisfies_dAlembert : SatisfiesDAlembert Real.cosh := by
  constructor
  · exact Real.cosh_zero
  · intro t u
    have h1 := Real.cosh_add t u
    have h2 := Real.cosh_sub t u
    linarith
THEOREM cosh_satisfies_dAlembert · IndisputableMonolith/Foundation/DAlembert/FourthGate.lean
cosh_satisfies_dAlembert · IndisputableMonolith/Foundation/DAlembert/FourthGate.lean:54 
/-- cosh satisfies the d'Alembert equation. -/
theorem cosh_satisfies_dAlembert : SatisfiesDAlembert Real.cosh := by
  constructor
  · exact Real.cosh_zero
  · intro t u
    have h1 := Real.cosh_add t u
    have h2 := Real.cosh_sub t u
    linarith
THEOREM dAlembert_classification · IndisputableMonolith/Foundation/DAlembert/FourthGate.lean
dAlembert_classification · IndisputableMonolith/Foundation/DAlembert/FourthGate.lean:163 
/-- **Theorem (d'Alembert Classification)**: If H is C², satisfies d'Alembert,
    H(0) = 1, H'(0) = 0, and H''(0) = λ², then H(t) = cosh(λt).

    **Note**: This general λ version is not used in the main forcing chain.
    The framework only requires the λ = 1 case, which is proved in
    `dAlembert_with_unit_calibration`. The general case reduces to it by scaling:
    For λ ≠ 0, define K(s) = H(s/λ); then K'' = K, K(0)=1, K'(0)=0, so K = cosh,
    hence H(t) = cosh(λt). For λ = 0, H'' = 0 gives H = 1 = cosh(0).
    Formalizing the scaling argument requires careful chain-rule handling. -/
theorem dAlembert_classification :
    ∀ H : ℝ → ℝ, ∀ lam : ℝ,
    SatisfiesDAlembert H →
    ContDiff ℝ 2 H →
    deriv H 0 = 0 →
    deriv (deriv H) 0 = lam ^ 2 →
    ∀ t, H t = Real.cosh (lam * t) := by
  intro H lam hDA hSmooth hDeriv0 hCalib t
  have h_ode : ∀ x, deriv (deriv H) x = deriv (deriv H) 0 * H x :=
    dalembert_deriv_ode H hSmooth hDA.2
  by_cases hlam : lam = 0
  · -- λ = 0: H'' = 0, so H is constant; H(0)=1, H'(0)=0 ⇒ H = 1 = cosh(0)
    subst hlam
    have hode0 : ∀ x, deriv (deriv H) x = 0 := fun x => by
      rw [h_ode x, hCalib, zero_pow two_ne_zero]; exact zero_mul (H x)
    -- H''=0 ⇒ deriv H constant; deriv H 0 = 0 ⇒ deriv H = 0 ⇒ H constant; H 0 = 1 ⇒ H = 1
    have hd_deriv : Differentiable ℝ (deriv H) := hSmooth.differentiable_deriv_two
    have hH'0 : ∀ x, deriv H x = 0 := fun x => (is_const_of_deriv_eq_zero hd_deriv hode0 x 0).trans hDeriv0
    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
    simp only [hH_const t, zero_mul, Real.cosh_zero]
  · -- λ ≠ 0: K(s) = H(s/λ) satisfies K'' = K, K(0)=1, K'(0)=0, K''(0)=1; apply unit calibration.
    let K := fun s => H (s / lam)
    have hK0 : K 0 = 1 := by simp [K, hDA.1]
    have hK_DA : SatisfiesDAlembert K := by
      constructor; exact hK0
      intro t u
      simp only [K]
      have ht : (t + u) / lam = t / lam + u / lam := by field_simp [hlam]
      have ht' : (t - u) / lam = t / lam - u / lam := by field_simp [hlam]
      rw [ht, ht']
      exact hDA.2 (t / lam) (u / lam)
    have hK_smooth : ContDiff ℝ 2 K :=
      ContDiff.comp hSmooth ((contDiff_id.div_const lam).of_le le_top)
    have hK'_0 : deriv K 0 = 0 := by
      have K_eq : K = fun s => H ((1/lam) * s) := by ext s; simp [K]; congr 1; field_simp [hlam]
      rw [K_eq, deriv_comp_mul_left (1/lam) H 0]
      rw [show (1/lam) * 0 = 0 from by ring, hDeriv0]; simp
    have hK''_0 : deriv (deriv K) 0 = 1 := by
      have K_eq : K = fun s => H ((1/lam) * s) := by ext s; simp [K]; congr 1; field_simp [hlam]
      have dK : deriv K = fun s => (1/lam) * deriv H (s/lam) := by
        ext s
        rw [K_eq, deriv_comp_mul_left (1/lam) H s, smul_eq_mul]
        rw [show (1/lam) * s = s / lam from by field_simp [hlam]]
      rw [dK, deriv_const_mul_field (1/lam)]
      rw [show (fun s => deriv H (s/lam)) = fun s => (deriv H) ((1/lam) * s) from by ext s; congr 1; field_simp [hlam]]
      rw [deriv_comp_mul_left (1/lam) (deriv H) 0, smul_eq_mul]
      rw [show (1/lam) * 0 = 0 from by ring, h_ode 0, hCalib, hDA.1]
      field_simp [hlam]
    have hK_ode : ∀ s, deriv (deriv K) s = K s := by
      intro s
      have K_eq : K = fun z => H ((1/lam) * z) := by ext z; simp [K]; congr 1; field_simp [hlam]
      have dK : deriv K = fun x => (1/lam) * deriv H (x/lam) := by
        ext x
        rw [K_eq, deriv_comp_mul_left (1/lam) H x, smul_eq_mul]
        rw [show (1/lam) * x = x / lam from by field_simp [hlam]]
      rw [dK, deriv_const_mul_field (1/lam)]
      rw [show (fun x => deriv H (x/lam)) = fun x => (deriv H) ((1/lam) * x) from by ext x; congr 1; field_simp [hlam]]
      rw [deriv_comp_mul_left (1/lam) (deriv H) s, smul_eq_mul]
      rw [show (1/lam) * s = s / lam from by field_simp [hlam], h_ode (s/lam)]
      simp only [K, hCalib]; field_simp [hlam]
    have hK_eq_cosh : ∀ s, K s = Real.cosh s :=
      Cost.FunctionalEquation.ode_cosh_uniqueness_contdiff K hK_smooth hK_ode hK0 hK'_0
    have h_eq : K (lam * t) = H t := by simp [K]; field_simp [hlam]
    rw [← h_eq, hK_eq_cosh (lam * t)]

What this page does not claim

The declaration does not claim that cosh is the unique solution to the d'Alembert equation. It does not claim that the d'Alembert equation alone forces the canonical cost function J(x). It does not claim that the hyperbolic cosine is a cost function itself, only that it satisfies a structural equation.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/DAlembert/FourthGate.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND