coneLiftAngle
plain-language theorem explainer
Defines the real-valued lifted cone angle on the standard 2-simplex for a path on S¹: a radial contraction of the path lift toward the apex value. Anyone constructing the zero-winding cone filler, or checking its face restrictions, cites this. The body is a one-line barycentric combination of the canonical path lift with the base parameter.
Claim. For a continuous path $\gamma:I\to S^1$ and $x\in\Delta^2=\mathrm{stdSimplex}\,\mathbb{R}\,(\mathrm{Fin}\,3)$, the lifted cone angle is $(1-x_2)\,\widetilde{\gamma}(b(x))+x_2\,\widetilde{\gamma}(0)$, where $\widetilde{\gamma}$ is the canonical continuous real lift of $\gamma$ starting at its prescribed lift-start, and $b(x)$ is the barycentric base parameter ($x_1/(1-x_2)$ off the apex, $0$ at the apex).
background
The module lifts the path-level winding/displacement invariant of CircleWinding to singular simplices of $S^1$, aiming at the chain-level identity that displacement kills boundaries of 2-simplices. That identity, with the generator evaluation, supplies the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
The canonical path lift $\widetilde{\gamma}:I\to\mathbb{R}$ is the continuous lift through the trigonometric covering of $S^1$, started at the designated lift-start. The barycentric base parameter $b(x)$ on $\Delta^2$ is $x_1/(1-x_2)$ away from the apex $v_2$ (where $x_2=1$) and is set to $0$ at the apex; it is discontinuous at the apex by itself.
The cone filler for a closed zero-winding edge needs a real angle that contracts the lifted edge radially to the apex value. Multiplying the (discontinuous) base evaluation by the vanishing factor $1-x_2$ is the standard fix that restores continuity at the apex once proved.
proof idea
Pure definition: evaluate the path lift of $\gamma$ at the barycentric base parameter of $x$, weight by $1-x_2$, and add the apex weight $x_2$ times the lift at $0$. No lemmas are applied; the formula is the radial contraction written in barycentric coordinates.
why it matters
This is the real-angle skeleton of the cone filler. Downstream, projecting through the circle cover yields the pointwise $S^1$ cone; face-restriction lemmas then show the lifted angle is constant on the side faces (once endpoints match) and recovers the lifted path on the base face. Those identities are the combinatorial input to packaging a continuous singular 2-simplex that fills a zero-winding closed edge.
In the module narrative, such fillers underwrite the homology invariance of simplex displacement (winding kills boundaries), which with the once-around generator gives the left-inverse half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The remaining hard analysis flagged in the doc is continuity of this angle at the apex: $b(x)$ jumps, but $1-x_2$ vanishes. No Recognition forcing-chain landmark (T5–T8, RCL) is touched directly; the work is classical singular-homology infrastructure for the circle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.