Foundation Jcost Hessian C7 Jcost Taylor Quadratic Coefficient Eq

The local cost expansion

The cost function in Recognition Science, a measure of the price of a recognition event, has a special point at the value 1, where the cost is zero. The declaration jcostTaylorQuadraticCoefficient_eq is a small but exact statement about what happens just next to that point. It says that the coefficient of the quadratic term in the local expansion of the cost is exactly 1/2. In the standard Taylor convention, where the Hessian is twice the quadratic coefficient, this means the Hessian coefficient is exactly 1.

The supporting theorem gives the full local picture. For any small displacement eps away from 1, the cost at 1 + eps is exactly eps^2 / (2 * (1 + eps)), provided eps is not -1. This is not an approximation; it is an algebraic identity. The numerator is purely quadratic, which is why the expansion is called quadratic. The denominator shows the cost is not symmetric around 1: moving down by eps costs more than moving up by the same amount, because the denominator shrinks.

This result is proved in the framework's machine-checked library of formal theorems. The declaration is a definition that names the coefficient 1/2, and the theorem states that this definition equals 1/2 by reflexivity. The supporting lemmas establish the local kernel and the Hessian certificate, all with zero axioms beyond the standard ones. The proof does not use calculus or derivatives; it works directly from the algebraic definition of the cost function.

In Recognition Science, this local expansion is the seed of a larger story. The exact quadratic coefficient at equilibrium is the first step toward understanding how small perturbations behave. The framework uses this to anchor the behavior of the cost near its minimum, which in turn supports the forcing chain that derives constants like the golden ratio and the number of spatial dimensions. The Hessian being exactly 1 is a clean, memorable fact that the rest of the framework builds on.

What this declaration does not claim is just as important. It does not claim that the cost function is globally quadratic; the exact formula shows the denominator depends on eps, so the cost is not a simple parabola. It does not claim anything about the second derivative in the usual calculus sense, because the proof avoids the derivative API entirely. It does not claim that the cost function is symmetric around 1, and the formula shows it is not. These limits are part of the honest statement of what the theorem establishes.

theorem jcostTaylorQuadraticCoefficient_eq :
    jcostTaylorQuadraticCoefficient = 1 / 2 := rfl

theorem jcost_one_plus_eq (eps : ℝ) (h : eps ≠ -1) :
    Jcost (1 + eps) = eps ^ 2 / (2 * (1 + eps)) := by
  have hx : 1 + eps ≠ 0 := by
    intro hz
    apply h
    linarith
  rw [Jcost_eq_sq hx]
  ring_nf

theorem jcostHessianCoefficient_eq_one :
    jcostHessianCoefficient = 1 := by
  unfold jcostHessianCoefficient jcostTaylorQuadraticCoefficient
  norm_num

What this page does not claim

The cost function is not globally quadratic; the denominator in the exact formula depends on the displacement. The theorem does not use or establish a second derivative in the calculus sense. The cost function is not symmetric around the equilibrium point.

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/JCostHessianC7.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: