zero_mem_Radical
plain-language theorem explainer
The zero vector satisfies the orthogonality condition defining the radical distribution of any rank-one Hessian metric. Researchers analyzing the logarithmic cost functional cite this to confirm the origin lies in the degenerate hyperplane. The proof is a one-line term-mode reduction that unfolds the set membership and dot product definitions then simplifies the resulting sum to zero.
Claim. Let $n$ be a natural number and let $α$ be any vector in $ℝ^n$. The zero vector $0 ∈ ℝ^n$ satisfies $∑_{i=1}^n α_i · 0 = 0$, hence belongs to the set ${v ∈ ℝ^n | ∑_{i=1}^n α_i v_i = 0}$.
background
The module defines the radical distribution of the rank-one log-coordinate Hessian metric. This distribution is the hyperplane orthogonal to the single active direction $α$, consisting of all vectors $v$ such that the weighted dot product equals zero. Vec $n$ denotes the space of $n$-component real vectors as maps from Fin $n$ to $ℝ$, while dot $α$ $t$ is the sum $∑ α_i t_i$ over components.
proof idea
The proof is a one-line term-mode reduction. It unfolds the definition of the radical set, replaces membership by the equality dot $α$ $0$ = 0, expands the dot product to its explicit sum, and applies simp to obtain the identity 0 = 0.
why it matters
This theorem supplies the base membership fact for the radical distribution in the cost analysis. It verifies that the origin satisfies the defining orthogonality condition of the rank-one Hessian. In the Recognition framework the result anchors the treatment of degenerate directions within the logarithmic metric, supporting later properties of affine leaves and integrability over the distribution.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.