Encyclopedia Foundation Foundation Dalembert Fourth Gate

ARTICLE 4 claims 4 theorems

Foundation Dalembert Fourth Gate

A classical equation from 18th-century wave theory acts as a filter that isolates one unique cost function in a framework for deriving physics.

Verify this page

The d'Alembert Gate

The d'Alembert functional equation, f(x+y) + f(x-y) = 2f(x)f(y), was studied by Jean le Rond d'Alembert in the 1700s. Its continuous solutions are exactly the hyperbolic cosine functions cosh(λx) for any real λ. This equation appears in wave motion, where it describes how a disturbance spreads, and in functional analysis as a characterization of exponential-like behavior.

In Recognition Science, the framework's library of machine-checked formal theorems uses this equation as the Fourth Gate, a filter that any candidate cost function must pass. A cost function here is a rule that assigns a nonnegative price to a recognition event, a discrete record of some occurrence. The gate demands that a shifted version of the cost function, built by composing it with the exponential map and adding one, satisfies d'Alembert's equation. This is a strong structural condition, not an arbitrary choice.

The module proves that the framework's canonical cost function, J(x) = (x + 1/x)/2 - 1, passes this gate. The proof is direct: the shifted log-lift of J is exactly cosh, and cosh satisfies d'Alembert's equation. The module also proves a converse: any smooth, even cost function with the right calibration that satisfies the gate must equal J. This is the d'Alembert classification theorem, which forces the unique form through an ordinary differential equation. The quadratic counterexample, whose log-lift is t²/2 + 1, fails the gate, showing the condition has teeth.

In Recognition Science, this gate is not an extra assumption. In the framework's Option A formulation, earlier gates already force the cost function to be cosh minus one, so the d'Alembert structure follows automatically. The Fourth Gate is a derived certificate, a convenient cross-check that packages the classical functional-equation viewpoint into a compact proof path. It confirms that the same unique cost function emerges whether one builds it from the composition law or from this classical equation.

What this establishes in plain language is a uniqueness result with a classical pedigree. The cost function that the framework derives from first principles is not one of many possibilities; it is the single smooth candidate that satisfies a 300-year-old equation. The gate turns a historical curiosity into a modern filter, and the filter admits exactly one function.

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 Jcost_has_dAlembert_structure · IndisputableMonolith/Foundation/DAlembert/FourthGate.lean
Jcost_has_dAlembert_structure · IndisputableMonolith/Foundation/DAlembert/FourthGate.lean:63 
/-- Jcost has d'Alembert structure. -/
theorem Jcost_has_dAlembert_structure : HasDAlembert Cost.Jcost := by
  unfold HasDAlembert SatisfiesDAlembert
  constructor
  · simp [Cost.Jcost, Real.exp_zero]
  · intro t u
    have hH : ∀ s, Cost.Jcost (Real.exp s) + 1 = Real.cosh s := by
      intro s
      simp only [Cost.Jcost]
      have hcosh : Real.cosh s = (Real.exp s + Real.exp (-s)) / 2 := Real.cosh_eq s
      have hneg : Real.exp (-s) = (Real.exp s)⁻¹ := Real.exp_neg s
      linarith
    simp only [hH]
    have hcosh := cosh_satisfies_dAlembert.2 t u
    exact hcosh
THEOREM dAlembert_forces_Jcost · IndisputableMonolith/Foundation/DAlembert/FourthGate.lean
dAlembert_forces_Jcost · IndisputableMonolith/Foundation/DAlembert/FourthGate.lean:320 
/-- **Full Inevitability**: d'Alembert structure + structural axioms forces F = Jcost. -/
theorem dAlembert_forces_Jcost (F : ℝ → ℝ)
    (hNorm : F 1 = 0)
    (hSymm : ∀ x : ℝ, 0 < x → F x = F x⁻¹)
    (hSmooth : ContDiff ℝ 2 F)
    (hCalib : deriv (deriv (fun t => F (Real.exp t))) 0 = 1)
    (hDA : HasDAlembert F) :
    ∀ x : ℝ, 0 < x → F x = Cost.Jcost x := by
  intro x hx
  let G := fun t => F (Real.exp t)
  have hGsmooth : ContDiff ℝ 2 G := hSmooth.comp Real.contDiff_exp
  have hGnorm : G 0 = 0 := by simp [G, hNorm]
  have hGeven : ∀ t, G (-t) = G t := by
    intro t
    simp only [G, Real.exp_neg]
    exact (hSymm (Real.exp t) (Real.exp_pos t)).symm
  have hGcosh := dAlembert_forces_Gcosh G hDA hGsmooth hGnorm hGeven hCalib
  have hFx : F x = G (Real.log x) := by simp [G, Real.exp_log hx]
  rw [hFx, hGcosh (Real.log x)]
  simp only [Cost.Jcost]
  have hcosh : Real.cosh (Real.log x) = (x + x⁻¹) / 2 := by
    rw [Real.cosh_eq, Real.exp_log hx, Real.exp_neg, Real.exp_log hx]
  linarith [hcosh]
THEOREM Fquad_not_dAlembert_structure · IndisputableMonolith/Foundation/DAlembert/FourthGate.lean
Fquad_not_dAlembert_structure · IndisputableMonolith/Foundation/DAlembert/FourthGate.lean:300 
/-- Fquad does NOT have d'Alembert structure. -/
theorem Fquad_not_dAlembert_structure : ¬ HasDAlembert Counterexamples.Fquad := by
  intro h
  unfold HasDAlembert at h
  have hH : (fun t => Counterexamples.Fquad (Real.exp t) + 1) = (fun t => t^2/2 + 1) := by
    ext t
    simp [Counterexamples.Fquad, Cost.F_ofLog, Counterexamples.Gquad, Real.log_exp]
  rw [hH] at h
  exact Hquad_not_dAlembert h

What this page does not claim

The Fourth Gate is an independent axiom; it is derived from earlier gates in the Option A formulation. The general λ classification theorem is used in the main forcing chain; only the λ = 1 case is required. The d'Alembert equation itself is a discovery of Recognition Science; it is a classical result from the 18th century.

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