linearTwoSimplexMap_face_one
plain-language theorem explainer
The middle face δ₁ of the lift-affine singular 2-simplex on lifts (p,q,r) equals the geodesic 1-simplex from p to r on S¹. Anyone computing the free singular boundary of that 2-simplex cites this face identification. The proof is a short pointwise calculation: unwind face and the two maps, insert the barycentric identities for δ₁, then finish by ring.
Claim. For all real lifts $p,q,r$, the face $\delta_1$ of the lift-affine singular $2$-simplex on $(p,q,r)$ equals the geodesic singular $1$-simplex from $p$ to $r$ on $S^1$.
background
This 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 is the chain-level reason winding is a homology invariant and 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 from lifts $a$ to $b$ is the projection of the straight line $(1-t)a+tb$ in the universal cover $\mathbb{R}\to S^1$. The lift-affine $2$-simplex on $(p,q,r)$ is the analogous affine map on barycentric coordinates, projected to the circle.
On the side face $\delta_1$, the middle barycentric coordinate vanishes and the last coordinate equals the terminal $\Delta^1$ coordinate; those two coordinate lemmas feed the face computation directly.
proof idea
Pointwise extensionality on $\Delta^1$. Unfold the face as composition with the face map, then the definitions of the lift-affine $2$-simplex and the geodesic $1$-simplex. Rewrite the two barycentric coordinates of $\delta_1$ via the face-map lemmas (middle coordinate $0$, last coordinate equal to the $\Delta^1$ terminal weight). A single congruence reduces the remaining scalar identity to a ring calculation on the affine combination $(1-t)p+tr$.
why it matters
This is one of the three face identities needed for 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)$. In particular $\mathrm{geo}(p,q)+\mathrm{geo}(q,r)$ is homologous to $\mathrm{geo}(p,r)$, so geodesics compose additively in $H_1$.
That composition law is the concrete algebraic engine behind the module's kills-boundaries theorem and the winding homomorphism on $1$-cycles. Together with the fact that the once-around generator has winding $1$, it gives the left-inverse half of the integer comparison $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The surjectivity half still needs a simplicial prism or subdivision operator not yet in Mathlib singular homology; this lemma sits entirely on the proved, axiom-free side of that split.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.