LevelSet
plain-language theorem explainer
LevelSet defines the affine hyperplanes orthogonal to a direction α at height c in n-dimensional space. Researchers working on integrability of radical distributions for rank-one log-coordinate Hessians cite this definition. It is introduced as a direct set comprehension that applies the weighted dot product from Core.
Claim. For a vector α in ℝ^n and scalar c in ℝ, the level set is the affine hyperplane { t in ℝ^n | α · t = c }.
background
Vec n is the type of n-component real vectors, written as functions Fin n → ℝ. The dot operation is the weighted sum ∑_{i} α_i t_i that appears in the logarithmic aggregate. The module sets up the radical distribution of the rank-one log-coordinate Hessian, whose kernel is the hyperplane dot α v = 0; the affine leaves { t | dot α t = c } are introduced to make integrability statements precise.
proof idea
One-line definition that directly constructs the set via the predicate dot α t = c, using the upstream dot and Vec declarations.
why it matters
The definition is used by affineShift_mem_LevelSet, mem_LevelSet_iff, preserves_own_leaf_iff_mem_Radical and radical_integrable_by_affine_leaves. These results establish that the radical distribution is integrable precisely because its integral manifolds are the stated affine hyperplanes. The construction therefore supplies the concrete geometric object required by the module's treatment of the rank-one log-coordinate metric.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.