Cost Ndim Hessian Quadratic Hessian

The quadratic form

The quadratic form is a standard tool in calculus and optimization. Given a smooth function of several variables, its Hessian matrix collects all the second partial derivatives. Feeding a direction vector into the Hessian produces a single number, the quadratic form, which describes how sharply the function curves when you move in that direction. A positive value means the function bends upward; a negative value means it bends downward.

In the Recognition Science framework, the n-dimensional cost function is studied in log-coordinates, where it takes a weighted aggregate of the coordinates as its only input. The framework's machine-checked library of formal theorems defines the Hessian matrix for this cost and proves a striking simplification: the quadratic form equals the hyperbolic cosine of the weighted aggregate times the square of the dot product between the weight vector and the direction vector. In symbols, Q(v) = cosh(α · t) (α · v)². The entire curvature of the cost in any direction is controlled by the single number α · v.

This structure has direct consequences. The theorem quadraticHessian_nonneg proves the quadratic form is always nonnegative, so the cost function is convex in log-coordinates. The theorem applyHessian_of_dot_zero shows that any direction orthogonal to the weight vector lies in the kernel of the Hessian, meaning the cost is flat along those directions. The Hessian has rank one: it factors through the outer product α ⊗ α, so all curvature is concentrated along the single direction set by the weights.

What the declaration does not claim is equally important. It does not assert that the cost function itself is uniquely determined by this Hessian structure, nor does it connect the quadratic form to any physical measurement or empirical value. The declarations define the Hessian and prove algebraic identities about it; they do not derive the weight vector α from first principles or show that this convexity property forces the golden ratio or any other constant. The quadratic form is a mathematical object within the framework, not a statement about the world.

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

/-- 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 declarations do not derive the weight vector α from first principles. The quadratic form does not connect to any empirical measurement or physical constant. The convexity result does not by itself force the golden ratio or any other framework constant.

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: