coneLiftAngle_faceMap_two
plain-language theorem explainer
On the base face δ₂ of Δ², the radially contracted cone angle for a path γ on S¹ collapses exactly to the ordinary path lift of γ. Anyone building the zero-winding cone filler or checking face restrictions of singular cones cites this. The proof unfolds the cone formula, uses that the apex coordinate vanishes on δ₂, and rewrites the base parameter as the standard Δ¹≃I homeomorphism, finishing by ring.
Claim. For every continuous path $\gamma:I\to S^1$ and every point $x$ of the standard $1$-simplex $\Delta^1$, the cone lift angle of $\gamma$ evaluated on the image of $x$ under the face map $\delta_2:\Delta^1\to\Delta^2$ equals the canonical real path lift of $\gamma$ at the unit-interval parameter of $x$.
background
The module lifts the path-level winding/displacement invariant of CircleWinding to singular simplices on $S^1$, aiming at the chain-level identity that displacement kills boundaries: for every singular $2$-simplex $F$, $\mathrm{disp}(\delta_0 F)-\mathrm{disp}(\delta_1 F)+\mathrm{disp}(\delta_2 F)=0$. That identity, with the generator evaluation, supplies the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
Here one works with an auxiliary cone construction that fills a closed zero-winding edge. The cone lift angle is the real-valued map $(1-x_2)\cdot\mathrm{pathLift}(\gamma)(\mathrm{coneBaseParam}(x))+x_2\cdot\mathrm{pathLift}(\gamma)(0)$, radially contracting the lifted edge toward the apex $v_2$. The base parameter $\mathrm{coneBaseParam}$ is the normalized barycentric coordinate $x_1/(1-x_2)$ along $v_0\to v_1$ (set to $0$ at the apex). The face map $\delta_2$ embeds $\Delta^1$ as the base edge opposite $v_2$, forcing the apex coordinate to vanish.
Upstream, $\mathrm{pathLift}$ is the canonical continuous lift of $\gamma$ through the trigonometric covering of $S^1$, and $\mathrm{coneBaseParam}\circ\delta_2$ is already known to recover the original $\Delta^1$ coordinate.
proof idea
Unfold the definition of the cone lift angle. Invoke the face-coordinate lemma that the apex slot of $\delta_2(x)$ is identically $0$. Separately, the coe-level identity $\mathrm{coneBaseParam}(\delta_2(x))=\mathrm{stdSimplexHomeomorphUnitInterval}(x)$ is obtained by ext from the already-proved real equality on the base face. Rewrite with those two facts; the prefactor $1-x_2$ becomes $1$ and the apex term drops, leaving exactly $\mathrm{pathLift},\gamma$ at the unit-interval parameter. Close with ring.
why it matters
This is the angle-level base-face restriction needed before projecting back to $S^1$. Its sole downstream consumer is the pointwise statement that the cone circle-point on $\delta_2$ recovers the original singular edge of $\gamma$. That face agreement is part of verifying that the cone filler is a genuine singular $2$-simplex whose boundary edges match the prescribed zero-winding loop, which in turn supports the telescoping argument behind $\mathrm{simplexDisplacement_boundary}$.
In the broader Recognition foundation stack this sits inside the purely topological half of the circle-winding chain: no RS constants, $\phi$-ladder, or forcing steps T0–T8 appear. The open generation half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ (every $1$-cycle homologous to an integer multiple of the fundamental cycle) still needs a simplicial prism/subdivision operator that Mathlib does not yet supply; the present lemma does not touch that gap.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.