coneLiftAngle_sub_start
plain-language theorem explainer
Algebraic identity for the cone-lifted angle of a path on S¹: its deviation from the apex value factors as (1−x₂) times a shifted path-lift difference. Continuity arguments at the cone apex cite this to isolate the vanishing prefactor. The proof is pure ring algebra after unfolding the cone-lift definition.
Claim. For a continuous path $\gamma:I\to S^1$ and $x$ in the standard $2$-simplex $\Delta^2$, the cone-lifted real angle at $x$ minus the path lift at the start equals $(1-x_2)$ times (the path lift at the barycentric base parameter of $x$, minus the path lift at the start).
background
The module lifts the path-level winding/displacement invariant of CircleWinding to singular simplices on $S^1$, and proves that displacement kills boundaries: the alternating face sum of any singular $2$-simplex vanishes. That identity is the chain-level fact making winding a homology invariant, and (with the generator evaluation) gives the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
Here one builds a continuous cone filler for a closed zero-winding edge. The path lift is the canonical continuous real lift of $\gamma$ through the trigonometric covering, starting at a fixed base angle. The barycentric base parameter of $x\in\Delta^2$ is $x_1/(1-x_2)$ away from the apex $v_2$, and $0$ at the apex. The cone-lifted angle is the radial contraction $(1-x_2)\cdot\mathrm{lift}(\gamma)(\mathrm{base}(x))+x_2\cdot\mathrm{lift}(\gamma)(0)$. Continuity fails naively at the apex because the base parameter jumps, but the prefactor $1-x_2$ vanishes there.
proof idea
Term proof: unfold the definition of the cone-lifted angle, then apply ring. Expanding
$(1-x_2),L(\mathrm{base}(x))+x_2,L(0)-L(0)$
and regrouping immediately yields
$(1-x_2),(L(\mathrm{base}(x))-L(0))$,
where $L$ is the path lift. No lemmas beyond the definition are required.
why it matters
This is the algebraic step that isolates the vanishing factor $1-x_2$ at the apex. The immediate parent is the uniform apex estimate: if the shifted lift is bounded by $C$, then the distance from the cone angle to the apex angle is at most $(1-x_2)C$. That squeeze estimate is what remains for the final continuity proof of the cone filler.
In the broader module story, a continuous zero-winding cone filler is the geometric ingredient that lets singular $2$-simplices telescope under displacement, proving that winding kills boundaries. Together with the evaluation of the fundamental loop, this supplies the split-injective half of the integer comparison $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The generation/surjectivity half still needs a simplicial prism or subdivision operator not yet in Mathlib.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.