metricEntry_zero
plain-language theorem explainer
The result shows that the metric entry derived from the Hessian reduces exactly to the outer product of the coordinate vector components when the auxiliary function is identically zero. Researchers modeling cost in log coordinates cite it to simplify equilibrium calculations in n-dimensional settings. The proof first records that the weighted dot product with the zero function vanishes, then substitutes the Hessian and metric definitions to finish.
Claim. For any natural number $n$, vector $a : Fin n → ℝ$, and indices $i,j ∈ Fin n$, the metric entry $M(a,0,i,j)$ equals $a_i a_j$, where $M(a,t,i,j) := a_i a_j cosh(a · t)$ and the zero function corresponds to the equilibrium point.
background
The module develops the cost metric in log coordinates. Vectors are maps from Fin n to ℝ. The weighted dot product is defined by summation of componentwise products. The Hessian entry is the product of components times the hyperbolic cosine of the dot product; the metric entry is identical to the Hessian entry by definition. An upstream equilibrium result states that the J-cost vanishes at the unit point, which is realized here by substituting the zero function.
proof idea
The tactic proof first introduces an auxiliary equality by unfolding the dot-product definition and simplifying the resulting sum to zero. It then applies simp to the goal, expanding the metric and Hessian entries and substituting the auxiliary equality.
why it matters
This theorem supplies the explicit reduction of the metric to the outer-product form at equilibrium, matching the Hessian model comment in the same file. It closes the link between the cost metric and the equilibrium theorem from nonlinear dynamics. In the Recognition framework it supports the log-coordinate treatment of the J-cost functional and the transition to the phi-ladder mass formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.