metricEntry
plain-language theorem explainer
The metric entry in log coordinates for the JlogN cost equals the Hessian entry at the same indices. Researchers assembling the N-dimensional cost metric tensor in Recognition Science cite this when building equilibrium models from Hessian data. The definition is a one-line wrapper delegating directly to the Hessian computation.
Claim. For vectors $α, t ∈ ℝ^n$ and indices $i, j ∈ {1,…,n}$, the metric entry $m_{ij}(α, t)$ is defined to equal the Hessian entry $h_{ij}(α, t)$.
background
The Cost.Ndim.Metric module constructs the cost metric in log coordinates. Vec n is the type of n-component real vectors, realized as functions Fin n → ℝ. The upstream hessianEntry supplies the log-coordinate Hessian for JlogN via the formula α_i α_j cosh(dot α t). The module doc states the local setting as the cost metric in log coordinates.
proof idea
This is a one-line wrapper that applies the definition of hessianEntry.
why it matters
The definition supplies the entries used by metric_at_equilibrium_eq_hessian, which proves coincidence with the outer-product Hessian model at equilibrium, and by metricEntry_zero, which evaluates the entry at zero displacement. It fills the step that converts the Hessian into metric entries for the Recognition cost framework in log coordinates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.