oneSimplexPath_fundamental
plain-language theorem explainer
The fundamental singular 1-simplex on S¹, reparameterised from Δ¹ to the unit interval, equals the standard once-around loop. Anyone computing simplex displacement or the winding left-inverse on H₁(S¹) cites this identification. The proof is pointwise: both sides are trigCirclePoint of 2π times the second barycentric coordinate, which is just t.
Claim. Reading the fundamental singular $1$-simplex $f:\Delta^1\to S^1$ (angle $2\pi$ times the second barycentric coordinate) as a path on the unit interval via $t\mapsto(1-t,t)$ yields exactly the fundamental once-around loop $\gamma(t)=(\cos 2\pi t,\sin 2\pi t)$ on $S^1$.
background
The module lifts path-level winding from CircleWinding to singular 1-simplices of $S^1$, so that displacement becomes a homology invariant. A singular 1-simplex is a continuous map $f:\Delta^1\to S^1$. The map oneSimplexPath composes $f$ with the standard homeomorphism $I\simeq\Delta^1$, $t\mapsto(1-t,t)$, producing a path $I\to S^1$.
The fundamental singular 1-simplex sends a point of $\Delta^1$ to the circle point at angle $2\pi$ times its second barycentric coordinate, so endpoints sit at angles $0$ and $2\pi$. The fundamental loop is the same trigonometric path written directly on $I$: $t\mapsto$ the sphere point at angle $2\pi t$. The second barycentric coordinate of $(1-t,t)$ is exactly $t$, which is the algebraic content of the coordinate lemma used below.
proof idea
Pointwise equality of continuous maps $I\to S^1$. After ext t, both sides reduce to trigCirclePoint applied to $2\pi$ times a real parameter: the left uses the second barycentric coordinate of intervalToSimplex t, the right uses $t$ itself. Rewrite by intervalToSimplex_coord_one, which is definitional (rfl): that coordinate equals $(t:\mathbb{R})$. No homotopy or winding arithmetic is needed.
why it matters
This is the bridge from the simplex presentation of the generator to the path-level fundamental loop. Downstream, simplexDisplacement_fundamental rewrites displacement of the fundamental singular 1-simplex through this identity and pathDisplacement_fundamentalLoop, obtaining displacement $2\pi$ (winding $1$).
That fact is the left-inverse half of the integer comparison $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$: winding sends the fundamental class to $1$. Together with the kills-boundaries identity for 2-simplices in this module, it makes simplex displacement a well-defined homomorphism on 1-cycles. The generation/surjectivity half still needs a prism or subdivision operator that Mathlib singular homology does not yet supply. No RS forcing-chain step (T0–T8) is invoked; the result is pure circle topology supporting the winding invariant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.