affineShift_mem_LevelSet
plain-language theorem explainer
The result shows that shifting a point on the level set α · t = c along a vector in the radical α · v = 0 keeps the image on the same level set. Researchers proving integrability of rank-one radical distributions cite it. The argument rewrites memberships to dot-product equations, substitutes the linearity identity for the affine shift, and closes by ring.
Claim. Assume $α · t = c$ and $α · v = 0$. Then $α · (t + s v) = c$ for every real $s$.
background
The module treats the radical distribution of the rank-one log-coordinate Hessian, which detects only the active direction α. The radical is therefore the hyperplane {v | α · v = 0} and the level sets are the parallel affine hyperplanes {t | α · t = c}, where the dot product is the weighted sum ∑ α_i t_i over the n coordinates.
proof idea
The proof rewrites both hypothesis and goal via the equivalence that equates level-set membership to the dot-product equation. It isolates α · v = 0 from the radical assumption. Substituting into the upstream linearity identity for the dot product under affine shift yields α · t + s · 0, which equals c by hypothesis on t. The ring tactic finishes the equality.
why it matters
This lemma is invoked directly by radical_integrable_by_affine_leaves to conclude that the radical distribution is integrable because its flows remain inside the affine hyperplanes. It also appears in the proof of preserves_own_leaf_iff_mem_Radical. In the Recognition framework the result confirms the integrability property required for the N-dimensional cost model, consistent with the rank-one structure of the log-coordinate Hessian.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.