Explanation of HasLogCurvature in IndisputableMonolith.Cost.FunctionalEquation

(1) Plain English

The declaration defines a predicate HasLogCurvature H κ that holds when the function H : ℝ → ℝ has quadratic behavior near zero with curvature coefficient κ. Specifically, as the input t approaches 0, the expression 2 * (H(t) - 1) / t² approaches the limit κ. This encodes a second-order Taylor-like condition in log-reparametrized coordinates.

(2) Why it matters in Recognition Science

It supplies the calibration condition used to bootstrap continuity and smoothness for solutions of the d'Alembert functional equation that arises in the uniqueness proof for the reciprocal-symmetric cost function J (the T5 step of the forcing chain). The predicate lets the framework derive that continuous solutions satisfying the cost equation are differentiable, which is required for the uniqueness theorem.

(3) How to read the formal statement

def HasLogCurvature (H : ℝ → ℝ) (κ : ℝ) : Prop :=
  Filter.Tendsto (fun t => 2 * (H t - 1) / t^2) (nhds 0) (nhds κ)

• def introduces a named proposition.
• Parameters are a function H and real κ.
• The body is a Filter.Tendsto statement: the map t ↦ 2*(H t - 1)/t² converges to κ in the neighborhood filter nhds 0.
• nhds is the standard neighborhood filter from Mathlib.

(4) Visible dependencies or certificates in the supplied source

The definition is used directly by tendsto_H_one_of_log_curvature (which shows the limit implies H approaches 1 at 0) and dAlembert_continuous_of_log_curvature (which upgrades the d'Alembert equation plus this curvature condition to continuity of H). No external certificates beyond Mathlib Filter and nhds are required inside the module.

(5) What this declaration does not prove

It is only a definition; it does not assert that Jcost satisfies HasLogCurvature, does not prove uniqueness of the cost function, and does not connect to the broader forcing chain or physical constants. Those steps lie outside this single declaration.