quadraticHessian_eq_zero_iff
plain-language theorem explainer
The Hessian quadratic form vanishes exactly when the vector lies in the hyperplane orthogonal to the active direction under the weighted dot product. Researchers modeling rank-one log-coordinate metrics in the cost framework would cite this to identify the kernel of the Hessian. The proof substitutes the closed-form expression for the quadratic form, invokes positivity of the hyperbolic cosine, and applies the definition of the radical set.
Claim. For vectors $α, t, v ∈ ℝ^n$, the quadratic form of the Hessian vanishes if and only if the weighted inner product of $α$ and $v$ is zero.
background
The module treats the radical distribution of the rank-one log-coordinate Hessian. This Hessian detects only the single active direction $α$, so its radical is the hyperplane where the weighted dot product vanishes. The weighted dot product is the sum $∑_i α_i t_i$ over components. The quadratic form itself expands to cosh of the dot product with $t$ times the square of the dot product with $v$.
proof idea
The proof rewrites the quadratic form via its explicit identity as a positive multiple of the squared dot product. It splits into two directions of the equivalence. One direction uses positivity of the hyperbolic cosine and the zero-product lemma to force the dot product to zero. The converse substitutes the membership condition directly into the rewritten expression.
why it matters
This equivalence pins down the kernel of the Hessian quadratic form for the rank-one case and supports the affine leaves orthogonal to the active direction. It fills a basic property in the radical-distribution construction within the cost module. No immediate downstream theorems are listed, yet the result closes a local step needed for integrability arguments on the distribution.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.