xFlatConnection_apply
plain-language theorem explainer
The result shows that the flat affine connection in x-coordinates evaluates to zero for any dimension, vector, and index triple. Researchers simplifying expressions in the pulled-back connection within the Recognition Science cost module would cite it during algebraic reductions. The proof proceeds by direct reflexivity on the defining equation.
Claim. Let $n$ be a natural number, $x$ a vector in $R^n$, and $i,j,k$ indices in the finite set of size $n$. The flat affine connection in $x$-coordinates satisfies $xFlatConnection(x,i,j,k)=0$.
background
The module records affine connections in $x$- and $t$-coordinates, where $t_i = log x_i$. The $t$-coordinates are affine-flat by construction; the pullback to $x$-coordinates yields the flat connection. Vec is the abbreviation for $n$-component real vectors, written as maps from Fin $n$ to reals. The upstream definition xFlatConnection sets this connection to the constant zero function on all inputs.
proof idea
The proof is a one-line wrapper that applies reflexivity directly to the definition of xFlatConnection.
why it matters
This supplies the basic simplification rule for the flat connection in $x$-coordinates, supporting later calculations of the pulled-back structure in the Recognition Science framework. It aligns with the module's statement that $t = log x$ coordinates are affine-flat. No downstream uses are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.