Encyclopedia Cost Cost Cont Diff Reduction Has Deriv At Deriv Of Cont Diff Two

ARTICLE 4 claims 4 theorems

Cost Cont Diff Reduction Has Deriv At Deriv Of Cont Diff Two

A technical lemma in a machine-checked library shows that a twice-smooth function has a derivative that is itself differentiable, a step toward proving a unique cost function.

Verify this page

The differentiability bridge

In classical analysis, a function that is twice continuously differentiable, often written C², has a first derivative that is itself differentiable. The declaration hasDerivAt_deriv_of_contDiffTwo formalizes exactly this fact inside the Recognition Science framework's machine-checked library: if a real-valued function H is C², then at every point x, the derivative of H has a derivative at x, and that value equals the second derivative of H at x. This is a standard result from calculus, restated as a formal lemma.

The lemma is a bridge, not a destination. It is used to differentiate the d'Alembert equation, a functional equation of the form H(t+u) + H(t-u) = 2 H(t) H(u), once and then twice. Differentiating this equation in the second variable at u = 0 produces a relation between the second derivative of H at t and its value at zero. With a calibration condition, this relation simplifies to the ordinary differential equation H'' = H, whose solutions are the hyperbolic cosine and its multiples.

In Recognition Science, this chain of reasoning supports a larger claim. The framework models recognition events in a discrete ledger, a record of events with a forced cost. The cost function J(x) = (x + 1/x)/2 - 1 is proved to be the unique function satisfying normalization, a composition law, and calibration, given C² regularity. The differentiability lemma is one of the regularity assumptions that makes this proof go through; it ensures that the derivative operations used in the derivation are valid.

The lemma does not, by itself, prove the uniqueness of the cost function, nor does it establish any property of the cost function directly. It is a technical tool about differentiability, not a statement about recognition or cost. The lemma also does not claim that every C² function satisfies the d'Alembert equation; it only states a fact about derivatives under the C² assumption. The framework's broader theorems, such as the uniqueness of J, rely on this lemma together with other hypotheses.

THEOREM hasDerivAt_deriv_of_contDiffTwo · IndisputableMonolith/Cost/ContDiffReduction.lean
hasDerivAt_deriv_of_contDiffTwo · IndisputableMonolith/Cost/ContDiffReduction.lean:38 
private lemma hasDerivAt_deriv_of_contDiffTwo {Hf : ℝ → ℝ}
    (h_diff : ContDiff ℝ 2 Hf) (x : ℝ) :
    HasDerivAt (deriv Hf) (deriv (deriv Hf) x) x := by
  exact (contDiffTwo_differentiable_deriv h_diff).differentiableAt.hasDerivAt
THEOREM dAlembert_second_deriv_at_zero_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
THEOREM dAlembert_to_ODE_of_contDiff · IndisputableMonolith/Cost/ContDiffReduction.lean
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 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 lemma does not prove the uniqueness of the cost function by itself. The lemma does not state that every C² function satisfies the d'Alembert equation. The lemma does not establish any property of the cost function directly.

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