Cost Ndim Hessian Gradient Entry

The gradient entry

The gradient entry is a number attached to one coordinate of a system that tracks the cost of recognition. In the framework, a ledger (a discrete record of events) assigns a cost to each state, and the gradient entry tells how that cost changes when one coordinate shifts while the others stay fixed. The declaration defines it, for a system with n coordinates, as the product of the coordinate's weight and the hyperbolic sine of a single aggregate value. That aggregate is the weighted sum of the coordinates, so the entire gradient depends on the system only through that one number.

The definition belongs to the n-dimensional reciprocal cost, which the framework derives from its five forced conditions. In log-coordinates, the cost depends only on the single weighted aggregate, not on each coordinate separately. The gradient entry is the coordinate of that dependence: it says that the cost's rate of change in the i-th direction is the weight times the hyperbolic sine of the aggregate. The declaration is a definition, not a theorem; it chooses the form, and the framework's library (a machine-checked collection of formal theorems) then proves properties about it.

The library proves that the Hessian, the matrix of second derivatives, is rank one and factors through the outer product of the weight vector with itself. At the equilibrium point where the aggregate is zero, the Hessian equals that outer product exactly. Away from equilibrium, the Hessian is the same matrix multiplied by the hyperbolic cosine of the aggregate. The quadratic form, which measures the cost's curvature in a direction, is always nonnegative. That means the cost is convex in the log-coordinates, so the equilibrium is a minimum, not a saddle or maximum.

The key consequence is that the Hessian has a single active direction. Vectors orthogonal to the weight vector lie in the kernel: moving in those directions costs nothing to second order. The cost's curvature is entirely along the weight direction, so the system's response to small perturbations is one-dimensional. This is what the declaration establishes: a precise, machine-checked statement that the n-dimensional cost has a one-dimensional curvature structure, with the gradient entry as its coordinate.

/-- Log-coordinate gradient entry for `JlogN`. -/
noncomputable def gradientEntry {n : ℕ} (α t : Vec n) (i : Fin n) : ℝ :=
  α i * Real.sinh (dot α t)

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

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

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

What this page does not claim

The gradient entry does not define the cost function itself; it only gives a coordinate of its gradient. The Hessian theorems do not claim that the cost is globally convex, only that its quadratic form is nonnegative at every point. The declaration does not establish the n-dimensional cost as the unique cost; that uniqueness is a separate theorem.

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: