metric_at_equilibrium_eq_hessian
plain-language theorem explainer
The theorem shows that the metric entry function, evaluated at the zero vector in log coordinates, equals the outer-product Hessian matrix built from α. Researchers modeling the cost metric for JlogN aggregates in Recognition Science cite this to anchor the equilibrium case. The proof applies functional extensionality on the matrix indices followed by direct simplification against the Hessian definition.
Claim. For any natural number $n$ and vector $α ∈ ℝ^n$, the metric entry function evaluated at the zero displacement equals the Hessian matrix: $g(α, 0) = H(α)$, where $H_{ij}(α) = α_i α_j$.
background
The module treats the cost metric in log coordinates. Vectors are coordinate functions from Fin n to reals. The Hessian matrix is defined as the outer product α ⊗ α. The metric entry is the Hessian-derived entry for the JlogN aggregate, obtained by specializing the general Hessian entry function at a displacement vector t.
proof idea
One-line wrapper that applies functional extensionality to the matrix indices i and j, then simplifies using the definition of hessianMatrix.
why it matters
This identity supplies the equilibrium base case for the cost metric in log coordinates. It confirms that the metric reduces exactly to the outer-product Hessian model when the displacement vanishes, supporting downstream derivations that rely on the J-cost function and the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.