coneCircleMapOfContinuous_side_faces_eq_of_winding_zero
plain-language theorem explainer
For a singular 1-simplex on S¹ with vanishing winding, once the pointwise cone map is continuous it packages as a singular 2-simplex whose two side faces coincide. Anyone building the cone filler for zero-winding closed 1-cycles cites this face identity. The proof is a pointwise extension of the already-proved cone-point side-face equality.
Claim. Let $f:\Delta^1\to S^1$ be a singular $1$-simplex with simplex winding $0$. If the pointwise cone map associated to the unit-interval reparameterisation of $f$ is continuous, then the $0$-th and $1$-st faces of the resulting singular $2$-simplex are equal as maps $\Delta^1\to S^1$.
background
This module lifts path-level winding on $S^1$ to singular simplices and proves that displacement kills boundaries, the chain-level fact behind the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. A singular $1$-simplex is a continuous map $\Delta^1\to S^1$; its winding is the path winding of the unit-interval reparameterisation. Faces of a singular $2$-simplex $F$ are the composites $F\circ\mathrm{faceMap}_i$.
The pointwise cone coneCirclePoint sends a path $\gamma:I\to S^1$ and a point of $\Delta^2$ to an $S^1$ value by projecting a lifted cone angle through the circle cover. Packaging that pointwise map as a genuine singular $2$-simplex requires continuity (especially at the apex); coneCircleMapOfContinuous isolates exactly that analytic obligation. Upstream, the zero-winding form of the pointwise side-face identity already equates the two lateral cone values on $\Delta^1$ whenever path winding vanishes.
proof idea
Term-mode, essentially a one-line wrapper. Extensionality on the two faces (as continuous maps $\Delta^1\to S^1$) reduces the claim to a pointwise equality. That equality is exactly coneCirclePoint_side_faces_eq_of_winding_zero applied to the unit-interval path of $f$, the zero-winding hypothesis, and the evaluation point. Continuity is only used to form the packaged $2$-simplex; the face comparison itself is inherited from the pointwise cone.
why it matters
Parent consumer is closedSingularOneCycle_bounds_of_continuous_coneCirclePoint, the continuity-hypothesis form of the closed-edge cone filler: after the pointwise face identities, a continuous zero-winding cone supplies a singular $2$-chain whose boundary is the closed $1$-cycle. Matching the two side faces is the geometric step that cancels the lateral edges, leaving only the base contribution needed for a genuine bounding chain.
In the module narrative this sits inside the "winding kills boundaries / cone filler" half of the $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ comparison: winding is already a left inverse to the fundamental class, and zero-winding closed simplices must bound. The remaining analytic gate is continuity of the cone at the apex; this lemma converts that gate into the side-face algebra the boundary computation needs. No forcing-chain landmark (T5–T8) is directly invoked; the result is pure singular-homology infrastructure for the circle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.