mem_Radical_iff
plain-language theorem explainer
The membership criterion for the radical distribution of a rank-one Hessian states that a vector v lies in Radical α precisely when its weighted inner product with α vanishes. Researchers working on the logarithmic cost metric in higher dimensions would invoke this equivalence to characterize the kernel of the Hessian quadratic form. The proof is a one-line reflexivity on the definition of Radical.
Claim. For vectors $α, v ∈ ℝ^n$, $v$ belongs to the radical distribution of $α$ if and only if the weighted dot product $α · v = 0$.
background
In the module on radical distributions for the rank-one log-coordinate metric, the Hessian detects only the active direction α. Its radical distribution is the hyperplane orthogonal to α, formalized as the set of vectors satisfying the defining predicate dot α v = 0. Vec n is the type of n-component real vectors (Fin n → ℝ) and dot is the weighted sum ∑ α_i v_i from the Core module for the logarithmic aggregate.
proof idea
The proof is a one-line wrapper that applies reflexivity of logical equivalence directly to the defining predicate of Radical α.
why it matters
This theorem supplies the membership test used by quadraticHessian_eq_zero_iff to establish that the Hessian quadratic form vanishes exactly on the radical distribution. It completes the basic kernel characterization for the rank-one case in the N-dimensional cost framework, supporting analysis of the log-coordinate metric whose radical is the constant hyperplane orthogonal to the active direction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.