linearSingularTwoSimplex
plain-language theorem explainer
Packages three real lifts p, q, r into the singular 2-simplex on S¹ whose continuous representative is the lift-affine (geodesic) map through the circle covering. Downstream free-chain arguments cite it as the generator of the 2-chains that witness geodesic composition in H₁. The body is a one-line transport of the concrete continuous map into Mathlib's singular simplicial set.
Claim. For $p,q,r\in\mathbb{R}$, write $F_{pqr}:\Delta^2\to S^1$ for the continuous map sending barycentric coordinates $(x_0,x_1,x_2)$ to the point on the unit circle whose lift is the affine combination $(1-x_1-x_2)p+x_1 q+x_2 r$. Then $\mathrm{linearSingularTwoSimplex}(p,q,r)$ is the corresponding singular $2$-simplex in the singular simplicial set of $S^1$.
background
The module lifts the path-level winding/displacement invariant of the circle to singular simplices of $S^1$, and proves that displacement kills boundaries: for every singular $2$-simplex $F$, the alternating face sum of displacements vanishes. That identity, with the generator sending the once-around loop to $1$, supplies the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
A singular $2$-simplex here is an element of the degree-$2$ object of Mathlib's singular simplicial set of the topological circle. The concrete continuous model is a continuous map $\Delta^2\to S^1$. The lift-affine (geodesic) map on three real lifts $p,q,r$ sends each barycentric point to $\mathrm{trigCirclePoint}$ of the corresponding affine combination; its three faces are the geodesic $1$-simplices on the three vertex pairs.
The conversion singularTwoSimplexOfMap is the inverse of Mathlib's equivalence between continuous maps $C(\Delta^2,S^1)$ and singular simplices, so the present definition is exactly that continuous geodesic $2$-simplex viewed as a singular simplex.
proof idea
One-line definitional wrapper: apply the continuous-to-singular transport to the already-constructed lift-affine continuous $2$-simplex on $(p,q,r)$. No tactics, no algebraic work; the content lives in the continuous map (affine combination of lifts, then circle covering) and in the face identities proved later for free chains built from this generator.
why it matters
This is the standard $2$-cell used to prove the geodesic composition law in free singular chains: the free boundary of the lift-affine simplex on $(p,q,r)$ equals $\mathrm{geo}(q,r)-\mathrm{geo}(p,r)+\mathrm{geo}(p,q)$, so geodesics compose additively in $H_1$. That identity is restated for free geodesic chains and specialized to the one-turn step $\partial(\mathrm{linear},0,2\pi,z+2\pi)$.
Those boundary formulas feed the geodesic winding step (shifting a terminal lift by $m$ full turns adds $m$ fundamental loops modulo an explicit $2$-boundary) and the terminal-side correction for oriented cyclic families, where lift-affine cones supply the composition-law summands of the bounding $2$-chain. In the module's program this is the concrete filler that makes winding a homology invariant on $1$-cycles, the left-inverse half of the integer comparison $H_1(S^1;\mathbb{Z})\to\mathbb{Z}$. The generation/surjectivity half still needs a simplicial prism or subdivision operator Mathlib does not yet provide.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.