coneLiftAngle_simplexEdge_two
plain-language theorem explainer
On the base edge of the standard 2-simplex cone, the lifted cone angle equals the ordinary path lift of γ. Anyone building the zero-winding cone filler for singular 1-simplices on S¹ cites this face restriction. The proof unfolds the cone formula, kills the apex coordinate, and substitutes the base-parameter identity.
Claim. For every continuous path $\gamma : I \to S^1$ and every $t \in I$, the lifted cone angle of $\gamma$ evaluated on the base edge $\delta_2$ of the standard $2$-simplex equals the canonical real path lift of $\gamma$ at $t$: $\mathrm{coneLiftAngle}(\gamma,\,\delta_2(t)) = \widetilde{\gamma}(t)$.
background
The module lifts the path-level winding/displacement invariant of the circle covering to singular simplices on $S^1$, aiming at the chain-level identity that winding kills boundaries. The key analytic object here is the cone filler for a closed edge: one cones a path $\gamma$ over the apex $v_2$ of $\Delta^2$ by radially contracting a real lift.
coneLiftAngle is that real lift on $\Delta^2$: $(1-x_2),\widetilde{\gamma}(\mathrm{coneBaseParam}(x))+x_2,\widetilde{\gamma}(0)$. The base parameter normalizes the $v_0\to v_1$ coordinate away from the apex. The geometric base edge is the face map $\delta_2:\Delta^1\to\Delta^2$, written simplexEdge 2; on that face the apex coordinate $x_2$ vanishes identically (faceMap_two_coord_two). Upstream, pathLift is the canonical continuous lift of $\gamma$ through the trigonometric covering of $S^1$, starting at the chosen initial angle.
proof idea
Unfold coneLiftAngle. First show the apex coordinate on the base edge is zero: rewrite by simplexEdge_apply and apply faceMap_two_coord_two. Next show the cone base parameter along that edge is exactly the interval parameter $t$, via coneBaseParam_simplexEdge_two_coe (after ext on the subtype). Substitute both identities into the cone formula; the prefactor $1-x_2$ becomes $1$ and the apex term drops, leaving pathLift γ t after a one-line ring.
why it matters
This is the base-face restriction step for the cone filler that witnesses zero winding of closed edges. Downstream, coneCirclePoint_simplexEdge_two pushes the identity through the covering map to conclude the pointwise cone equals $\gamma$ on the base edge; the sibling side-face identity coneCirclePoint_simplexEdge_zero_of_lift_endpoint_eq uses the same cone infrastructure under the zero-winding endpoint condition.
In the module narrative this supports the $2$-simplex telescoping that proves simplexDisplacement_boundary: alternating face displacements sum to zero. Together with the fundamental-loop normalization, that is the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The generation/surjectivity half still needs a simplicial prism operator Mathlib does not yet supply. No Recognition forcing-chain landmark (T5–T8) is invoked here; the result is pure circle topology scaffolding for the winding homomorphism.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.