Encyclopedia Cost Cost Cont Diff Reduction D Alembert First Deriv Of Cont Diff

ARTICLE 5 claims 5 theorems

Cost Cont Diff Reduction D Alembert First Deriv Of Cont Diff

A small regularity assumption turns a functional equation into an ordinary differential equation, and that switch is what lets a uniqueness proof go through.

Verify this page

The first derivative step

The d'Alembert equation, named for Jean le Rond d'Alembert's 1747 work on vibrating strings, is the functional equation H(t+u) + H(t-u) = 2 H(t) H(u). It appears whenever a quantity's value at a sum and difference of two inputs is governed by its values at the inputs separately. The equation has many wild solutions if no regularity is assumed; demanding that H be twice continuously differentiable, written C², selects the well-behaved ones.

The declaration dAlembert_first_deriv_of_contDiff proves that if H satisfies the d'Alembert equation and is C², then differentiating once in the second variable yields the identity deriv H(t+u) - deriv H(t-u) = 2 H(t) deriv H(u). This is the first step in a chain: differentiating again at u = 0 gives H''(t) = H(t) H''(0), and with the calibration H''(0) = 1, the function satisfies the ordinary differential equation H'' = H. The unique solution with H(0) = 1 is the hyperbolic cosine, cosh(t) = (e^t + e^-t)/2.

In Recognition Science, the framework models recognition cost as a function J(x) = (x + 1/x)/2 - 1, derived from normalization, a composition law, and calibration. The C² reduction sharpens the earlier theorem: on the twice-differentiable surface, reciprocal symmetry J(x) = J(1/x) is derived from the composition law rather than assumed. The machine-checked library of formal theorems proves that normalization, composition, calibration, and C² regularity of H = J + 1 force the canonical cost.

What the declaration does not claim is broader. It does not prove that every d'Alembert solution is cosh; that requires calibration. It does not establish the cost function without the composition law. It does not show that the C² condition is necessary; merely sufficient. The theorem is a bridge: it converts a functional equation into an ODE, and the ODE is what the uniqueness proof uses.

THEOREM dAlembert_first_deriv_of_contDiff · IndisputableMonolith/Cost/ContDiffReduction.lean
dAlembert_first_deriv_of_contDiff · IndisputableMonolith/Cost/ContDiffReduction.lean:43 
/-- Differentiate the d'Alembert equation once in the second variable. -/
theorem dAlembert_first_deriv_of_contDiff
    (Hf : ℝ → ℝ)
    (h_dAlembert : ∀ t u, Hf (t + u) + Hf (t - u) = 2 * Hf t * Hf u)
    (h_diff : ContDiff ℝ 2 Hf) :
    ∀ t u, deriv Hf (t + u) - deriv Hf (t - u) = 2 * Hf t * deriv Hf u := by
  intro t u
  have h_diff1 : Differentiable ℝ Hf := contDiffTwo_differentiable h_diff
  have h_plus :
      HasDerivAt (fun v => Hf (t + v)) (deriv Hf (t + u)) u := by
    have h_inner : HasDerivAt (fun v => t + v) 1 u := by
      simpa using (hasDerivAt_const u t).add (hasDerivAt_id u)
    simpa using (h_diff1.differentiableAt (x := t + u)).hasDerivAt.comp u h_inner
  have h_minus :
      HasDerivAt (fun v => Hf (t - v)) (-deriv Hf (t - u)) u := by
    have h_inner : HasDerivAt (fun v => t - v) (-1) u := by
      simpa using (hasDerivAt_const u t).sub (hasDerivAt_id u)
    simpa using (h_diff1.differentiableAt (x := t - u)).hasDerivAt.comp u h_inner
  have h_left :
      HasDerivAt (fun v => Hf (t + v) + Hf (t - v))
        (deriv Hf (t + u) - deriv Hf (t - u)) u := by
    simpa using h_plus.add h_minus
  have h_const : HasDerivAt (fun _ : ℝ => 2 * Hf t) 0 u :=
    hasDerivAt_const u (2 * Hf t)
  have h_right :
      HasDerivAt (((fun _ : ℝ => 2 * Hf t) * Hf)) (2 * (Hf t * deriv Hf u)) u := by
    simpa [mul_assoc] using h_const.mul ((h_diff1.differentiableAt (x := u)).hasDerivAt)
  have h_eq :
      (fun v => Hf (t + v) + Hf (t - v)) = ((fun _ : ℝ => 2 * Hf t) * Hf) := by
    funext v
    simpa [Pi.mul_apply, mul_assoc] using h_dAlembert t v
  have h_deriv_eq := congrArg (fun f : ℝ → ℝ => deriv f u) h_eq
  change deriv (fun v => Hf (t + v) + Hf (t - v)) u =
      deriv (((fun _ : ℝ => 2 * Hf t) * Hf)) u at h_deriv_eq
  rw [h_left.deriv, h_right.deriv] at h_deriv_eq
  simpa [mul_assoc] using h_deriv_eq
THEOREM dAlembert_second_deriv_at_zero_of_contDiff · dAlembert_to_ODE_of_contDiff · IndisputableMonolith/Cost/ContDiffReduction.lean
dAlembert_second_deriv_at_zero_of_contDiff · IndisputableMonolith/Cost/ContDiffReduction.lean:80 
/-- Differentiate the first-derivative identity at `u = 0` to relate `H''(t)` to `H''(0)`. -/
theorem dAlembert_second_deriv_at_zero_of_contDiff
    (Hf : ℝ → ℝ)
    (h_dAlembert : ∀ t u, Hf (t + u) + Hf (t - u) = 2 * Hf t * Hf u)
    (h_diff : ContDiff ℝ 2 Hf) :
    ∀ t, 2 * deriv (deriv Hf) t = 2 * Hf t * deriv (deriv Hf) 0 := by
  intro t
  have h_first :
      (fun u => deriv Hf (t + u) - deriv Hf (t - u)) =
        ((fun _ : ℝ => 2 * Hf t) * deriv Hf) := by
    funext u
    simpa [Pi.mul_apply, mul_assoc] using
      dAlembert_first_deriv_of_contDiff Hf h_dAlembert h_diff t u
  have h_plus :
      HasDerivAt (fun u => deriv Hf (t + u)) (deriv (deriv Hf) t) 0 := by
    have h_inner : HasDerivAt (fun u => t + u) 1 0 := by
      simpa using (hasDerivAt_const 0 t).add (hasDerivAt_id 0)
    simpa using (hasDerivAt_deriv_of_contDiffTwo h_diff (t + 0)).comp 0 h_inner
  have h_minus_raw :
      HasDerivAt (fun u => deriv Hf (t - u)) (-deriv (deriv Hf) t) 0 := by
    have h_inner : HasDerivAt (fun u => t - u) (-1) 0 := by
      simpa using (hasDerivAt_const 0 t).sub (hasDerivAt_id 0)
    simpa using (hasDerivAt_deriv_of_contDiffTwo h_diff (t - 0)).comp 0 h_inner
  have h_left_raw :
      HasDerivAt (fun u => deriv Hf (t + u) - deriv Hf (t - u))
        (deriv (deriv Hf) t + deriv (deriv Hf) t) 0 := by
    simpa using h_plus.sub h_minus_raw
  have h_const : HasDerivAt (fun _ : ℝ => 2 * Hf t) 0 0 :=
    hasDerivAt_const 0 (2 * Hf t)
  have h_right :
      HasDerivAt (((fun _ : ℝ => 2 * Hf t) * deriv Hf))
        (2 * (Hf t * deriv (deriv Hf) 0)) 0 := by
    simpa [mul_assoc] using h_const.mul (hasDerivAt_deriv_of_contDiffTwo h_diff 0)
  have h_deriv_eq := congrArg (fun f : ℝ → ℝ => deriv f 0) h_first
  change deriv (fun u => deriv Hf (t + u) - deriv Hf (t - u)) 0 =
      deriv (((fun _ : ℝ => 2 * Hf t) * deriv Hf)) 0 at h_deriv_eq
  rw [h_left_raw.deriv, h_right.deriv] at h_deriv_eq
  linarith
dAlembert_to_ODE_of_contDiff · IndisputableMonolith/Cost/ContDiffReduction.lean:119 
/-- A `C²` d'Alembert solution with calibrated second derivative satisfies `H'' = H`. -/
theorem dAlembert_to_ODE_of_contDiff
    (Hf : ℝ → ℝ)
    (h_dAlembert : ∀ t u, Hf (t + u) + Hf (t - u) = 2 * Hf t * Hf u)
    (h_diff : ContDiff ℝ 2 Hf)
    (h_deriv2_zero : deriv (deriv Hf) 0 = 1) :
    ∀ t, deriv (deriv Hf) t = Hf t := by
  intro t
  have h_rel := dAlembert_second_deriv_at_zero_of_contDiff Hf h_dAlembert h_diff t
  rw [h_deriv2_zero] at h_rel
  linarith
THEOREM dAlembert_cosh_solution_of_contDiff · IndisputableMonolith/Cost/ContDiffReduction.lean
dAlembert_cosh_solution_of_contDiff · IndisputableMonolith/Cost/ContDiffReduction.lean:169 
/-- `C²` d'Alembert solutions are determined by calibration and equal `cosh`. -/
theorem dAlembert_cosh_solution_of_contDiff
    (Hf : ℝ → ℝ)
    (h_one : Hf 0 = 1)
    (h_dAlembert : ∀ t u, Hf (t + u) + Hf (t - u) = 2 * Hf t * Hf u)
    (h_diff : ContDiff ℝ 2 Hf)
    (h_deriv2_zero : deriv (deriv Hf) 0 = 1) :
    ∀ t, Hf t = Real.cosh t := by
  have h_ode : ∀ t, deriv (deriv Hf) t = Hf t :=
    dAlembert_to_ODE_of_contDiff Hf h_dAlembert h_diff h_deriv2_zero
  have h_even : Function.Even Hf := dAlembert_even Hf h_one h_dAlembert
  have h_diff0 : DifferentiableAt ℝ Hf 0 :=
    (contDiffTwo_differentiable h_diff).differentiableAt
  have h_deriv_zero : deriv Hf 0 = 0 :=
    even_deriv_at_zero Hf h_even h_diff0
  exact ode_cosh_uniqueness_contdiff Hf h_diff h_ode h_one h_deriv_zero
THEOREM composition_law_forces_reciprocity · IndisputableMonolith/Cost/ContDiffReduction.lean
composition_law_forces_reciprocity · IndisputableMonolith/Cost/ContDiffReduction.lean:138 
/-- A normalized composition-law cost is automatically reciprocal. -/
theorem composition_law_forces_reciprocity
    (F : ℝ → ℝ)
    (hNorm : IsNormalized F)
    (hComp : SatisfiesCompositionLaw F) :
    IsReciprocalCost F := by
  intro x hx
  let Hf : ℝ → ℝ := H F
  have h_H0 : Hf 0 = 1 := by
    dsimp [Hf]
    simpa [H, G, IsNormalized] using hNorm
  have hCoshAdd : CoshAddIdentity F := (composition_law_equiv_coshAdd F).mp hComp
  have h_direct : DirectCoshAdd (G F) := CoshAddIdentity_implies_DirectCoshAdd F hCoshAdd
  have h_dAlembert : ∀ t u, Hf (t + u) + Hf (t - u) = 2 * Hf t * Hf u := by
    intro t u
    have hG := h_direct t u
    have h_goal :
        (G F (t + u) + 1) + (G F (t - u) + 1) = 2 * (G F t + 1) * (G F u + 1) := by
      calc
        (G F (t + u) + 1) + (G F (t - u) + 1)
            = (G F (t + u) + G F (t - u)) + 2 := by ring
        _ = (2 * (G F t * G F u) + 2 * (G F t + G F u)) + 2 := by simpa [hG]
        _ = 2 * (G F t + 1) * (G F u + 1) := by ring
    simpa [Hf, H] using h_goal
  have h_even : Function.Even Hf := dAlembert_even Hf h_H0 h_dAlembert
  have h_even_at_log := h_even (Real.log x)
  have h_eq_plus :
      F x + 1 = F x⁻¹ + 1 := by
    simpa [Hf, H, G, Real.exp_log hx, Real.exp_neg] using h_even_at_log.symm
  linarith
THEOREM law_of_logic_forces_jcost_of_contDiff · IndisputableMonolith/Cost/ContDiffReduction.lean
law_of_logic_forces_jcost_of_contDiff · IndisputableMonolith/Cost/ContDiffReduction.lean:186 
/-- Sharpened T5 surface:
normalization, the composition law, calibration, and `C²` regularity of `H = G + 1`
already force the canonical reciprocal cost. Reciprocal symmetry is derived, not assumed. -/
theorem law_of_logic_forces_jcost_of_contDiff
    (F : ℝ → ℝ)
    (hNorm : IsNormalized F)
    (hComp : SatisfiesCompositionLaw F)
    (hCalib : IsCalibrated F)
    (h_diff : ContDiff ℝ 2 (H F)) :
    ∀ x : ℝ, 0 < x → F x = Cost.Jcost x := by
  intro x hx
  let Gf : ℝ → ℝ := G F
  let Hf : ℝ → ℝ := H F
  have hCoshAdd : CoshAddIdentity F := (composition_law_equiv_coshAdd F).mp hComp
  have h_direct : DirectCoshAdd Gf := CoshAddIdentity_implies_DirectCoshAdd F hCoshAdd
  have h_H0 : Hf 0 = 1 := by
    dsimp [Hf]
    simpa [H, G, IsNormalized] using hNorm
  have h_dAlembert : ∀ t u, Hf (t + u) + Hf (t - u) = 2 * Hf t * Hf u := by
    intro t u
    have hG := h_direct t u
    have h_goal :
        (Gf (t + u) + 1) + (Gf (t - u) + 1) = 2 * (Gf t + 1) * (Gf u + 1) := by
      calc
        (Gf (t + u) + 1) + (Gf (t - u) + 1)
            = (Gf (t + u) + Gf (t - u)) + 2 := by ring
        _ = (2 * (Gf t * Gf u) + 2 * (Gf t + Gf u)) + 2 := by simp [hG]
        _ = 2 * (Gf t + 1) * (Gf u + 1) := by ring
    simpa [Hf, H, Gf] using h_goal
  have h_H_d2 : deriv (deriv Hf) 0 = 1 := by
    have hG_d2 : deriv (deriv Gf) 0 = 1 := by
      simpa [Gf, G, IsCalibrated] using hCalib
    have hderiv : deriv Hf = deriv Gf := by
      funext t
      change deriv (fun y => Gf y + 1) t = deriv Gf t
      exact deriv_add_const (f := Gf) (x := t) (c := (1 : ℝ))
    have hderiv2 : deriv (deriv Hf) = deriv (deriv Gf) := congrArg deriv hderiv
    exact (congrArg (fun g => g 0) hderiv2).trans hG_d2
  have h_H_cosh : ∀ t, Hf t = Real.cosh t :=
    dAlembert_cosh_solution_of_contDiff Hf h_H0 h_dAlembert (by simpa [Hf] using h_diff) h_H_d2
  have h_G_cosh : ∀ t, Gf t = Real.cosh t - 1 := by
    intro t
    have hH := h_H_cosh t
    have hH' : Gf t + 1 = Real.cosh t := by
      simpa [Hf, H, Gf] using hH
    linarith
  have ht : Real.exp (Real.log x) = x := Real.exp_log hx
  have hJG : G Cost.Jcost (Real.log x) = Real.cosh (Real.log x) - 1 :=
    Jcost_G_eq_cosh_sub_one (Real.log x)
  calc
    F x = F (Real.exp (Real.log x)) := by rw [ht]
    _ = Gf (Real.log x) := rfl
    _ = Real.cosh (Real.log x) - 1 := h_G_cosh (Real.log x)
    _ = G Cost.Jcost (Real.log x) := by simpa using hJG.symm
    _ = Cost.Jcost (Real.exp (Real.log x)) := by simp [G]
    _ = Cost.Jcost x := by rw [ht]

What this page does not claim

The declaration does not prove that every d'Alembert solution is cosh without calibration. The declaration does not establish the cost function without the composition law. The declaration does not show that the C² condition is necessary, only sufficient.

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/Cost/ContDiffReduction.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