mem_Radical_iff
Membership in the radical distribution of a rank-one Hessian is equivalent to the weighted dot product with the active direction vanishing. Analysts of the log-coordinate cost metric invoke this equivalence to identify the kernel of the associated quadratic form. The proof is immediate reflexivity on the set predicate defining the distribution.
claimFor $n$ a natural number and vectors $α, v$ in $ℝ^n$, $v$ belongs to the radical distribution of $α$ if and only if the weighted dot product $α · v$ equals zero.
background
The RadicalDistribution module formalizes the radical of the rank-one log-coordinate Hessian metric. This Hessian detects only the single active direction $α$, so its radical is the hyperplane orthogonal to $α$ under the weighted dot product, realized as the affine leaves where the dot product equals a constant.
proof idea
The proof applies Iff.rfl, which is reflexivity on the biconditional. This directly equates the membership predicate to the defining condition in the set Radical $α$.
why it matters in Recognition Science
The result is invoked by quadraticHessian_eq_zero_iff to show that the Hessian quadratic form vanishes exactly on the radical distribution. It supports the formalization of the cost metric in N dimensions, consistent with the rank-one structure in the Recognition Science treatment of the Hessian and its role in the forcing chain.
scope and limits
- Does not determine the codimension of the radical hyperplane.
- Does not address integration or measures on the distribution.
- Does not extend to Hessians of rank greater than one.
- Does not fix any concrete value for the dimension n.
formal statement (Lean)
31@[simp] theorem mem_Radical_iff {n : ℕ} (α : Vec n) (v : Vec n) :
32 v ∈ Radical α ↔ dot α v = 0 := Iff.rfl
proof body
33