Cost Ndim Hessian Apply Hessian Of Dot Zero

The flat directions

In calculus, the Hessian matrix of a function records its local curvature: how the slope changes when you nudge the input in each direction. For a function of many variables, the Hessian is an n by n matrix, and applying it to a vector tells you how the curvature responds to a change along that vector. The declaration applyHessian_of_dot_zero is a theorem about this matrix for a specific family of cost functions, the n-dimensional reciprocal cost used in Recognition Science.

That cost function is built from a weighted aggregate of its inputs, a single number called the ledger entry, a discrete record of events. In log-coordinates, the cost depends only on this one aggregate, not on the individual inputs separately. The theorem states a simple geometric consequence: if a vector v is orthogonal to the weight vector α, meaning their dot product is zero, then the Hessian applied to v is exactly the zero vector. In plain terms, curvature along any direction perpendicular to α does not exist; that direction is flat.

This is a rank-one structure. The Hessian matrix is a scalar multiple of the outer product α ⊗ α, which means it has only one active direction, the direction of α itself. All other directions lie in its kernel. The theorem applyHessian_of_dot_zero is the precise statement of that kernel: the null space is the orthogonal complement of α. It is a proved theorem in the framework's machine-checked library of formal theorems, and it holds for any dimension n.

The theorem does not claim that the cost function itself is flat along those directions, only that its second derivative is. The first derivative, the gradient, can still be nonzero. It also does not claim that the Hessian is zero everywhere; at a general point it is a positive scalar multiple of α ⊗ α, with the scalar depending on the aggregate. The flatness is a property of the curvature alone, and it is exact only for vectors orthogonal to α.

What this fact changes is the picture of the cost surface. Instead of an n-dimensional bowl with curvature in every direction, the model has a single curved ridge along α and complete flatness in every perpendicular direction. That structure is what makes the n-dimensional cost tractable: all of its local geometry is described by one direction and one scalar.

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

What this page does not claim

The theorem does not claim the gradient is zero along directions orthogonal to α. The theorem does not claim the Hessian is zero everywhere, only at points where the aggregate dot α t is zero. The theorem does not claim the cost function is flat along those directions, only that its second derivative is.

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: