LevelSet
LevelSet defines the affine hyperplanes of vectors t satisfying the linear condition dot α t = c for fixed direction α and level c. Researchers formalizing the radical distribution of the rank-one log-coordinate Hessian cite this to describe its integrable leaves. The definition is a direct set comprehension built from the weighted dot product.
claimFor direction vector $α ∈ ℝ^n$ and constant $c ∈ ℝ$, the level set is the affine hyperplane $ { t ∈ ℝ^n | α · t = c } $, where the dot product is the weighted sum $∑_{i=1}^n α_i t_i$.
background
The module formalizes the radical distribution of the rank-one log-coordinate metric Hessian, which detects only the single active direction α. Its radical is the hyperplane of vectors v with dot α v = 0; integrability is expressed through the parallel affine leaves { t | dot α t = c } at each level c. Vec n is the type of n-component real vectors (Fin n → ℝ). The dot operation is the weighted inner product ∑ α i * t i used by the logarithmic aggregate.
proof idea
This is a direct definition that sets LevelSet α c to the set comprehension { t | dot α t = c }. It is a one-line wrapper around the set notation using the upstream dot product; no lemmas or tactics are invoked.
why it matters in Recognition Science
The definition supplies the explicit affine leaves needed to prove integrability of the radical distribution. It is invoked by affineShift_mem_LevelSet (shifts along radical directions stay inside a leaf) and radical_integrable_by_affine_leaves (the distribution is integrable by these hyperplanes). This supports the rank-one character of the log-coordinate Hessian, consistent with the single active direction in the Recognition Science forcing chain (T5 J-uniqueness onward).
scope and limits
- Does not impose any norm or length condition on α.
- Does not equip the level sets with a measure or integration structure.
- Does not relate the construction to the phi-ladder or mass formulas.
- Does not restrict the ambient dimension n.
formal statement (Lean)
24def LevelSet {n : ℕ} (α : Vec n) (c : ℝ) : Set (Vec n) :=
proof body
Definition body.
25 { t | dot α t = c }
26
27/-- Affine translation along a constant direction. -/