Foundation Dalembert Fourth Gate D Alembert With Unit Calibration

The d'Alembert equation and its unique solution

The d'Alembert functional equation, f(x+y) + f(x-y) = 2f(x)f(y), is a classical object in mathematics. Jean le Rond d'Alembert studied it in the 18th century. Its continuous solutions are exactly the hyperbolic cosine functions cosh(λx) for any real λ. This means the equation alone does not pick a single function; it allows a whole family, one for each value of the scaling parameter λ.

What selects a unique member of that family is a calibration condition. If a function H is twice continuously differentiable, satisfies the d'Alembert equation, has H(0)=1, H'(0)=0, and its second derivative at zero equals 1, then H must be exactly cosh(t). The theorem named dAlembert_with_unit_calibration in the framework's machine-checked library of formal theorems states precisely this. It proves that the unit calibration H''(0)=1 forces the λ=1 case, eliminating all other scalings.

In Recognition Science, this result serves as the Fourth Gate in a chain that derives the cost function J(x) = (x + 1/x)/2 - 1. The framework models recognition costs as functions on positive reals, and the shifted log-lift H(t) = F(e^t) + 1 is required to satisfy d'Alembert. The unit calibration is not an extra assumption; it follows from earlier gates. The theorem dAlembert_forces_Gcosh shows that with d'Alembert structure, smoothness, evenness, and the unit calibration, the underlying function G must equal cosh(t) - 1.

The declaration also participates in a contrast. A quadratic candidate, H(t) = t²/2 + 1, fails the d'Alembert equation, and the library proves this in Hquad_not_dAlembert. The summary theorem fourth_gate_summary packages both facts: the true cost Jcost satisfies the d'Alembert structure, and the quadratic counterexample does not. This separation is what makes the gate a genuine filter rather than a formality.

What the declaration does not claim is broader than what it proves. It does not establish the full forcing chain from recognition axioms to Jcost; that requires additional structural premises like symmetry and normalization, which appear in the separate theorem dAlembert_forces_Jcost. It does not prove the general classification for arbitrary λ, which remains a paper-level derivation. The unit calibration itself is not derived within this declaration; it is a premise taken as given, though the framework derives it elsewhere in the chain.

/-- **Corollary**: With calibration H''(0) = 1, we get H = cosh.
    Proof: dalembert_deriv_ode gives H''(t) = H''(0)·H(t); substituting H''(0) = 1
    gives H'' = H; ODE uniqueness (H(0)=1, H'(0)=0) then forces H = cosh. -/
theorem dAlembert_with_unit_calibration (H : ℝ → ℝ)
    (hDA : SatisfiesDAlembert H)
    (hSmooth : ContDiff ℝ 2 H)
    (hDeriv0 : deriv H 0 = 0)
    (hCalib : deriv (deriv H) 0 = 1) :
    ∀ t, H t = Real.cosh t := by
  -- Step 1: H''(t) = H''(0) · H(t) from d'Alembert + C²
  have hode_gen : ∀ x, deriv (deriv H) x = deriv (deriv H) 0 * H x :=
    dalembert_deriv_ode H hSmooth hDA.2
  -- Step 2: Substitute H''(0) = 1 to get the canonical ODE H'' = H
  have hode : ∀ t, deriv (deriv H) t = H t := fun t => by
    rw [hode_gen t, hCalib, one_mul]
  -- Step 3: H(0) = 1 (from SatisfiesDAlembert)
  have hH0 : H 0 = 1 := hDA.1
  -- Step 4: ODE uniqueness — the unique C² solution to H'' = H, H(0) = 1, H'(0) = 0 is cosh
  exact Cost.FunctionalEquation.ode_cosh_uniqueness_contdiff H hSmooth hode hH0 hDeriv0

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

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

/-- **Fourth Gate Theorem**: Jcost satisfies d'Alembert structure; Fquad does not. -/
theorem fourth_gate_summary :
    HasDAlembert Cost.Jcost ∧
    ¬ HasDAlembert Counterexamples.Fquad :=
  ⟨Jcost_has_dAlembert_structure, Fquad_not_dAlembert_structure⟩

What this page does not claim

The declaration does not prove the full forcing chain from recognition axioms to Jcost. The declaration does not derive the unit calibration; it takes it as a premise. The general classification for arbitrary λ is not formalized in this declaration.

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: