Cost Ndim Hessian Quadratic Hessian Eq

The single active direction

The second derivative of a cost function, its Hessian, usually contains a matrix of many numbers, one for each pair of directions. The declaration quadraticHesian_eq shows that for the n-dimensional reciprocal cost used in Recognition Science, this matrix is far simpler. In log-coordinates, the Hessian at any point is a scalar multiple of the outer product α ⊗ α, where α is a fixed vector of weights. The scalar factor is the hyperbolic cosine of the dot product α · t, with t the log-coordinate state.

The practical consequence is that the Hessian has rank one. It acts on any vector v by first projecting v onto the direction α, then scaling the result. The quadratic form, which measures the second-order change in cost along a direction, therefore depends only on the single number α · v. The theorem states this explicitly: quadraticHessian α t v equals cosh(α · t) times the square of (α · v). This means the curvature of the cost surface is completely described by one active direction, the vector α, and all orthogonal directions are flat.

In Recognition Science, this structure is not an accident but a consequence of the framework's definition of cost. The framework models recognition as a ledger, a discrete record of events, and the cost of recognition is forced by five plain conditions. The n-dimensional cost function extends this to multiple simultaneous recognitions, and the Hessian result shows that the curvature of this extended cost inherits the same one-dimensional character. The theorem is proved in the machine-checked library of formal theorems, with no unverified assumptions beyond the standard axioms of the underlying type theory.

What the theorem does not claim is that the vector α is unique or that the cost function itself is uniquely determined by this Hessian property. The Hessian result is a property of a chosen cost function, not a derivation of that function. The framework's uniqueness theorem for the one-dimensional cost J(x) = (x + 1/x)/2 − 1 is separate, and the n-dimensional extension is a definitional choice, not a forced consequence. The theorem also says nothing about the physical meaning of α; it is an input to the model, not an output.

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

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

What this page does not claim

The vector α is unique or derived from the framework. The n-dimensional cost function itself is uniquely forced by the Hessian property. The theorem assigns a physical meaning to the weight vector α.

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: