coneLiftAngle_simplexEdge_one
plain-language theorem explainer
On the δ₁ face of the standard 2-simplex, the real cone-lift angle of a path γ on S¹ is constantly the initial lift value pathLift(γ)(0). Anyone building the zero-winding cone filler or checking face restrictions of the cone map cites this. The proof unfolds the linear cone formula, identifies the apex coordinate with t, and case-splits on the apex: either the base parameter collapses by definition or it is forced to 0, so the convex combination is constant.
Claim. For every continuous path $\gamma : I \to S^1$ and every $t \in I$, the lifted cone angle of $\gamma$ evaluated on the $\delta_1$ edge of the standard $2$-simplex equals the initial value of the canonical real lift of $\gamma$: $\mathrm{coneLiftAngle}(\gamma,\,\delta_1(t)) = \widetilde{\gamma}(0)$.
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$, $\mathrm{disp}(\delta_0 F)-\mathrm{disp}(\delta_1 F)+\mathrm{disp}(\delta_2 F)=0$. That identity is the chain-level half of the split injection $H_1(S^1;\mathbb{Z})\hookrightarrow\mathbb{Z}$.
Here one builds an explicit cone filler for a closed zero-winding edge. The barycentric base parameter $\mathrm{coneBaseParam}$ is $x_1/(1-x_2)$ away from the apex $v_2$ and $0$ at the apex. The lifted cone angle is the radial contraction $\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 of $S^1$.
Upstream, $\mathrm{coneBaseParam}$ on the $\delta_1$ face is $0$ away from the apex, and the face-coordinate lemmas identify the apex weight on $\delta_1(t)$ with $t$ itself.
proof idea
Unfold the definition of the lifted cone angle. First rewrite the apex coordinate: on $\mathrm{simplexEdge},1,t$ one has $x_2=t$, via $\mathrm{simplexEdge_apply}$, $\mathrm{faceMap_one_coord_two}$, and $\mathrm{intervalToSimplex_coord_one}$.
Case on whether $t=1$. At the apex, substitute $t=1$ and simplify with the apex clause of $\mathrm{coneBaseParam}$; both weights collapse to the constant $\widetilde{\gamma}(0)$.
Off the apex, apply $\mathrm{coneBaseParam_faceMap_one_coe_of_not_apex}$ to force the base parameter to $0$ on $\delta_1$. The formula becomes $(1-t)\widetilde{\gamma}(0)+t\widetilde{\gamma}(0)$, which rings to $\widetilde{\gamma}(0)$.
why it matters
This is the angle-level constancy statement on the $\delta_1$ side of the zero-winding cone. Its sole downstream consumer is $\mathrm{coneCirclePoint_simplexEdge_one}$, which pushes the same identity through the covering map to conclude that the pointwise cone is constantly $\gamma(0)$ on that face.
Facewise control of the cone is required before one can assemble a continuous singular $2$-simplex filler and feed it into the telescoping argument of $\mathrm{simplexDisplacement_boundary}$. That boundary-vanishing theorem, together with the normalization that the fundamental loop has winding $1$, supplies the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ in the Recognition foundation stack. The generation/surjectivity half remains open pending a simplicial prism or subdivision operator not yet in Mathlib.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.