applyHessian_of_dot_zero
plain-language theorem explainer
Vectors orthogonal to the weighting vector α under the dot product lie in the kernel of the Hessian operator for the n-dimensional reciprocal cost. This confirms the rank-one character of the Hessian once the cost is expressed in log-coordinates. Workers on the Recognition Science cost model cite it when analyzing null directions of the quadratic form. The proof reduces the vector equality to components via extensionality and simplifies directly with the directional property of the Hessian action.
Claim. Let $n$ be a natural number and let $α, t, v$ be vectors in $ℝ^n$. If the weighted inner product $⟨α, v⟩ = ∑ α_i v_i$ vanishes, then the Hessian operator applied to $v$ at $t$ returns the zero vector.
background
The module supplies Hessian formulas for the n-dimensional reciprocal cost. In log-coordinates the cost depends only on the single weighted aggregate given by the dot product, so the Hessian is rank one and factors through the outer product α ⊗ α. Vec n is the type of n-component real vectors, realized as maps from Fin n to ℝ. The dot product is the weighted sum ∑_{i} α_i t_i. The upstream theorem applyHessian_eq_direction states that the Hessian action is always parallel to α: applyHessian α t v equals the vector whose i-th component is cosh(dot α t) ⋅ α_i ⋅ dot α v.
proof idea
The proof is a one-line wrapper. It applies function extensionality to reduce the vector equality to a pointwise claim, then simplifies using the directional equality applyHessian_eq_direction together with the hypothesis that dot α v = 0.
why it matters
The result shows that the orthogonal complement of α lies in the kernel of the Hessian, confirming that the operator has rank one. It supports the module claim that the n-dimensional cost depends only on the single aggregate dot α t. Within the Recognition Science framework this property aligns with the reduction of the cost to a one-dimensional effective potential along the forcing direction. No downstream uses are recorded, but the lemma closes a basic algebraic fact required for quadratic-form analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.