radical_integrable_by_affine_leaves
plain-language theorem explainer
The radical distribution of the rank-one Hessian metric integrates to the affine hyperplanes orthogonal to the active direction α. Researchers analyzing the geometry of the cost function in the N-dimensional setting cite this result to confirm that shifts along the kernel preserve the foliation. The proof is a one-line wrapper that invokes the membership preservation theorem for affine shifts.
Claim. Let $n$ be a natural number, let $α ∈ ℝ^n$, and let $c ∈ ℝ$. For all vectors $t, v ∈ ℝ^n$ such that $⟨α, t⟩ = c$ and $⟨α, v⟩ = 0$, and for every real scalar $s$, the translated vector $t + s v$ satisfies $⟨α, t + s v⟩ = c$.
background
The module treats the radical distribution of the rank-one log-coordinate Hessian, which detects only the single active direction α. Radical is the kernel {v | ⟨α, v⟩ = 0}. LevelSet is the family of affine hyperplanes {t | ⟨α, t⟩ = c}. Affine shift is the translation map sending (t, v, s) to the vector whose i-th component is t_i + s v_i. The local setting is the rank-one case of the Hessian metric on log-coordinates, where the distribution is constant and its integrability reduces to preservation of these hyperplanes. The key upstream result is the theorem that affine shifts along radical vectors remain inside a fixed LevelSet.
proof idea
The proof introduces the vectors t and v together with the membership hypotheses and the scalar s, then applies the upstream theorem affineShift_mem_LevelSet directly to obtain the required membership in the target LevelSet.
why it matters
This result establishes integrability of the radical distribution, confirming that its leaves are precisely the affine hyperplanes orthogonal to α. It supplies the basic geometric fact needed for any further analysis of the cost function in the N-dimensional radical setting. In the Recognition Science framework it aligns with the rank-one structure forced by the log-coordinate metric and the active edge count A = 1. The declaration closes a foundational step with no open scaffolding remaining.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.