linearTwoSimplexMap_face_two
plain-language theorem explainer
The base face δ₂ of the lift-affine singular 2-simplex on real lifts (p,q,r) equals the geodesic 1-simplex from p to q on S¹. Anyone computing the free singular boundary of that 2-simplex, or proving geodesic composition in H₁(S¹), cites this face identity. The proof is pointwise: unwind the face composite, insert the two barycentric identities for δ₂, and finish by ring.
Claim. For all real lifts $p,q,r$, the face $\delta_2$ of the lift-affine continuous map $\Delta^2\to S^1$ determined by $(p,q,r)$ equals the geodesic singular $1$-simplex from $p$ to $q$ (the projection of the straight line in the cover $\mathbb{R}\to S^1$).
background
The module lifts path-level winding and displacement on $S^1$ to singular simplices and proves that displacement kills boundaries: for every singular $2$-simplex $F$, $\mathrm{disp}(\delta_0 F)-\mathrm{disp}(\delta_1 F)+\mathrm{disp}(\delta_2 F)=0$. That identity, with the generator evaluation on the once-around loop, supplies 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 on lifts $a,b$ is the projection of the affine path $t\mapsto(1-t)a+tb$ through the covering $\mathbb{R}\to S^1$. The lift-affine $2$-simplex on $(p,q,r)$ is the analogous affine interpolation in the cover, projected to $S^1$.
Two coordinate lemmas pin the base face: on $\delta_2$, the second barycentric coordinate of $\Delta^1$ is preserved, and the cone coordinate $x_2$ vanishes. Those are exactly the identities needed to match the geodesic formula on the $p$–$q$ edge.
proof idea
Pointwise equality of continuous maps on $\Delta^1$. After ext x, simplify the definitions of face (composition with the face map), the lift-affine $2$-simplex, and the geodesic $1$-simplex. Rewrite the two barycentric coordinates of $\delta_2$ via faceMap_two_coord_one and faceMap_two_coord_two (second coordinate preserved, cone coordinate zero). The remaining real-linear combination of $p$ and $q$ matches the geodesic parameter by congr 1 and ring.
why it matters
This is one of the three face evaluations that assemble the free singular boundary of the lift-affine $2$-simplex. The immediate parent is the geodesic composition law: that boundary equals $\mathrm{geo}(q,r)-\mathrm{geo}(p,r)+\mathrm{geo}(p,q)$, so $\mathrm{geo}(p,q)+\mathrm{geo}(q,r)$ is homologous to $\mathrm{geo}(p,r)$ in $H_1$. Without the $\delta_2$ face matching $\mathrm{geo}(p,q)$, the free-module boundary computation does not close.
In the module narrative this supports the chain-level “winding kills boundaries” identity and the left-inverse half of the integer comparison $H_1(S^1;\mathbb{Z})\to\mathbb{Z}$. The converse generation half still needs a simplicial prism or subdivision operator that Mathlib singular homology does not yet supply; this lemma is pure face geometry and does not touch that gap.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.