Foundation Dalembert Fourth Gate Jcost Has D Alembert Structure

The d'Alembert gate

Jean le Rond d'Alembert, studying vibrating strings in the 1740s, wrote down a functional equation that bears his name: f(x+y) + f(x-y) = 2f(x)f(y). Its continuous solutions are exactly the hyperbolic cosines, cosh(λx), for any real λ. The equation expresses a deep symmetry: the value at two shifted points determines the product of values at the original points.

In the Recognition Science framework, the cost function J(x) = (x + 1/x)/2 - 1 is forced by five plain axioms. The declaration Jcost_has_dAlembert_structure establishes that this cost function, when transformed by the shifted log-lift H(t) = J(eᵗ) + 1, satisfies d'Alembert's equation. Since J(eᵗ) = cosh(t) - 1, the lift H(t) is exactly cosh(t), which trivially satisfies the equation. The theorem is a cross-check: the unique cost function already has this classical structure built in, not as an extra assumption but as a derived consequence.

The declaration does not claim that d'Alembert's equation alone forces J. The equation admits a whole family of solutions, cosh(λx), and only the calibration condition H''(0) = 1 selects the λ = 1 case. Nor does it claim that the framework's other candidate cost functions satisfy the equation. In fact, the quadratic cost Fquad(x) = (x - 1)²/2 fails the d'Alembert gate, as the theorem Fquad_not_dAlembert_structure shows. This contrast is the gate's purpose: it separates the forced cost from its near misses.

What the declaration changes is the route to inevitability. The framework's library proves dAlembert_forces_Jcost: if a function F is normalized, symmetric, smooth, calibrated, and has d'Alembert structure, then F equals Jcost everywhere on positive reals. This packages the classical functional-equation viewpoint as a compact certificate path, making the uniqueness result checkable through a different door than the original forcing chain.

/-- 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

/-- 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

/-- **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]

What this page does not claim

The d'Alembert equation alone forces J; it only does so together with normalization, symmetry, smoothness, and calibration. All candidate cost functions in the framework satisfy the d'Alembert gate; Fquad is a proved counterexample. The declaration proves the full forcing chain; it is one cross-check within a larger library.

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: