xDirection
plain-language theorem explainer
The xDirection definition supplies the componentwise ratio vector with entries α_i / x_i for n-dimensional vectors α and x. Analysts deriving the Hessian of the multi-component reciprocal cost cite this auxiliary to isolate the active direction. It is realized by direct pointwise division in a one-line definition.
Claim. For vectors $α, x : ℝ^n$, the active $x$-direction is the vector $d$ with components $d_i = α_i / x_i$.
background
The module records positive-coordinate Hessian formulas for the multi-component reciprocal cost. Vectors are realized as coordinate functions Vec n := Fin n → ℝ. The general entry formula is written in terms of the positive aggregate R = aggregate α x, after which the 2×2 case yields a closed determinant factorization together with zero-cost degeneracy and nondegeneracy criteria away from the neutral locus.
proof idea
This definition is a one-line wrapper that applies componentwise division: the i-th entry is α i divided by x i.
why it matters
This auxiliary feeds xHessianEntry and its specializations to diagonal, off-diagonal, and zero-cost cases, supporting the determinant factorization in the 2×2 setting. It supplies the active direction term inside the positive-coordinate Hessian formulas of the module. The construction sits inside the J-cost framework and connects to the phi-ladder corrections appearing in related capacity results.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.