linearTwoSimplexMap
plain-language theorem explainer
Defines the lift-affine singular 2-simplex on S¹: barycentric coordinates on Δ² are sent to the trig circle point of the affine combination of three real lifts p, q, r. Anyone building geodesic faces or the free boundary geo(q,r)−geo(p,r)+geo(p,q) cites it. Continuity is pure composition of barycentric projections with continuous_trigCirclePoint.
Claim. For $p,q,r\in\mathbb{R}$, there is a continuous map $\Delta^2\to S^1$ given by $x\mapsto \gamma\bigl((1-x_1-x_2)p+x_1 q+x_2 r\bigr)$, where $\gamma$ is the standard trigonometric parametrization of the unit circle and $x_i$ are barycentric coordinates on the standard $2$-simplex.
background
The module lifts path-level winding/displacement on $S^1$ to singular simplices and proves that displacement vanishes on boundaries: for every singular $2$-simplex $F$, $\mathrm{disp}(\partial_0 F)-\mathrm{disp}(\partial_1 F)+\mathrm{disp}(\partial_2 F)=0$. That identity, with the generator evaluation, supplies the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
A TwoSimplex is a continuous map $C(\Delta^2,S^1)$ with $\Delta^2=\mathrm{stdSimplex},\mathbb{R},(\mathrm{Fin},3)$. The map trigCirclePoint is the once-around trigonometric parametrization into Mathlib's exact TopCat.sphere 1; its continuity is already proved upstream.
The construction is geodesic in the cover: lifts $p,q,r\in\mathbb{R}$ are combined affinely on $\Delta^2$, then projected. Faces of such maps are the geodesics on the three vertex pairs.
proof idea
Definition with a continuity obligation. Extract continuous coordinate projections $x\mapsto x_1$ and $x\mapsto x_2$ from the subtype of the standard simplex, form the affine combination $(1-x_1-x_2)p+x_1 q+x_2 r$ by field operations (all continuous), and compose with continuous_trigCirclePoint. No topology beyond composition of continuous maps is used.
why it matters
This is the concrete carrier for geodesic $2$-chains in the circle winding calculus. Downstream, linearSingularTwoSimplex packages it as a singular simplex; the three face lemmas identify $\partial_0$, $\partial_1$, $\partial_2$ with geodesics $q\to r$, $p\to r$, $p\to q$. Those feed the geodesic composition law: the free boundary is $\mathrm{geo}(q,r)-\mathrm{geo}(p,r)+\mathrm{geo}(p,q)$.
That law is the chain-level engine behind telescoping and the kills-boundaries identity in the module doc. In the broader Recognition foundation it supports the winding homomorphism as a left inverse to the fundamental class on $H_1(S^1)$, the split-injective half of the integer comparison. The generation/surjectivity half still needs a simplicial prism operator Mathlib does not yet supply.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.