affineShift
The affineShift definition supplies the n-dimensional vector t + s v via componentwise addition. Analysts of radical distributions for rank-one log-Hessian metrics cite it to parameterize motion along the kernel while staying inside level sets of the dot product with the active direction. The definition is introduced directly as the generator of those affine leaves.
claimFor vectors $t, v$ in the space of $n$-component real tuples and scalar $s$, the affine shift is the vector whose $i$-th component equals $t_i + s v_i$.
background
In the module setting the log-coordinate Hessian is rank one, detecting only a single active direction α; its radical distribution is therefore the hyperplane orthogonal to α. Vectors are realized as maps from Fin n to the reals. Affine leaves are the level sets {t | dot α t = c} that foliate the space. The upstream Vec abbreviation supplies the coordinate-function representation used throughout.
proof idea
The definition is a direct one-line componentwise construction: the output at each index i is t i plus s times v i. No lemmas or tactics are applied; the body is the primitive operation later unfolded in dot-product calculations and membership proofs.
why it matters in Recognition Science
The definition feeds the four downstream results that establish preservation of level sets, the explicit dot-product formula under shift, the equivalence between leaf preservation and membership in the radical, and the integrability statement that the radical is foliated by affine hyperplanes. It thereby completes the formalization of the constant hyperplane distribution for the rank-one case in the log-coordinate metric.
scope and limits
- Does not assume any particular value of n.
- Does not impose orthogonality or other constraints on v.
- Does not define the radical distribution or the active direction α.
- Does not compute costs, Hessians, or integrals.
formal statement (Lean)
28def affineShift {n : ℕ} (t v : Vec n) (s : ℝ) : Vec n :=
proof body
Definition body.
29 fun i => t i + s * v i
30