affineShift_mem_LevelSet
If t satisfies dot α t = c and v satisfies dot α v = 0, then the affine shift t + s v satisfies dot α (t + s v) = c. Analysts of the rank-one Hessian in the Recognition Science cost model cite this to confirm that radical directions preserve affine leaves. The proof is a direct algebraic reduction that invokes dot linearity and closes by ring simplification.
claimLet $dot_α$ denote the weighted dot product. If $dot_α t = c$ and $dot_α v = 0$, then $dot_α (t + s v) = c$ for any real scalar $s$.
background
The RadicalDistribution module treats the log-coordinate Hessian as rank-one, so its radical is the hyperplane kernel of the active direction α. Radical α is defined as the set of vectors v with dot α v = 0. LevelSet α c is the parallel affine hyperplane {t | dot α t = c}. The dot operation is the finite sum ∑ α_i t_i over Fin n. AffineShift t v s is the translation t + s · v. The upstream theorem dot_affineShift records the expansion dot α (t + s v) = dot α t + s · dot α v. The equivalence mem_LevelSet_iff is the tautological membership statement for these sets.
proof idea
The term proof first rewrites both the hypothesis ht and the goal with mem_LevelSet_iff. It extracts dot α v = 0 from the radical membership hv. It then substitutes the expansion supplied by dot_affineShift and finishes with the ring tactic on the resulting linear identity.
why it matters in Recognition Science
The lemma is invoked verbatim inside radical_integrable_by_affine_leaves, which states that the radical distribution is integrable because its flows remain inside the affine hyperplanes dot α = c. This supplies the local leaf-preservation step required for integrability of the radical in the N-dimensional cost model. In the Recognition framework the result supports the decomposition of the Hessian into active and radical directions that follows from the rank-one structure in the forcing chain.
scope and limits
- Does not claim leaf preservation for vectors outside the radical.
- Does not prove integrability of the distribution.
- Does not restrict the dimension n or the vector α.
- Does not address curvature or global metric properties.
Lean usage
intro t v ht hv s; exact affineShift_mem_LevelSet α ht hvformal statement (Lean)
103theorem affineShift_mem_LevelSet {n : ℕ} (α : Vec n) {c s : ℝ} {t v : Vec n}
104 (ht : t ∈ LevelSet α c) (hv : v ∈ Radical α) :
105 affineShift t v s ∈ LevelSet α c := by
proof body
Term-mode proof.
106 rw [mem_LevelSet_iff] at ht ⊢
107 have hv' : dot α v = 0 := hv
108 rw [dot_affineShift, ht, hv']
109 ring
110
111/-- The radical distribution is integrable: its integral leaves are the affine
112hyperplanes `dot α = c`. -/