Radical
plain-language theorem explainer
Radical defines the radical distribution of the rank-one Hessian metric as the hyperplane orthogonal to the active direction α. Researchers analyzing the logarithmic cost geometry in n dimensions cite it when proving that the Hessian quadratic form vanishes on this set or when showing integrability via affine leaves. The definition is a direct set comprehension built from the weighted dot product.
Claim. For a vector α in ℝ^n, the radical distribution is the set {v in ℝ^n | α · v = 0}.
background
Vec n is the space of n-component real vectors, written as functions Fin n → ℝ. The dot product is the weighted sum ∑_{i:Fin n} α_i v_i, the inner product underlying the logarithmic aggregate in the cost model. The module treats the log-coordinate Hessian as rank-one, detecting only the active direction α, so its radical distribution is the constant hyperplane orthogonal to α, with integrability expressed through the affine leaves {t | dot α t = c}.
proof idea
The definition is a one-line set comprehension that applies the upstream dot product: Radical α collects every v such that dot α v = 0. It directly invokes the Core definitions of Vec and dot without further lemmas.
why it matters
This definition supplies the central object for the RadicalDistribution module and is invoked by eleven downstream results, including add_mem_Radical, quadraticHessian_eq_zero_iff, and radical_integrable_by_affine_leaves. It realizes the radical of the rank-one Hessian inside the Recognition Science cost geometry, supporting the framework's treatment of the log-coordinate metric and its affine-leaf integrability.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.