mem_LevelSet_iff
plain-language theorem explainer
Membership of a vector t in the affine leaf orthogonal to direction α at level c is equivalent to the dot product α · t equaling c. Researchers formalizing the radical distribution of the rank-one log-coordinate Hessian cite this equivalence to simplify membership tests in affine leaves. The proof is a direct one-line reflexivity on the defining predicate of the level set.
Claim. Let $n$ be a natural number, let $α, t$ be vectors in $ℝ^n$, and let $c$ be real. Then $t$ belongs to the affine hyperplane $ { s | α · s = c } $ if and only if $α · t = c$.
background
The module develops the radical distribution attached to the rank-one log-coordinate Hessian, whose kernel is the hyperplane orthogonal to the single active direction α. Affine leaves are the parallel hyperplanes { t | dot α t = c } that foliate the space and support integrability statements. Vec is the type of n-component real vectors realized as maps from Fin n to reals; dot is the weighted inner product ∑ α_i t_i.
proof idea
One-line wrapper that applies the definition of LevelSet via Iff.rfl.
why it matters
The equivalence is invoked by affineShift_mem_LevelSet to verify that radical directions preserve each leaf and by preserves_own_leaf_iff_mem_Radical to characterize the radical as those directions that fix their own leaf. It supplies the basic rewriting tool for the affine-leaf description of the radical distribution in the cost model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.