coneTerminalSide_eq_constantOneSimplex_of_simplexWinding_zero
plain-language theorem explainer
Zero winding of a singular 1-simplex on the circle forces the terminal-return side of its cone to equal the constant apex edge. Algebraic topologists building the winding homomorphism on singular chains of S¹ cite this when collapsing cone boundaries. The proof rewrites simplex winding to path winding, gets equal lift endpoints, then applies the lift-endpoint form of the same identity.
Claim. Let $f:\Delta^1\to S^1$ be a singular $1$-simplex with winding number zero. Then the terminal-return side of the cone over the path associated to $f$ equals the constant singular $1$-simplex based at that path's initial point.
background
The module lifts the path-level winding invariant of CircleWinding to singular simplices of $S^1$ and proves that winding kills boundaries, the chain-level fact needed for a homology invariant. A singular $1$-simplex is a continuous map $f:\Delta^1\to S^1$; reparameterizing $\Delta^1$ to the unit interval yields a path, and the simplex winding is the path winding (displacement divided by $2\pi$).
The cone over a path $\gamma$ has a concrete terminal-return side: on $\Delta^1$ it evaluates the covering exponential at the linear blend $(1-t),\widetilde{\gamma}(1)+t,\widetilde{\gamma}(0)$ of the canonical real lift endpoints. When those endpoints coincide, that side is literally the constant apex edge. Upstream, zero path winding already forces $\widetilde{\gamma}(1)=\widetilde{\gamma}(0)$ ("lift-level form consumed by the singular cone construction").
proof idea
Two short steps. First, rewrite the hypothesis simplexWinding f = 0 through the definitions of simplex displacement and path winding to obtain pathWinding of the associated path equal to zero; apply pathLift_endpoint_eq_of_winding_zero to conclude the canonical lift endpoints agree. Second, feed that endpoint equality into the already-proved companion coneTerminalSide_eq_constantOneSimplex_of_lift_endpoint_eq, which is exactly the same geometric claim stated at the lift level rather than the winding level.
why it matters
This is the winding-specialized form of the cone side identity used by singularTwoBoundaryFree_freeMk_coneCircleMap_of_simplexWinding_zero: "the terminal-return side equals the constant apex side, so the cone's free boundary is just the original edge generator." That parent theorem is the zero-winding case of the free boundary shell for the cone $2$-simplex, needed when building a chain homotopy that kills null-winding edges.
In the module's larger program, winding on $1$-cycles is a left inverse to the fundamental class (via pathWinding_fundamentalLoop), giving the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. Collapsing the terminal side of null-winding cones is a local geometric ingredient of that comparison. The generation (surjectivity) half still needs a simplicial prism or subdivision operator that Mathlib singular homology does not yet supply; this lemma does not touch that gap.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.