coneCircleMapOfContinuous
plain-language theorem explainer
Packages a continuous path on the circle into a singular 2-simplex once the pointwise cone map is known to be continuous. Anyone building cone fillers for zero-winding edges on S¹ cites this packaging step. The body is a ContinuousMap constructor: the underlying function is the pointwise cone, and the continuity field is the supplied hypothesis.
Claim. Given a continuous path $\gamma : I \to S^1$ and a proof that the pointwise cone map $x \mapsto \mathrm{trig}(\mathrm{coneLiftAngle}(\gamma,x))$ is continuous on the standard $2$-simplex $\Delta^2$, obtain the singular $2$-simplex $C(\Delta^2,S^1)$ whose underlying function is that cone.
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$, the alternating face sum of displacements vanishes. That identity, with the generator evaluation, supplies the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
A singular $2$-simplex here is a continuous map $\Delta^2\to S^1$, where $\Delta^2=\mathrm{stdSimplex},\mathbb{R},(\mathrm{Fin},3)$. The pointwise cone sends each barycentric point $x\in\Delta^2$ to the circle point obtained by projecting a lifted cone angle of $\gamma$ through the trigonometric cover. That construction is not yet a ContinuousMap; continuity at the apex is the remaining analytic obligation.
Faces of a $2$-simplex are obtained by precomposition with the topological face inclusions $\Delta^1\to\Delta^2$ (skipping one vertex).
proof idea
One-line ContinuousMap packaging. The underlying function field is set to the pointwise cone of $\gamma$; the continuity field is filled by the hypothesis that this pointwise map is continuous on $\Delta^2$. No further lemmas are applied.
why it matters
Isolates the sole analytic gap before cone fillers become singular chains: continuity of the pointwise cone at the apex. Downstream face lemmas read off the three faces of this packaged simplex (base face recovers the original edge; $\delta_1$ is the constant apex edge; $\delta_0$ is the terminal-return side). With zero winding, the two side faces agree, so they cancel in the boundary.
The parent theorem closedSingularOneCycle_bounds_of_continuous_coneCirclePoint uses this packaging to turn a closed zero-winding edge into a singular $2$-chain whose boundary is that edge, once continuity is assumed. That is the continuity-hypothesis form of the closed-edge cone filler needed for the generation half of the $H_1(S^1)$ comparison (prism/subdivision still open in Mathlib). In the Recognition foundation stack this is pure singular-homology infrastructure for the circle winding invariant, not a physics forcing step (T0–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.