Cost Ndim Xcoordinates X Hessian Matrix2 Eq General

The two-component Hessian identity

In the Recognition Science framework, the cost (a penalty assigned to each possible state of a system) is not a free choice. A proved theorem forces it to have the form J(x) = (x + 1/x)/2 - 1. When several components interact, the framework builds a multi-component cost, and the curvature of that cost surface is recorded in a matrix called the Hessian. The declaration xHessianMatrix2_eq_general is a formal identity: it states that the Hessian computed by the general entry formula equals the Hessian obtained by writing out the 2 by 2 case directly.

The identity matters because it closes a gap between two ways of writing the same object. The general formula defines each entry of the Hessian using the aggregate R = a/x + b/y, a positive weighted sum of the coordinates. The 2 by 2 version specializes that formula to two components, with explicit entries such as (a/(2x²))((a-1)R + (a+1)/R) on the diagonal and (ab/(2xy))(R + 1/R) off the diagonal. The theorem xHessianMatrix2_eq_general proves, with a machine-checked argument, that these two descriptions agree for every choice of positive weights a, b and coordinates x, y.

What the declaration does not claim is just as important. It does not assert that the Hessian is nondegenerate, nor that it has any particular rank. Those properties are separate theorems in the same module, and they require extra conditions: the determinant formula shows the Hessian becomes degenerate exactly when R = 1 (the neutral locus) or when a certain secondary factor vanishes. The identity itself is purely algebraic, a statement about equality of matrix entries, not about the geometry of the cost surface.

In the broader framework, this identity is a technical bridge. It lets later results, such as the determinant factorization and the degeneracy criterion, be stated cleanly in the 2 by 2 case. The payoff for a reader is a precise sense of how the general curvature formula behaves when reduced to two components, and a clear boundary between what the identity establishes and what requires further hypotheses.

theorem xHessianMatrix2_eq_general (a b x y : ℝ) :
    xHessianMatrix2 a b x y
      = fun i j => xHessianEntry (vec2 a b) (vec2 x y) i j := by
  ext i j
  fin_cases i <;> fin_cases j <;>
    simp [xHessianMatrix2, xHessianMatrix2OfR, xHessianEntry,
      xDirection, xDiagonalCorrection, vec2]
  all_goals ring

/-- The `x`-coordinate Hessian entry of `JcostN`. -/
noncomputable def xHessianEntry {n : ℕ} (α x : Vec n) (i j : Fin n) : ℝ :=
  ((aggregate α x + (aggregate α x)⁻¹) / 2) * xDirection α x i * xDirection α x j
    - ((aggregate α x - (aggregate α x)⁻¹) / 2) * xDiagonalCorrection α x i j

What this page does not claim

The identity does not prove the Hessian is nondegenerate or has any particular rank. The identity does not establish the behavior of the Hessian away from the 2 by 2 case.

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/XCoordinates.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: