coneTerminalSideLift_lifts
plain-language theorem explainer
The explicit real lift of the cone's terminal-return side, composed with the trigonometric covering of the circle, recovers the path of that singular 1-simplex. Anyone computing path displacement of cone faces cites this to justify the closed-form lift. The proof is a pointwise identity: unfold the four definitions and apply the second-coordinate lemma for the interval-to-simplex homeomorphism.
Claim. For every continuous path $\gamma : I \to S^1$, writing $\widetilde{\gamma}$ for a real lift of $\gamma$, the composition of the trigonometric covering $t \mapsto (\cos 2\pi t, \sin 2\pi t)$ with the affine real path $t \mapsto (1-t)\widetilde{\gamma}(1)+t\widetilde{\gamma}(0)$ equals the path obtained by reparameterizing the terminal-return singular $1$-simplex of the cone over $\gamma$ along the standard homeomorphism $I \simeq \Delta^1$.
background
This module lifts the path-level winding/displacement invariant on $S^1$ to singular simplices of $\mathrm{TopCat.sphere},1$ and proves the chain-level fact that displacement kills boundaries. Displacement of a singular $1$-simplex is path displacement after reparameterizing $\Delta^1$ onto the unit interval.
The cone over a path $\gamma$ has three sides. The terminal-return side is the singular $1$-simplex that, in covering coordinates, runs affinely from the lifted endpoint $\widetilde{\gamma}(1)$ back to $\widetilde{\gamma}(0)$. Its explicit real lift is the continuous map $t \mapsto (1-t)\widetilde{\gamma}(1)+t\widetilde{\gamma}(0)$. The map $\mathrm{trigCirclePoint}$ is the once-around trigonometric parametrization into the exact sphere object. The reparameterization $I\to\Delta^1$ is $t\mapsto(1-t,t)$, inverse to Mathlib's stdSimplexHomeomorphUnitInterval.
Upstream, the covering is known to be surjective onto the sphere carrier, and the second barycentric coordinate of the homeomorphism inverse is exactly the interval parameter.
proof idea
Term proof by functional extensionality on $t\in I$. Unfold the definitions of the real lift, the simplex-to-path conversion, the cone terminal side, and the interval-to-simplex map. The remaining identity is that the second barycentric coordinate of $\mathrm{stdSimplexHomeomorphUnitInterval.symm}(t)$ equals $t$, which is exactly the coordinate lemma for that homeomorphism. No homotopy or covering theory is invoked.
why it matters
Feeds the theorem that the terminal-return cone side has path displacement opposite the base path. That sign reversal is part of the cone calculus underlying the kills-boundaries identity: for every singular $2$-simplex the alternating face sum of displacements vanishes. Together with the evaluation of the once-around generator, this supplies the injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ (the infinite-order class on integer multiples of the fundamental loop). The generation/surjectivity half remains open, pending a simplicial prism or subdivision operator that Mathlib's singular homology does not yet provide. No Recognition-physics constants are involved; this is pure foundation for the winding homomorphism.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.