preserves_own_leaf_iff_mem_Radical
plain-language theorem explainer
The equivalence states that a vector v preserves the affine leaf of the rank-one Hessian through any point t precisely when its dot product with the active direction α vanishes. Researchers working on the geometry of the log-coordinate metric would cite this to confirm that the radical distribution consists exactly of the integrable directions. The proof proceeds by a direct two-direction argument using the explicit formula for the dot product after an affine shift.
Claim. Let α, t, v be vectors in ℝⁿ. Then ∀ s ∈ ℝ, the point t + s v lies in the level set {x | α · x = α · t} if and only if α · v = 0.
background
The radical distribution is defined as the set of vectors v satisfying dot(α, v) = 0, which is the kernel of the rank-one Hessian metric induced by the single active direction α. The affine leaves are the level sets {x | dot(α, x) = c}, which serve as the integral manifolds orthogonal to α. This construction appears in the Ndim cost module, which formalizes the geometry of the logarithmic coordinate metric whose Hessian is rank one. The dot product is the weighted sum ∑ α_i t_i over the n components. The affine shift operation is defined by t + s v. The upstream lemma dot_affineShift states that dot(α, affineShift t v s) equals dot(α, t) + s · dot(α, v).
proof idea
The proof uses constructor to split the biconditional. In the forward direction, instantiate the universal quantifier at s = 1, rewrite via mem_LevelSet_iff and dot_affineShift, then apply linarith to conclude dot(α, v) = 0. In the reverse direction, apply the upstream theorem affineShift_mem_LevelSet directly to the hypothesis that v lies in the radical.
why it matters
This equivalence confirms that the radical distribution is precisely the set of directions that leave the affine leaves invariant, which is a key step in establishing the integrability of the distribution in the rank-one case. It supports the local claim in the RadicalDistribution module that the log-coordinate Hessian has a well-defined radical hyperplane. In the Recognition Science framework this aligns with the rank-one structure arising from J-uniqueness in the forcing chain, though the declaration has no listed downstream uses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.