add_mem_Radical
plain-language theorem explainer
Vectors orthogonal to a fixed direction α remain closed under addition in the radical of the rank-one Hessian. Analysts of the log-coordinate metric cite this to confirm the kernel is an additive subgroup. The proof unfolds the dot-product definition of Radical, extracts the two zero-sum conditions, and reduces the claim to linearity of summation via mul_add and ring.
Claim. Let $n$ be a natural number and let $α, v, w$ be vectors in $ℝ^n$. If $∑_i α_i v_i = 0$ and $∑_i α_i w_i = 0$, then $∑_i α_i (v_i + w_i) = 0$.
background
In the module on radical distribution for the rank-one log-coordinate metric, the Hessian detects only the active direction α. Its radical is the hyperplane orthogonal to α. Vec n is the type of n-component real vectors, realized as functions Fin n → ℝ. The dot product is the weighted sum ∑_{i:Fin n} α i * t i. Radical α is defined as the set of vectors v satisfying dot α v = 0, which supplies the affine leaves {t | dot α t = c}.
proof idea
The tactic proof unfolds Radical and dot at the hypotheses and goal. It introduces the two summation equalities hv0 and hw0. A calc block then rewrites the target sum as the sum of the two given zero sums by distributing multiplication over addition and applying Finset.sum_add_distrib, after which mul_add and ring close the equality to zero.
why it matters
The result supplies the additive closure needed for the radical to behave as a linear subspace in the cost framework. It is invoked directly by sub_mem_Radical to obtain closure under subtraction. This step supports the formal treatment of the kernel of the rank-one Hessian arising from the logarithmic aggregate, consistent with the single-active-direction structure in the Recognition Science cost model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.