coneCircleMapOfContinuous_face_two
plain-language theorem explainer
If the pointwise zero-winding cone over a singular 1-edge on S¹ is continuous, then the base face (index 2) of the packaged singular 2-simplex recovers that edge exactly. Homology and chain-level arguments that build cone fillers for zero-winding loops cite this face identity. The proof is an extensionality reduction to the already-proved pointwise base-face restriction.
Claim. Let $f:\Delta^1\to S^1$ be a singular $1$-simplex, and write $\gamma$ for the corresponding path on the unit interval. If the pointwise cone map $x\mapsto\mathrm{coneCirclePoint}(\gamma)(x)$ on $\Delta^2$ is continuous, then the face of index $2$ of the singular $2$-simplex it defines equals $f$.
background
The module lifts path winding and displacement from CircleWinding to singular simplices of $S^1$, aiming at the chain-level identity that displacement kills boundaries of singular $2$-simplices. A singular $1$-simplex is a continuous map $\Delta^1\to S^1$; reading it through the standard homeomorphism $\Delta^1\simeq I$ yields a path. Faces of a singular $2$-simplex $F:\Delta^2\to S^1$ are the three edge restrictions $F\circ\mathrm{faceMap}_i$.
The cone construction builds a candidate $2$-simplex filler over a path by lifting angles, coning in the cover, and projecting back to $S^1$ via coneCirclePoint. Continuity at the apex is isolated as a separate analytic hypothesis; once assumed, coneCircleMapOfContinuous packages the pointwise cone as a concrete singular $2$-simplex. Upstream, the pointwise identity coneCirclePoint_faceMap_two_of_oneSimplex already says that restricting that cone along face map $2$ recovers the original edge at every point of $\Delta^1$.
proof idea
After ext x on the equality of continuous maps $\Delta^1\to S^1$, the goal is pointwise. It is discharged by the upstream lemma coneCirclePoint_faceMap_two_of_oneSimplex, which equates the cone evaluated on the geometric face map of index $2$ with the original singular edge. No further continuity or homotopy reasoning appears here: the packaging definition only supplies the continuous map whose underlying function is already the cone, so face restriction reduces to that pointwise fact.
why it matters
This is one of the face identities needed to compute the singular boundary of the cone filler. Downstream, singularTwoBoundaryFree_freeMk_coneCircleMap uses the packaged cone and records that its free boundary is terminal-return minus constant apex plus the original edge; the base-face clause is exactly this theorem. The closed-edge case closedSingularOneCycle_bounds_of_continuous_coneCirclePoint then specialises under endpoint matching and zero winding, turning continuity of the cone into a genuine $2$-chain bound for a closed zero-winding $1$-cycle.
In the module narrative, that bound is the remaining analytic step toward the "winding kills boundaries" half of the comparison $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$, complementing simplexDisplacement_boundary and the generator evaluation on the fundamental loop. It does not itself touch the RS forcing chain (T5–T8) or the Recognition Composition Law; it sits in the topological foundation that underwrites circle invariants used later in the monolith.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.