Foundation Jcost Hessian C7 Jcost Taylor Quadratic Coefficient

The quadratic coefficient

The cost function J(x) = (x + 1/x)/2 - 1 measures the forced price of a recognition event in the Recognition Science framework. At its equilibrium point x = 1, the cost is zero. The question is how the cost behaves when the input moves slightly away from that balance. The framework's machine-checked library of formal theorems proves an exact local algebraic kernel: for any small offset eps, J(1 + eps) = eps^2 / (2(1 + eps)). This is not an approximation. It is an exact identity that holds for every real eps except -1, where the expression is undefined.

Near equilibrium, this exact form behaves like a quadratic: the leading term is eps^2 / 2. The declaration jcostTaylorQuadraticCoefficient records that coefficient as the number 1/2. In the standard Taylor convention, the Hessian coefficient is twice the quadratic coefficient, so the framework also defines jcostHessianCoefficient = 2 * (1/2) = 1. Both values are proved by reflexivity: the definitions literally reduce to the numbers 1/2 and 1. The structure JCostHessianCert bundles these three facts, the local kernel, the half coefficient, and the unit Hessian, into a single certificate that the library can reference as one unit.

What this does not claim is broader than what it does. The exact identity holds at the single point x = 1, not globally. It says nothing about the cost function's behavior far from equilibrium, where the full formula J(x) = (x + 1/x)/2 - 1 governs. The result is purely local. It also does not assert that the cost function is differentiable in the analytic sense; the library proves the algebraic identity directly, without invoking a derivative API. The coefficient 1/2 is a formal definitional fact, not a measured quantity. Nothing here connects the Hessian coefficient to any physical constant or to the golden ratio phi, which appears elsewhere in the framework's forcing chain. The declaration is a small, sharp local fact, and it stays that way.

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 jcostTaylorQuadraticCoefficient_eq :
    jcostTaylorQuadraticCoefficient = 1 / 2 := rfl

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

What this page does not claim

The identity holds only at x = 1, not globally. The coefficient 1/2 is a definitional fact, not a measured value. No connection is made to phi or any physical constant in this declaration.

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: