Encyclopedia Cost Cost Functional Equation D Alembert Continuous Of Log Curvature

ARTICLE 3 claims 2 theorems 1 model

Cost Functional Equation D Alembert Continuous Of Log Curvature

A single regularity condition, called log-curvature, turns a purely algebraic functional equation into a proof that its only solution is the familiar hyperbolic cosine.

Verify this page

The continuity bridge

The d'Alembert equation, H(t+u) + H(t-u) = 2 H(t) H(u), is a classical functional equation studied since the 18th century. It asks for functions whose value at a sum and difference of two inputs relates to the product of their individual values. Without any regularity assumptions, it admits many wild, discontinuous solutions. The theorem dAlembert_continuous_of_log_curvature shows that adding one local condition near zero, called log-curvature, forces any such function to be continuous everywhere.

The condition is concrete. A function H with H(0) = 1 has log-curvature κ if the ratio 2(H(t) - 1)/t² approaches κ as t approaches 0. This measures how sharply H bends at the origin, a second-derivative-like quantity defined without assuming differentiability. The theorem states that if H satisfies the d'Alembert equation, has H(0) = 1, and has any finite log-curvature κ, then H is continuous on the entire real line. This is a pure regularity result: it upgrades a local condition to a global one using only the algebraic structure of the equation.

In the framework's ledger, a discrete record of recognition events, this continuity bridge is a load-bearing step. The framework models recognition costs as functions on positive reals, and its central uniqueness theorem, law_of_logic_forces_jcost, derives the cost function J(x) = (x + 1/x)/2 - 1 from five conditions. One of those conditions is continuity, and the dAlembert_continuous_of_log_curvature theorem supplies that continuity from the more primitive log-curvature condition. It is a lemma in the proof chain, not the main result itself.

What the theorem does not claim is equally precise. It does not identify the value of κ; any finite κ works for the continuity conclusion. It does not assert that H equals cosh, because continuity alone does not select the solution. The stronger conclusion, that H(t) = cosh(t), requires the additional assumption that the second derivative at zero equals 1, as in the companion theorem dAlembert_cosh_solution_of_log_curvature. The continuity bridge is necessary but not sufficient for the full classification.

The practical consequence is that a single local measurement of curvature at one point, the origin, controls the behavior of the entire function. This is what makes the framework's cost uniqueness tractable: instead of checking regularity everywhere, one checks a local condition and the algebraic equation does the rest. The theorem turns a potentially unruly family of solutions into a well-behaved one, ready for the next step in the forcing chain.

THEOREM dAlembert_continuous_of_log_curvature · IndisputableMonolith/Cost/FunctionalEquation.lean
dAlembert_continuous_of_log_curvature · IndisputableMonolith/Cost/FunctionalEquation.lean:224 
theorem dAlembert_continuous_of_log_curvature
  (H : ℝ → ℝ)
  (h_one : H 0 = 1)
  (h_dAlembert : ∀ t u, H (t+u) + H (t-u) = 2 * H t * H u)
  {κ : ℝ} (h_calib : HasLogCurvature H κ) :
  Continuous H := by
  refine continuous_iff_continuousAt.2 ?_
  intro t
  have h_lim_H : Filter.Tendsto H (nhds 0) (nhds 1) :=
    tendsto_H_one_of_log_curvature H h_one h_calib
  have h_sum :
      Filter.Tendsto (fun u => H (t+u) + H (t-u)) (nhds 0) (nhds (2 * H t)) := by
    have h_prod : Filter.Tendsto (fun u => (2 * H t) * H u) (nhds 0)
        (nhds ((2 * H t) * (1 : ℝ))) := (tendsto_const_nhds.mul h_lim_H)
    have h_prod' : Filter.Tendsto (fun u => 2 * H t * H u) (nhds 0) (nhds (2 * H t)) := by
      simpa [mul_assoc] using h_prod
    have h_eq : (fun u => H (t+u) + H (t-u)) = fun u => 2 * H t * H u := by
      funext u
      exact h_dAlembert t u
    simpa [h_eq] using h_prod'
  have h_diff_sq :
      Filter.Tendsto (fun u => (H (t+u) - H (t-u))^2) (nhds 0) (nhds (0 : ℝ)) := by
    have h_u_sq : Filter.Tendsto (fun u => (H u)^2) (nhds 0) (nhds ((1 : ℝ)^2)) := by
      simpa [pow_two] using h_lim_H.mul h_lim_H
    have h_u_sq_sub : Filter.Tendsto (fun u => (H u)^2 - 1) (nhds 0) (nhds (0 : ℝ)) := by
      have h_const : Filter.Tendsto (fun _ : ℝ => (1 : ℝ)) (nhds 0) (nhds (1 : ℝ)) :=
        tendsto_const_nhds
      simpa using h_u_sq.sub h_const
    have h_const :
        Filter.Tendsto (fun _ : ℝ => 4 * ((H t)^2 - 1)) (nhds 0)
          (nhds (4 * ((H t)^2 - 1))) := tendsto_const_nhds
    have h_mul :
        Filter.Tendsto (fun u => (4 * ((H t)^2 - 1)) * ((H u)^2 - 1)) (nhds 0)
          (nhds (4 * ((H t)^2 - 1) * (0 : ℝ))) := h_const.mul h_u_sq_sub
    have h_eq :
        (fun u => (H (t+u) - H (t-u))^2) =
          (fun u => 4 * ((H t)^2 - 1) * ((H u)^2 - 1)) := by
      funext u
      exact dAlembert_diff_square H h_one h_dAlembert t u
    simpa [h_eq] using h_mul
  have h_abs :
      Filter.Tendsto (fun u => |H (t+u) - H (t-u)|) (nhds 0) (nhds (0 : ℝ)) := by
    have h_sqrt :
        Filter.Tendsto (fun u => Real.sqrt ((H (t+u) - H (t-u))^2)) (nhds 0)
          (nhds (Real.sqrt 0)) :=
      (Real.continuous_sqrt.tendsto 0).comp h_diff_sq
    simpa [Real.sqrt_sq_eq_abs] using h_sqrt
  have h_diff :
      Filter.Tendsto (fun u => H (t+u) - H (t-u)) (nhds 0) (nhds (0 : ℝ)) :=
    (tendsto_zero_iff_abs_tendsto_zero (f := fun u => H (t+u) - H (t-u))).2 h_abs
  have h_sum_diff :
      Filter.Tendsto
        (fun u => (H (t+u) + H (t-u)) + (H (t+u) - H (t-u)))
        (nhds 0) (nhds ((2 * H t) + (0 : ℝ))) := h_sum.add h_diff
  have h_twice : Filter.Tendsto (fun u => 2 * H (t+u)) (nhds 0) (nhds (2 * H t)) := by
    have h_sum_diff' :
        Filter.Tendsto
          (fun u => H (t+u) + H (t+u))
          (nhds 0) (nhds (2 * H t)) := by
      have h_eq :
          (fun u => (H (t+u) + H (t-u)) + (H (t+u) - H (t-u))) =
            (fun u => H (t+u) + H (t+u)) := by
        funext u
        ring
      have h_sum_diff'' :
          Filter.Tendsto
            (fun u => (H (t+u) + H (t-u)) + (H (t+u) - H (t-u)))
            (nhds 0) (nhds (2 * H t)) := by
        simpa using h_sum_diff
      simpa [h_eq] using h_sum_diff''
    simpa [two_mul] using h_sum_diff'
  have h_half :
      Filter.Tendsto (fun u => (2 * H (t+u)) / 2) (nhds 0) (nhds ((2 * H t) / 2)) := by
    have h_const : Filter.Tendsto (fun _ : ℝ => (1 / 2 : ℝ)) (nhds 0) (nhds (1 / 2 : ℝ)) :=
      tendsto_const_nhds
    simpa [div_eq_mul_inv] using h_twice.mul h_const
  have h_at0 : Filter.Tendsto (fun u => H (t+u)) (nhds 0) (nhds (H t)) := by
    simpa using h_half
  have h_map :
      Filter.Tendsto H (Filter.map (fun u => t + u) (nhds 0)) (nhds (H t)) :=
    (Filter.tendsto_map'_iff).2 h_at0
  have h_tendsto : Filter.Tendsto H (nhds t) (nhds (H t)) := by
    simpa [map_add_left_nhds_zero] using h_map
  exact h_tendsto
MODEL HasLogCurvature · IndisputableMonolith/Cost/FunctionalEquation.lean
HasLogCurvature · IndisputableMonolith/Cost/FunctionalEquation.lean:156 
/-- The paper's log curvature `κ(F) = lim_{t→0} 2 F(e^t)/t²`, stated on the
**punctured** filter.

The puncture is not cosmetic. On the full filter `nhds 0` this predicate is
unsatisfiable for every nonzero `κ`: Lean's division is total with `x / 0 = 0`,
so the quotient takes the value `0` at `t = 0`, and convergence along a filter
that contains the point pins the value at the point. The repo carried the
full-filter reading until 2026-07-25, which silently made two results vacuous;
`hasLogCurvature_full_filter_forces_zero` keeps that from recurring quietly. -/
def HasLogCurvature (H : ℝ → ℝ) (κ : ℝ) : Prop :=
  Filter.Tendsto (fun t => 2 * (H t - 1) / t^2)
    (nhdsWithin (0 : ℝ) ({(0 : ℝ)}ᶜ)) (nhds κ)
THEOREM dAlembert_continuous_of_log_curvature · IndisputableMonolith/Cost/FunctionalEquation.lean
dAlembert_continuous_of_log_curvature · IndisputableMonolith/Cost/FunctionalEquation.lean:224 
theorem dAlembert_continuous_of_log_curvature
  (H : ℝ → ℝ)
  (h_one : H 0 = 1)
  (h_dAlembert : ∀ t u, H (t+u) + H (t-u) = 2 * H t * H u)
  {κ : ℝ} (h_calib : HasLogCurvature H κ) :
  Continuous H := by
  refine continuous_iff_continuousAt.2 ?_
  intro t
  have h_lim_H : Filter.Tendsto H (nhds 0) (nhds 1) :=
    tendsto_H_one_of_log_curvature H h_one h_calib
  have h_sum :
      Filter.Tendsto (fun u => H (t+u) + H (t-u)) (nhds 0) (nhds (2 * H t)) := by
    have h_prod : Filter.Tendsto (fun u => (2 * H t) * H u) (nhds 0)
        (nhds ((2 * H t) * (1 : ℝ))) := (tendsto_const_nhds.mul h_lim_H)
    have h_prod' : Filter.Tendsto (fun u => 2 * H t * H u) (nhds 0) (nhds (2 * H t)) := by
      simpa [mul_assoc] using h_prod
    have h_eq : (fun u => H (t+u) + H (t-u)) = fun u => 2 * H t * H u := by
      funext u
      exact h_dAlembert t u
    simpa [h_eq] using h_prod'
  have h_diff_sq :
      Filter.Tendsto (fun u => (H (t+u) - H (t-u))^2) (nhds 0) (nhds (0 : ℝ)) := by
    have h_u_sq : Filter.Tendsto (fun u => (H u)^2) (nhds 0) (nhds ((1 : ℝ)^2)) := by
      simpa [pow_two] using h_lim_H.mul h_lim_H
    have h_u_sq_sub : Filter.Tendsto (fun u => (H u)^2 - 1) (nhds 0) (nhds (0 : ℝ)) := by
      have h_const : Filter.Tendsto (fun _ : ℝ => (1 : ℝ)) (nhds 0) (nhds (1 : ℝ)) :=
        tendsto_const_nhds
      simpa using h_u_sq.sub h_const
    have h_const :
        Filter.Tendsto (fun _ : ℝ => 4 * ((H t)^2 - 1)) (nhds 0)
          (nhds (4 * ((H t)^2 - 1))) := tendsto_const_nhds
    have h_mul :
        Filter.Tendsto (fun u => (4 * ((H t)^2 - 1)) * ((H u)^2 - 1)) (nhds 0)
          (nhds (4 * ((H t)^2 - 1) * (0 : ℝ))) := h_const.mul h_u_sq_sub
    have h_eq :
        (fun u => (H (t+u) - H (t-u))^2) =
          (fun u => 4 * ((H t)^2 - 1) * ((H u)^2 - 1)) := by
      funext u
      exact dAlembert_diff_square H h_one h_dAlembert t u
    simpa [h_eq] using h_mul
  have h_abs :
      Filter.Tendsto (fun u => |H (t+u) - H (t-u)|) (nhds 0) (nhds (0 : ℝ)) := by
    have h_sqrt :
        Filter.Tendsto (fun u => Real.sqrt ((H (t+u) - H (t-u))^2)) (nhds 0)
          (nhds (Real.sqrt 0)) :=
      (Real.continuous_sqrt.tendsto 0).comp h_diff_sq
    simpa [Real.sqrt_sq_eq_abs] using h_sqrt
  have h_diff :
      Filter.Tendsto (fun u => H (t+u) - H (t-u)) (nhds 0) (nhds (0 : ℝ)) :=
    (tendsto_zero_iff_abs_tendsto_zero (f := fun u => H (t+u) - H (t-u))).2 h_abs
  have h_sum_diff :
      Filter.Tendsto
        (fun u => (H (t+u) + H (t-u)) + (H (t+u) - H (t-u)))
        (nhds 0) (nhds ((2 * H t) + (0 : ℝ))) := h_sum.add h_diff
  have h_twice : Filter.Tendsto (fun u => 2 * H (t+u)) (nhds 0) (nhds (2 * H t)) := by
    have h_sum_diff' :
        Filter.Tendsto
          (fun u => H (t+u) + H (t+u))
          (nhds 0) (nhds (2 * H t)) := by
      have h_eq :
          (fun u => (H (t+u) + H (t-u)) + (H (t+u) - H (t-u))) =
            (fun u => H (t+u) + H (t+u)) := by
        funext u
        ring
      have h_sum_diff'' :
          Filter.Tendsto
            (fun u => (H (t+u) + H (t-u)) + (H (t+u) - H (t-u)))
            (nhds 0) (nhds (2 * H t)) := by
        simpa using h_sum_diff
      simpa [h_eq] using h_sum_diff''
    simpa [two_mul] using h_sum_diff'
  have h_half :
      Filter.Tendsto (fun u => (2 * H (t+u)) / 2) (nhds 0) (nhds ((2 * H t) / 2)) := by
    have h_const : Filter.Tendsto (fun _ : ℝ => (1 / 2 : ℝ)) (nhds 0) (nhds (1 / 2 : ℝ)) :=
      tendsto_const_nhds
    simpa [div_eq_mul_inv] using h_twice.mul h_const
  have h_at0 : Filter.Tendsto (fun u => H (t+u)) (nhds 0) (nhds (H t)) := by
    simpa using h_half
  have h_map :
      Filter.Tendsto H (Filter.map (fun u => t + u) (nhds 0)) (nhds (H t)) :=
    (Filter.tendsto_map'_iff).2 h_at0
  have h_tendsto : Filter.Tendsto H (nhds t) (nhds (H t)) := by
    simpa [map_add_left_nhds_zero] using h_map
  exact h_tendsto

What this page does not claim

The theorem does not prove that the cost function J is the only solution to the full five-condition system. The theorem does not identify the numerical value of the log-curvature κ. The theorem does not establish that H equals cosh without the additional second-derivative condition.

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