Cost Ndim Hessian

The shape of the cost surface

The cost of recognition, the price reality pays to record an event, is a function of how far a state has moved from its equilibrium. In the framework's native coordinates, this cost has a second derivative, a Hessian, that describes how sharply the cost surface curves. The module cost-ndim-hessian proves that in any number of dimensions, this curvature is simple: it has rank one, meaning it is active along a single direction and flat along every other.

To see why, consider the framework's cost function in log-coordinates, where the state is a vector t and the weights are a vector α. The cost depends on t only through the single weighted aggregate dot α t, the sum of α_i times t_i. Because of this, the Hessian matrix factors as the outer product α ⊗ α, scaled by a positive factor that depends on the state. At equilibrium, where t is zero, the scaling factor is exactly 1, so the Hessian is precisely α ⊗ α.

This structure has a concrete consequence: the Hessian's action on any vector v is always parallel to α, and the quadratic form it defines, the curvature along v, is proportional to (dot α v)². Vectors orthogonal to α lie in the kernel of the Hessian, meaning the cost surface is completely flat along those directions. The framework's library proves these facts formally: hessianAt_factor, applyHessian_eq_direction, applyHessian_of_dot_zero, and quadraticHessian_eq are all theorems in the machine-checked collection.

In Recognition Science, this result matters because it constrains how the framework can extend to many dimensions. The cost surface has a single active direction, the one defined by the weight vector α, and all other directions are inert. This is not a choice but a forced consequence of the cost function's form. It means that any dynamics built on this cost will be driven along one line in the state space, with no curvature to guide motion elsewhere. The framework models this as the fundamental shape of its geometry, a fact that holds for any number of dimensions n.

What this establishes in plain language is that the framework's cost surface is one-dimensional in its curvature, no matter how many variables are involved. The practical upshot is that the framework's geometry is highly constrained: it has a single distinguished direction, and all other directions are flat. This is a structural fact about the framework, not an empirical observation, and it shapes what the framework can and cannot do as it scales to higher dimensions.

/-- 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

/-- The Hessian action is always parallel to `α`. -/
theorem applyHessian_eq_direction {n : ℕ} (α t v : Vec n) :
    applyHessian α t v = fun i => Real.cosh (dot α t) * α i * dot α v := by
  funext i
  unfold applyHessian applyTensor hessianAt hessianEntry dot
  calc
    ∑ j : Fin n, (α i * α j * Real.cosh (dot α t)) * v j
        = ∑ j : Fin n, (α i * Real.cosh (dot α t)) * (α j * v j) := by
            apply Finset.sum_congr rfl
            intro j hj
            ring
    _ = (α i * Real.cosh (dot α t)) * ∑ j : Fin n, α j * v j := by
          rw [Finset.mul_sum]
    _ = Real.cosh (dot α t) * α i * dot α v := by
          simp [dot, mul_comm, mul_assoc]

@[simp] theorem hessianAt_zero {n : ℕ} (α : Vec n) :
    hessianAt α (fun _ => 0) = hessianMatrix α := by
  funext i j
  simp [hessianAt, hessianMatrix, hessianEntry_zero]

/-- The Hessian action is always parallel to `α`. -/
theorem applyHessian_eq_direction {n : ℕ} (α t v : Vec n) :
    applyHessian α t v = fun i => Real.cosh (dot α t) * α i * dot α v := by
  funext i
  unfold applyHessian applyTensor hessianAt hessianEntry dot
  calc
    ∑ j : Fin n, (α i * α j * Real.cosh (dot α t)) * v j
        = ∑ j : Fin n, (α i * Real.cosh (dot α t)) * (α j * v j) := by
            apply Finset.sum_congr rfl
            intro j hj
            ring
    _ = (α i * Real.cosh (dot α t)) * ∑ j : Fin n, α j * v j := by
          rw [Finset.mul_sum]
    _ = Real.cosh (dot α t) * α i * dot α v := by
          simp [dot, mul_comm, mul_assoc]

/-- 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

theorem quadraticHessian_nonneg {n : ℕ} (α t v : Vec n) :
    0 ≤ quadraticHessian α t v := by
  rw [quadraticHessian_eq]
  positivity

What this page does not claim

This module does not derive the cost function itself, only its Hessian structure. The rank-one property does not imply the cost surface is flat overall; it is curved along one direction. No claim is made here about how this Hessian structure relates to physical measurements.

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: