hessianEntry_zero
plain-language theorem explainer
The theorem establishes that the Hessian entry of the n-dimensional logarithmic cost at the zero vector equals the componentwise product α_i α_j. Analysts extending the Recognition cost to multiple dimensions cite this when confirming the rank-one equilibrium structure. The argument is a direct unfolding of the entry definition followed by simplification with cosh(0) = 1.
Claim. For any natural number $n$, vector $α ∈ ℝ^n$, and indices $i,j$, the Hessian entry of the cost at the zero displacement satisfies $H_{ij}(α, 0) = α_i α_j$, where $H_{ij}(α, t) := α_i α_j · cosh(⟨α, t⟩)$ and ⟨α, t⟩ denotes the weighted sum ∑_k α_k t_k.
background
In the n-dimensional reciprocal cost the displacement vector t enters the cost only through the single scalar aggregate given by the weighted dot product. Vectors are maps from the finite index set Fin n to the reals, and the dot product is defined as the sum over components of α_i t_i. The Hessian entry is then defined to be the product α_i α_j times cosh of that aggregate, which immediately makes every Hessian matrix a rank-one object proportional to the outer product α ⊗ α.
proof idea
The proof unfolds the definition of the Hessian entry (which inserts the cosh of the dot product) and the definition of the dot product. At the zero function the dot product vanishes, so the identity cosh(0) = 1 reduces the expression to the product α_i α_j.
why it matters
The result is invoked by the companion theorem that the full Hessian matrix at zero equals the outer-product matrix. It confirms the rank-one equilibrium model required by the n-dimensional cost construction, consistent with the one-dimensional J-cost whose Hessian at equilibrium is fixed by the self-similar point. The module supplies the Hessian formulas referenced by Metric.lean.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.