sub_mem_Radical
plain-language theorem explainer
The declaration shows that the radical distribution of a rank-one Hessian metric is closed under vector subtraction. Analysts of the logarithmic cost function in multiple dimensions cite it to confirm the distribution forms a linear subspace. The proof reduces subtraction to addition after scaling by -1 and invokes the corresponding additive and scalar-multiplication closure results.
Claim. Let $n$ be a natural number and let $α ∈ ℝ^n$. If $v, w ∈ ℝ^n$ satisfy $α · v = 0$ and $α · w = 0$, then $α · (v - w) = 0$.
background
The module defines the radical distribution of the rank-one log-coordinate Hessian metric as the hyperplane orthogonal to the active direction α, specifically the set of vectors v such that the weighted dot product α · v = 0. This follows from the fact that the Hessian only detects the single active direction α, leading to affine leaves { t | α · t = c }. The vector space Vec n consists of functions from Fin n to ℝ. Upstream results establish closure under addition and scalar multiplication for this set.
proof idea
The proof is a one-line term-mode application of simpa that rewrites subtraction via v - w = v + (-1) · w and then applies the add_mem_Radical and smul_mem_Radical lemmas to conclude membership.
why it matters
This result confirms that the radical distribution is a vector subspace, which is a prerequisite for showing that the Hessian quadratic form vanishes exactly on it. It supports the formalization of integrability over the affine leaves in the cost model. In the Recognition Science framework it contributes to the N-dimensional cost structure underlying the derivation of spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.