Foundation Jcost Hessian C7 Jcost Local Quadratic Kernel

The local quadratic kernel

The recognition cost function J measures the price of a recognition event, a discrete record of something happening. It has a natural resting point at the value 1, where the cost is zero. The question is what happens when you nudge the input slightly away from 1, say to 1 + eps, where eps is a small number. The answer, proved as an exact algebraic identity, is that J(1 + eps) equals eps squared divided by 2 times (1 + eps).

This is stronger than a typical approximation. Many functions look quadratic near a minimum, but here the formula is exact for every eps except -1. The expression is not a truncated Taylor series; it is the true value of J at that point. Written another way, J(1 + eps) times 2(1 + eps) equals eps squared. That clean form is the local quadratic kernel, a precise statement about how the cost rises as you move away from equilibrium.

The theorem also records the Taylor coefficient. In the standard convention, the quadratic coefficient is 1/2, meaning the leading term is eps squared over 2. From that, the Hessian coefficient, which is twice the quadratic coefficient, comes out to exactly 1. These are not approximations or fitted numbers; they are forced by the definition of J itself.

In Recognition Science, this local behavior matters because it shows the cost function is not flat near its minimum. The curvature is fixed and positive, so small perturbations carry a definite, nonzero price. That fact anchors later results about stability and scaling, though this theorem alone does not establish those.

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

/-- The exact quadratic numerator in the local J-cost expansion. -/
theorem jcost_local_quadratic_kernel (eps : ℝ) (h : eps ≠ -1) :
    Jcost (1 + eps) * (2 * (1 + eps)) = eps ^ 2 := by
  rw [jcost_one_plus_eq eps h]
  have hx : 1 + eps ≠ 0 := by
    intro hz
    apply h
    linarith
  have hden : 2 * (1 + eps) ≠ 0 := by
    exact mul_ne_zero (by norm_num) hx
  field_simp [hden, hx]

theorem jcostTaylorQuadraticCoefficient_eq :
    jcostTaylorQuadraticCoefficient = 1 / 2 := rfl

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

What this page does not claim

This theorem does not prove the global uniqueness of J. It does not establish any property of J away from the point 1 + eps. It does not connect the Hessian coefficient to any empirical measurement.

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: