Cost Ndim Hessian Hessian At Factor

The Hessian factor

The Hessian is the matrix of second derivatives of a function, the object that measures how the slope changes as you move. For the n-dimensional reciprocal cost function used in Recognition Science, the Hessian has a simple structure. The declaration hessianAt_factor proves that the Hessian at any point is exactly the Hessian at the equilibrium point, multiplied by a single scalar factor. That factor is the hyperbolic cosine of the weighted aggregate of the coordinates, which is a positive number that depends only on how far the system is from its balanced state.

This factorization means the curvature of the cost function does not change shape as the system moves; it only scales uniformly. The direction of steepest curvature, encoded by the outer product of the weight vector with itself, remains fixed. The scalar factor grows as the system moves away from equilibrium, so the cost function becomes more curved, but it always curves in the same pattern. This is a theorem proved in the machine-checked library of formal theorems, not a numerical observation.

In Recognition Science, the cost is a measure of how much it costs to recognize one state given another, and the equilibrium point is where the cost is zero. The theorem shows that the local geometry of the cost function is controlled by one single active direction. Vectors orthogonal to the weight vector lie in the kernel of the Hessian, meaning they feel no curvature at all. The quadratic form, which gives the second-order change in cost along a direction, depends only on the component of that direction along the weight vector.

The theorem does not claim that the cost function itself is quadratic. The Hessian factorization holds at every point, but the function is not a quadratic form globally. It also does not claim any physical meaning for the weight vector or the coordinates; these are definitional choices within the framework. The factorization is a mathematical property of the cost function, not a statement about the physical world.

/-- The full Hessian is a scalar multiple of the equilibrium outer-product model. -/
theorem hessianAt_factor {n : ℕ} (α t : Vec n) :
    hessianAt α t = fun i j => Real.cosh (dot α t) * hessianMatrix α i j := by
  funext i j
  unfold hessianAt hessianEntry hessianMatrix
  ring

/-- Vectors orthogonal to `α` lie in the kernel of the Hessian. -/
theorem applyHessian_of_dot_zero {n : ℕ} (α t v : Vec n)
    (hv : dot α v = 0) :
    applyHessian α t v = 0 := by
  funext i
  simp [applyHessian_eq_direction, hv]

/-- The Hessian quadratic form depends only on the single active direction `dot α v`. -/
theorem quadraticHessian_eq {n : ℕ} (α t v : Vec n) :
    quadraticHessian α t v = Real.cosh (dot α t) * (dot α v) ^ 2 := by
  unfold quadraticHessian dot
  rw [applyHessian_eq_direction]
  calc
    ∑ i : Fin n, v i * (Real.cosh (dot α t) * α i * dot α v)
        = ∑ i : Fin n, Real.cosh (dot α t) * dot α v * (v i * α i) := by
            apply Finset.sum_congr rfl
            intro i hi
            ring
    _ = (Real.cosh (dot α t) * dot α v) * ∑ i : Fin n, v i * α i := by
          rw [Finset.mul_sum]
    _ = Real.cosh (dot α t) * (dot α v) * dot α v := by
          congr 1
          unfold dot
          apply Finset.sum_congr rfl
          intro i hi
          ring
    _ = Real.cosh (dot α t) * (dot α v) ^ 2 := by
          ring

What this page does not claim

The cost function is not globally quadratic, only its local second-order behavior factors this way. The theorem assigns no physical meaning to the weight vector or the coordinates. The scalar factor is always positive, but the theorem does not claim the cost function is convex everywhere.

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/Ndim/Hessian.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: