affineShift
plain-language theorem explainer
The affineShift definition constructs the vector obtained by translating t along direction v by scalar s in n dimensions. Researchers working on integrability of the radical distribution for the log-coordinate Hessian cite this construction to handle affine leaves. It is supplied as a direct componentwise definition that enables level-set preservation lemmas.
Claim. For vectors $t, v : Vec n$ and scalar $s : ℝ$, the affine shift is the vector whose $i$-th component equals $t_i + s v_i$ for each index $i$.
background
Vec n is the type of n-component real vectors, represented as functions Fin n → ℝ. The module develops the radical distribution of the rank-one log-coordinate Hessian, which is the hyperplane orthogonal to the active direction α under the weighted dot product. Affine leaves are the level sets {t | dot α t = c}.
proof idea
This is a direct definition implemented as the lambda fun i => t i + s * v i. No lemmas are applied; it is the primitive operation for affine translations in the vector space.
why it matters
This definition supports the key results on the radical distribution being integrable via its affine leaves. It is used in affineShift_mem_LevelSet to show shifts along radical directions preserve level sets, in dot_affineShift to compute the dot product after shift, and in radical_integrable_by_affine_leaves to establish integrability. In the Recognition Science framework it underpins analysis of the Hessian radical within the cost function for the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.