geodesicOneSimplex_apply
plain-language theorem explainer
At a point x of the standard 1-simplex, the geodesic singular 1-simplex from lift values a to b is the trigonometric circle point at the affine combination (1−x₁)a + x₁ b. Anyone computing faces of lift-affine 2-simplices or identifying the once-around generator cites this. The proof is pure definitional equality (rfl), marked @[simp].
Claim. For $a,b\in\mathbb{R}$ and $x\in\Delta^1=\mathrm{stdSimplex}\,\mathbb{R}\,(\mathrm{Fin}\,2)$, the geodesic singular $1$-simplex from lift $a$ to lift $b$ satisfies $f_{a,b}(x)=\gamma\bigl((1-x_1)a+x_1 b\bigr)$, where $\gamma$ is the standard trigonometric parametrization $\mathbb{R}\to S^1$.
background
The module lifts path-level winding on $S^1$ to singular simplices and proves that displacement kills 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 once-around generator mapping to $1$, gives the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
A geodesic singular $1$-simplex is the projection of the straight line in the universal cover $\mathbb{R}\to S^1$ joining lift values $a$ and $b$. Concretely its underlying map sends $x\in\Delta^1$ to the trigonometric circle point at the convex combination $(1-x_1)a+x_1 b$. The trigonometric point map is the once-around parametrization into the exact TopCat.sphere 1 object.
The standard $1$-simplex is coordinatized by barycentric weights on $\mathrm{Fin},2$; the second coordinate $x_1$ runs the affine parameter from the initial to the terminal vertex.
proof idea
One-line definitional proof: rfl. The statement is exactly the toFun clause in the definition of the geodesic singular $1$-simplex, so evaluation unfolds by construction. Marked @[simp] so face and endpoint lemmas can rewrite through it automatically.
why it matters
This simp lemma is the evaluation interface for every geodesic edge used in the chain-level winding argument. Downstream it powers: constant-edge identification when endpoints coincide; $2\pi\mathbb{Z}$-shift invariance of geodesics; the identification of the geodesic from $0$ to $2\pi$ with the fundamental once-around simplex map; and the three face theorems for the lift-affine $2$-simplex ($\delta_0$, $\delta_1$, $\delta_2$ faces equal the geodesics on the corresponding vertex pairs).
Those face identities feed the $2$-simplex telescoping that proves displacement kills boundaries, the key homology-invariance step toward $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. In the Recognition foundation this is pure topological scaffolding for circle winding, not a forcing-chain (T0–T8) step, but it underwrites the singular-homology half of the winding invariant used elsewhere in the circle-lifting development.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.