smul_mem_Radical
plain-language theorem explainer
The theorem shows that the radical hyperplane orthogonal to a fixed direction α remains invariant under scaling by any real scalar s. Researchers analyzing the n-dimensional cost Hessian would cite this when confirming that the radical forms a linear subspace. The proof expands the scaled dot product, factors the scalar via finite-sum distributivity, and reduces to the hypothesis via ring algebra.
Claim. Let $n$ be a natural number, let $α, v ∈ ℝ^n$, and let $s ∈ ℝ$. If $∑_i α_i v_i = 0$, then $∑_i α_i (s v_i) = 0$.
background
The module treats the radical distribution of the rank-one log-coordinate Hessian, which detects only the single active direction α. Radical α is the hyperplane {v | dot α v = 0}, where dot is the weighted sum ∑ α_i v_i and Vec n denotes the space of functions Fin n → ℝ. The module also introduces the affine leaves {t | dot α t = c} to capture integrability along directions orthogonal to α.
proof idea
The tactic proof unfolds Radical and dot at the hypothesis and goal. It rewrites ∑ α_i (s v_i) as s ⋅ ∑ α_i v_i by Finset.mul_sum and sum_congr with ring, then substitutes the hypothesis that the inner sum vanishes and applies ring to obtain zero.
why it matters
This result is invoked by the downstream theorem sub_mem_Radical to establish closure under subtraction, thereby helping confirm that Radical α is a linear subspace. It supports the module's formalization of affine leaves for the rank-one Hessian metric in the cost framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.