Cost Ndim Xcoordinates X Hessian Entry Diag

The diagonal entry

A Hessian matrix collects the second derivatives of a function, and its diagonal entries measure how the function bends along each coordinate axis. In the Recognition Science framework, the cost function J measures the price of a recognition event, and its x-coordinate Hessian describes how that price curves as the inputs move. The declaration xHessianEntry_diag establishes a compact algebraic formula for the diagonal entries of this Hessian, written in terms of the positive aggregate R = aggregate α x and the coordinates x_i.

The formula itself is a direct consequence of the definitions. For a diagonal entry i = j, the theorem states that the entry equals (α_i / (2 * x_i²)) * (((α_i - 1) * R) + ((α_i + 1) * R⁻¹)). This expression combines the coordinate value x_i, the weight α_i, and the aggregate R into a single closed form. The proof unfolds the definitions of the Hessian entry, the direction vector, and the diagonal correction term, then simplifies with ring arithmetic.

What the formula reveals is a precise condition for the diagonal entry to vanish. If the weight α_i equals 1, the first factor (α_i - 1) becomes zero, and the whole entry collapses to zero regardless of the aggregate R. This matches the zero-cost degeneracy: when the aggregate equals 1, the Hessian collapses to a rank-one outer product, and the diagonal entries lose their independent curvature. Away from that neutral locus, the diagonal entry is generically nonzero, as the generic nondegeneracy criterion confirms for the 2 × 2 case.

The theorem does not claim that the diagonal entries are always positive, nor that the Hessian is positive definite. It only establishes the algebraic identity. The sign of the entry depends on the signs of α_i, x_i, and the aggregate R, and the framework does not impose positivity on the Hessian itself. The result is a computational tool: it gives an exact expression that can be evaluated, differentiated, or used in further proofs, but it carries no geometric or physical interpretation beyond the algebraic statement.

theorem xHessianEntry_diag {n : ℕ} (α x : Vec n) (i : Fin n) :
    xHessianEntry α x i i
      = (α i / (2 * (x i) ^ 2))
          * (((α i - 1) * aggregate α x) + ((α i + 1) * (aggregate α x)⁻¹)) := by
  unfold xHessianEntry xDirection xDiagonalCorrection
  simp
  ring

theorem xHessianEntry_diag {n : ℕ} (α x : Vec n) (i : Fin n) :
    xHessianEntry α x i i
      = (α i / (2 * (x i) ^ 2))
          * (((α i - 1) * aggregate α x) + ((α i + 1) * (aggregate α x)⁻¹)) := by
  unfold xHessianEntry xDirection xDiagonalCorrection
  simp
  ring

/-- Away from the neutral locus and the secondary discriminant factor, the
`2 × 2` `x`-coordinate Hessian is nondegenerate. -/
theorem det_xHessianMatrix2_ne_zero_of_generic (a b x y : ℝ)
    (hx : x ≠ 0) (hy : y ≠ 0)
    (ha : a ≠ 0) (hb : b ≠ 0)
    (hR1 : aggregate (vec2 a b) (vec2 x y) ≠ 1)
    (hdisc :
      (aggregate (vec2 a b) (vec2 x y)) ^ 2 * a
        + (aggregate (vec2 a b) (vec2 x y)) ^ 2 * b
        - (aggregate (vec2 a b) (vec2 x y)) ^ 2
        + a + b + 1 ≠ 0) :
    Matrix.det (xHessianMatrix2 a b x y) ≠ 0 := by
  let R := aggregate (vec2 a b) (vec2 x y)
  have hR : R ≠ 0 := (aggregate_pos (vec2 a b) (vec2 x y)).ne'
  have hRp1 : R + 1 ≠ 0 := by
    have hpos : 0 < R := by simp [R]
    linarith
  have hden : 4 * R ^ 2 * x ^ 2 * y ^ 2 ≠ 0 := by
    have hR2 : R ^ 2 ≠ 0 := pow_ne_zero 2 hR
    have hx2 : x ^ 2 ≠ 0 := pow_ne_zero 2 hx
    have hy2 : y ^ 2 ≠ 0 := pow_ne_zero 2 hy
    have h4R : 4 * R ^ 2 ≠ 0 := mul_ne_zero (by norm_num) hR2
    have h4Rx : 4 * R ^ 2 * x ^ 2 ≠ 0 := mul_ne_zero h4R hx2
    exact mul_ne_zero h4Rx hy2
  rw [det_xHessianMatrix2_formula a b x y hx hy]
  refine div_ne_zero ?_ hden
  refine neg_ne_zero.mpr ?_
  refine mul_ne_zero ?_ hdisc
  refine mul_ne_zero ?_ hRp1
  refine mul_ne_zero ?_ (sub_ne_zero.mpr hR1)
  exact mul_ne_zero ha hb

What this page does not claim

The diagonal entries are always positive or the Hessian is positive definite. The formula applies to coordinates that are not positive. The theorem provides a physical interpretation of the Hessian beyond its algebraic content.

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: