sub_mem_Radical
The radical distribution of a rank-one Hessian metric is closed under vector subtraction. Researchers analyzing the geometry of the log-coordinate cost functional cite this result to confirm that the kernel forms a linear subspace. The argument rewrites subtraction via addition of a negated vector and invokes the established closure properties under addition and scalar multiplication.
claimLet $n$ be a natural number and let $α ∈ ℝ^n$. If $v, w ∈ ℝ^n$ satisfy $∑_{i=1}^n α_i v_i = 0$ and $∑_{i=1}^n α_i w_i = 0$, then $∑_{i=1}^n α_i (v_i - w_i) = 0$.
background
The module defines the radical distribution of the rank-one log-coordinate Hessian metric. Radical α is the set of vectors v such that the weighted dot product ∑ α_i v_i equals zero; this hyperplane is orthogonal to the single active direction α. Vec n is the type of n-component real vectors, realized as maps from Fin n to ℝ, with the dot product supplying the natural pairing.
proof idea
The proof is a one-line wrapper. It rewrites v - w as v + (-1) • w via sub_eq_add_neg, then applies add_mem_Radical to the pair consisting of v and the scaled vector, where the scaled vector lies in Radical α by smul_mem_Radical.
why it matters in Recognition Science
This result completes the subspace axioms for the radical distribution inside the module. It supports the subsequent treatment of affine leaves {t | dot α t = c} and feeds the analysis of the Hessian quadratic form that vanishes exactly on this distribution. In the Recognition Science setting it supplies a basic linear-algebra fact for the rank-one metric that appears in the cost functional.
scope and limits
- Does not prove that Radical α is a vector subspace over the reals.
- Does not address nonempty-ness or dimension of the radical.
- Does not connect to the number-theoretic radical imported from ArithmeticFunctions.
- Does not treat the Hessian quadratic form vanishing condition.
formal statement (Lean)
67theorem sub_mem_Radical {n : ℕ} (α : Vec n) {v w : Vec n}
68 (hv : v ∈ Radical α) (hw : w ∈ Radical α) :
69 v - w ∈ Radical α := by
proof body
Term-mode proof.
70 simpa [sub_eq_add_neg] using
71 add_mem_Radical α hv (smul_mem_Radical α (-1) hw)
72
73/-- The Hessian quadratic form vanishes exactly on the radical distribution. -/