xFlatConnection
plain-language theorem explainer
The xFlatConnection definition supplies the zero-valued flat affine connection on x-coordinates for any dimension n. Coordinate-change calculations in the Recognition Science cost model cite this when contrasting the flat t-chart with its pullback. The implementation is a direct constant definition that requires no further reduction.
Claim. The flat affine connection in $x$-coordinates is the zero map: for every $n : ℕ$, every vector $x : ℝ^n$, and every indices $i,j,k$, the connection coefficient equals $0$.
background
The Cost.Ndim.Connections module records affine connections in the original $x$-coordinates and in the logarithmic $t = log x$ coordinates. Vec n is the abbreviation for $n$-component real vectors used as coordinate functions. The upstream back structure embeds LogicNat into the positive reals via an exponential map, supplying the multiplicative group structure that justifies the logarithm.
proof idea
The declaration is a one-line definition that returns the constant real number zero regardless of its arguments. No lemmas are invoked; the body is the literal 0.
why it matters
This definition supplies the base flat connection that the subsequent theorem xFlatConnection_apply simplifies to zero by reflexivity. It anchors the projective equivalence dichotomy proved in the module, which shows the one-dimensional case is projectively equivalent to the zero connection while higher dimensions are not. The construction supports separation of the affine-flat $t$-chart from its $x$-pullback, consistent with the coordinate conventions in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.