coneLiftAngle_faceMap_one
plain-language theorem explainer
On the middle face δ₁ of the standard 2-simplex, the real cone-lift angle of a closed path γ on S¹ is constantly equal to the lift of γ at the initial endpoint. Anyone building the zero-winding cone filler or checking face restrictions of the cone cites this. The proof unfolds the linear cone formula, substitutes the face coordinate identity, and case-splits on the apex: either the prefactor vanishes or the base parameter is forced to 0.
Claim. Let $\gamma : I \to S^1$ be continuous and let $x \in \Delta^1 = \mathrm{stdSimplex}\,\mathbb{R}\,(\mathrm{Fin}\,2)$. Write $\delta_1 : \Delta^1 \to \Delta^2$ for the middle face inclusion. Then the cone-lift angle of $\gamma$ at $\delta_1(x)$ equals the canonical real lift of $\gamma$ evaluated at $0$: $\mathrm{coneLiftAngle}(\gamma,\delta_1(x)) = \widetilde{\gamma}(0)$.
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}$.
The cone filler is the geometric tool that contracts a closed zero-winding edge over an apex. Its real lift is $\mathrm{coneLiftAngle}(\gamma,x)=(1-x_2),\widetilde{\gamma}(\mathrm{coneBaseParam},x)+x_2,\widetilde{\gamma}(0)$, where $\widetilde{\gamma}=\mathrm{pathLift},\gamma$ is the canonical continuous lift through the trigonometric covering, and $\mathrm{coneBaseParam}$ is the barycentric base parameter $x_1/(1-x_2)$ away from the apex $v_2$ (set to $0$ at the apex).
The middle face map $\delta_1$ inserts a 1-simplex into $\Delta^2$ opposite the middle vertex. Upstream, $\mathrm{coneBaseParam_faceMap_one_coe_of_not_apex}$ already records that on this face, away from the apex, the base parameter is identically $0$ (the initial-endpoint side of the lifted cone formula).
proof idea
Unfold $\mathrm{coneLiftAngle}$. Apply $\mathrm{faceMap_one_coord_two}$ to replace coordinate $2$ of $\delta_1(x)$ by $x_1$, so the formula becomes $(1-x_1),\widetilde{\gamma}(\mathrm{coneBaseParam}(\delta_1 x))+x_1,\widetilde{\gamma}(0)$.
Case-split on $x_1=1$. If equal, the prefactor vanishes and $\mathrm{simp}$ yields $\widetilde{\gamma}(0)$. If not, invoke $\mathrm{coneBaseParam_faceMap_one_coe_of_not_apex}$ to force the base parameter to $0$ as a real, promote that equality to an equality in $I$ by $\mathrm{ext}$, substitute, and finish by $\mathrm{ring}$.
why it matters
This is the angle-level restriction of the cone filler to the middle side face $\delta_1$. Downstream, $\mathrm{coneCirclePoint_faceMap_one}$ pushes the identity through the covering map to conclude that the $S^1$-valued cone is constantly $\gamma(0)$ on that whole face: "Pointwise $S^1$ side restriction for $\delta_1$: the cone is constant on this side."
Constant side values are exactly what make the cone a legitimate singular 2-simplex filler whose boundary faces match the prescribed closed edge and the two degenerate radial edges. That filler is the geometric engine behind the 2-simplex telescoping argument in the module doc: the boundary walk is homotopic rel endpoints inside the convex $\Delta^2$, so displacement is additive and homotopy-invariant, hence kills boundaries.
In the broader Recognition foundation stack this is pure classical topology supporting the winding homomorphism on 1-cycles; it does not itself invoke the forcing chain T0–T8, but it underwrites the $H_1(S^1)\cong\mathbb{Z}$ comparison used wherever circle windings appear as discrete invariants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.