Encyclopedia Foundation Foundation Dalembert Fourth Gate D Alembert Forces Gcosh

ARTICLE 3 claims 3 theorems

Foundation Dalembert Fourth Gate D Alembert Forces Gcosh

A single functional equation, known since the 18th century, pins down the entire shape of a recognition cost curve, leaving no freedom for alternatives.

Verify this page

The forced shape of the cost curve

The French mathematician Jean le Rond d'Alembert studied an equation in the 1700s that asks for functions where the value at a sum and the value at a difference combine in a fixed way: for all numbers t and u, f(t+u) + f(t-u) = 2 f(t) f(u). Its continuous solutions are exactly the hyperbolic cosine functions cosh(λt), with λ any real number. This is a classical result in functional equation theory, and it is the backbone of the Recognition Science framework's fourth gate.

In the framework, a recognition cost is a function that measures the price of acknowledging an event, and the framework models it through a shifted log-lift: for a cost function F, define H(t) = F(e^t) + 1. The fourth gate demands that H satisfy d'Alembert's equation. The declaration dAlembert_forces_Gcosh proves that if a function G satisfies this structure, is twice continuously differentiable, is even, vanishes at zero, and has a calibrated second derivative at zero equal to 1, then G(t) = cosh(t) - 1 for every t. There is no other possibility under these conditions.

The proof works by differentiating the d'Alembert equation twice, which yields the differential equation G''(t) = G(t) + 1. With the initial conditions G(0) = 0 and G''(0) = 1, the unique solution is cosh(t) - 1. The framework's library of machine-checked formal theorems records this as a proved result, not a hypothesis. The same library also shows that a quadratic alternative, H(t) = t²/2 + 1, fails the d'Alembert test, confirming that the gate is genuinely restrictive.

What the declaration does not claim is broader. It does not claim that the d'Alembert equation alone forces the cost function; the calibration condition G''(0) = 1 is essential, and without it the general solution is cosh(λt) for arbitrary λ. It does not claim that the cost function J(x) = (x + 1/x)/2 - 1 is the only function satisfying the framework's axioms, since that requires the full chain of gates. And it does not claim anything about the physical interpretation of the cost function, which the framework treats as a separate modeling step.

THEOREM dAlembert_forces_Gcosh · IndisputableMonolith/Foundation/DAlembert/FourthGate.lean
dAlembert_forces_Gcosh · IndisputableMonolith/Foundation/DAlembert/FourthGate.lean:259 
/-- d'Alembert structure + calibration forces G = cosh - 1. -/
theorem dAlembert_forces_Gcosh (G : ℝ → ℝ)
    (hDA : SatisfiesDAlembert (fun t => G t + 1))
    (hSmooth : ContDiff ℝ 2 G)
    (_ : G 0 = 0)
    (hEven : ∀ t, G (-t) = G t)
    (hCalib : deriv (deriv G) 0 = 1) :
    ∀ t, G t = Real.cosh t - 1 := by
  let H := fun t => G t + 1
  have hHsmooth : ContDiff ℝ 2 H := hSmooth.add contDiff_const
  have hHderiv0 : deriv H 0 = 0 := by
    have hderivH : deriv H = deriv G := by ext t; simp [H, deriv_add_const]
    rw [hderivH]
    have hGeven : (fun t => G (-t)) = G := funext hEven
    have hcomp : deriv (fun t => G (-t)) 0 = deriv G 0 := by simp only [hGeven]
    have hchain : deriv (fun t => G (-t)) 0 = -(deriv G 0) := by
      have heq : (fun t => G (-t)) = G ∘ (fun t => -t) := rfl
      rw [heq]
      have hGdiff : DifferentiableAt ℝ G 0 := hSmooth.differentiable (by norm_num) |>.differentiableAt
      rw [deriv_comp (0 : ℝ) (by simp only [neg_zero]; exact hGdiff) differentiable_neg.differentiableAt]
      simp only [neg_zero, deriv_neg', mul_neg_one]
    rw [hchain] at hcomp
    linarith
  have hHcalib : deriv (deriv H) 0 = 1 := by
    have h1 : deriv H = deriv G := by ext t; simp [H, deriv_add_const]
    have h2 : deriv (deriv H) = deriv (deriv G) := by simp [h1]
    rw [h2, hCalib]
  have hHcosh := dAlembert_with_unit_calibration H hDA hHsmooth hHderiv0 hHcalib
  intro t
  have := hHcosh t
  simp only [H] at this
  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)]
THEOREM Hquad_not_dAlembert · IndisputableMonolith/Foundation/DAlembert/FourthGate.lean
Hquad_not_dAlembert · IndisputableMonolith/Foundation/DAlembert/FourthGate.lean:294 
/-- The quadratic log-lift H(t) = t²/2 + 1 does NOT satisfy d'Alembert. -/
theorem Hquad_not_dAlembert : ¬ SatisfiesDAlembert (fun t => t^2/2 + 1) := by
  intro ⟨_, hda⟩
  have h11 := hda 1 1
  norm_num at h11

What this page does not claim

The d'Alembert equation alone, without the calibration G''(0) = 1, does not force the specific solution cosh(t) - 1. The declaration does not prove that J(x) = (x + 1/x)/2 - 1 is the only function satisfying the framework's full set of axioms. The declaration makes no claim about the physical interpretation or empirical content of the cost function.

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