linearTwoSimplexMap_face_zero

This module lifts path-level winding/displacement on $S^1$ to singular simplices and proves that displacement kills $2$-boundaries, giving the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.

A singular $2$-simplex is a continuous map $\Delta^2\to S^1$; its $i$-th face is composition with the standard face map $\delta_i:\Delta^1\to\Delta^2$. The geodesic $1$-simplex from lifts $a$ to $b$ is the projection of the straight line $(1-t)a+tb$ through the covering map $\mathbb{R}\to S^1$. The lift-affine $2$-simplex on $(p,q,r)$ is the analogous affine map on barycentric coordinates of $\Delta^2$, then projected to the circle.

On the side face $\delta_0$, the ambient barycentric coordinates satisfy $x_1=u_0$ and $x_2=u_1$ for the domain $\Delta^1$ coordinates $u$ (the two face-map coordinate lemmas used below).

Pointwise equality of continuous maps on $\Delta^1$. After ext, both sides simplify via the definitions of face (composition with the face map), the lift-affine $2$-simplex, and the geodesic $1$-simplex. The $\delta_0$ coordinate lemmas replace the ambient $x_1,x_2$ by the domain barycentric coordinates. The standard-simplex identity $u_0+u_1=1$ rewrites $u_0=1-u_1$, and ring matches the geodesic convex combination $(1-u_1)q+u_1 r$.

Feeds the geodesic composition law: the free singular boundary of the lift-affine $2$-simplex on $(p,q,r)$ is $\mathrm{geo}(q,r)-\mathrm{geo}(p,r)+\mathrm{geo}(p,q)$, so geodesics compose additively in $H_1$. That identity is the concrete chain-level witness that geodesic edges behave like a group law up to boundaries, which is the computational engine behind the module's kills-boundaries theorem and the winding left-inverse to the fundamental class on $S^1$.

In the broader Recognition foundation stack this is pure singular-homology scaffolding for the circle (no direct T0–T8 forcing step), but it closes the face bookkeeping needed before winding can be promoted from paths to homology classes.