metricEntry_zero
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not address metric entries for nonzero auxiliary functions.
- Does not extend to infinite-dimensional or non-Euclidean index sets.
- Does not derive any dynamical evolution or stability properties.
- Does not connect directly to the Recognition Composition Law or the forcing chain steps T5-T8.
formal statement (Lean)
15@[simp] theorem metricEntry_zero {n : ℕ} (α : Vec n) (i j : Fin n) :
16 metricEntry α (fun _ => 0) i j = α i * α j := by
proof body
Tactic-mode proof.
17 have hdot : dot α (fun _ => 0) = 0 := by
18 unfold dot
19 simp
20 simp [metricEntry, hessianEntry, hdot]
21
22/-- The metric at equilibrium coincides with the outer-product Hessian model. -/