geodesicOneSimplex
plain-language theorem explainer
Geodesic singular 1-simplices on the circle are projections of straight segments in the universal cover ℝ. Given lift endpoints a and b, the map sends a point of Δ¹ to the circle point at the affine combination (1−t)a+tb. Workers of the winding-homology comparison cite this as the model edge generating free C₁. Continuity is the composite of the trigonometric covering with an affine combination of barycentric coordinates.
Claim. For $a,b\in\mathbb{R}$, the geodesic singular $1$-simplex is the continuous map $\Delta^1\to S^1$ given by $x\mapsto \gamma\bigl((1-x_1)a+x_1 b\bigr)$, where $\gamma:\mathbb{R}\to S^1$ is the standard trigonometric covering map and $x_1$ is the second barycentric coordinate on the standard topological $1$-simplex $\Delta^1=\mathrm{stdSimplex}\,\mathbb{R}\,(\mathrm{Fin}\,2)$.
background
The module lifts path-level winding and displacement from CircleWinding to singular simplices of $S^1$, and proves that displacement vanishes on boundaries. A singular $1$-simplex is a continuous map $\Delta^1\to S^1$, with $\Delta^1$ the standard topological $1$-simplex (barycentric coordinates on $\mathrm{Fin},2$). Displacement of such a simplex is path displacement after reparameterizing $\Delta^1$ to the unit interval.
The trigonometric covering $\gamma:\mathbb{R}\to S^1$ (once-around parametrization into the exact TopCat.sphere 1 object) is continuous. Lift values $a,b\in\mathbb{R}$ are points in the universal cover; their projections are the endpoints of the edge on the circle. Affine interpolation $(1-t)a+tb$ is the unique geodesic in the cover between those lifts.
Together with the kills-boundaries identity for $2$-simplices and the fact that the once-around generator has winding $1$, this apparatus supplies the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
proof idea
Definitional construction, not a deep proof. The underlying function is $\gamma\circ\ell$ where $\ell(x)=(1-x_1)a+x_1 b$. Continuity is a one-block composite: the coordinate projection $x\mapsto x_1$ is continuous on the subtype stdSimplex, affine combination of constants with that coordinate is continuous, and the trigonometric covering map is continuous by the upstream continuity theorem for the once-around parametrization. No homotopy or winding lemmas are invoked at this stage.
why it matters
Model edges for the free singular chain complex on $S^1$. Downstream, the free $C_1$ generator of a geodesic edge is built by packaging this map; the composition law for lift-affine $2$-simplices then reads $\partial,\mathrm{geo}(p,q,r)=\mathrm{geo}(q,r)-\mathrm{geo}(p,r)+\mathrm{geo}(p,q)$. The geodesic from $0$ to $2\pi$ is identified with the fundamental once-around simplex map, so the winding homomorphism hits the generator of $H_1$.
Cone constructions use it directly: the terminal-return side of a path cone equals the geodesic from the terminal lift back to the initial lift. Shift invariance (adding $2\pi m$ to both endpoints) and the constant-edge case $a=a$ are immediate specializations. In the Recognition foundation stack this is the concrete singular model behind the winding invariant that splits the integer comparison map on $H_1(S^1)$, the topological half of the eight-tick / circle story (T7) rather than a forcing-chain step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.