coneLiftAngle_faceMap_two_of_oneSimplex
plain-language theorem explainer
On the base face δ₂ of the standard 2-simplex, the radially contracted cone lift angle of a singular 1-simplex equals the ordinary path lift after the standard Δ¹ ≃ I homeomorphism. Anyone building the zero-winding cone filler or checking face restrictions of the cone map cites this. The proof unfolds the cone formula, substitutes the vanishing apex coordinate and the base-parameter identity, then simplifies by ring.
Claim. Let $f$ be a singular $1$-simplex on $S^1$ (a continuous map $\Delta^1\to S^1$) and let $x\in\Delta^1$. On the base face $\delta_2:\Delta^1\to\Delta^2$, the cone lift angle of the path associated to $f$ at $\delta_2(x)$ equals the ordinary covering-space path lift of that path evaluated at the image of $x$ under the standard homeomorphism $\Delta^1\simeq I$.
background
This module lifts the path-level winding and displacement invariant of CircleWinding to singular simplices of $S^1$, aiming at the chain-level identity that displacement kills boundaries: for every singular $2$-simplex the alternating face sum of displacements vanishes. That identity, with the generator evaluation, supplies the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
A singular $1$-simplex is a continuous map $\Delta^1=\mathrm{stdSimplex},\mathbb{R}(\mathrm{Fin},2)\to S^1$. Face maps $\delta_i:\Delta^1\to\Delta^2$ are the affine coface embeddings. The cone base parameter on $\Delta^2$ is the normalized barycentric coordinate along the base edge $v_0\to v_1$ (value $x_1/(1-x_2)$ away from the apex $v_2$, and $0$ at the apex). The cone lift angle contracts the covering lift of a closed edge radially toward the apex: $(1-x_2)\cdot\mathrm{pathLift}(\gamma)(\mathrm{coneBaseParam},x)+x_2\cdot\mathrm{pathLift}(\gamma)(0)$.
Upstream, pathLift is the canonical continuous lift of a path on $S^1$ through the exponential covering. The companion lemma coneBaseParam_faceMap_two_coe states that on $\delta_2$ the cone base parameter recovers the original $\Delta^1$ coordinate.
proof idea
Tactic proof. Unfold the definition of the cone lift angle. Invoke faceMap_two_coord_two to obtain that the apex coordinate of $\delta_2(x)$ is $0$. Separately, show by ext and coneBaseParam_faceMap_two_coe that the cone base parameter of $\delta_2(x)$ equals the standard homeomorphism $\Delta^1\simeq I$ applied to $x$. Rewrite both facts into the unfolded formula; the prefactor $1-x_2$ becomes $1$ and the apex term drops, leaving exactly pathLift of the associated path at that interval point. Finish with ring.
why it matters
The cone filler is the geometric device that exhibits a zero-winding closed edge as a boundary in the singular chain complex of $S^1$. Restricting the lifted angle to the base face must recover the original edge lift; otherwise the filler would not glue to the given $1$-simplex. This theorem is the angle-level half of that restriction.
It feeds directly into coneCirclePoint_faceMap_two_of_oneSimplex, whose doc-comment records the pointwise claim: after projection to $S^1$, the base face of the cone is exactly the original singular edge. That pointwise identity is the last algebraic step before the cone can be used inside the telescoping argument for simplexDisplacement_boundary (the kills-boundaries identity of the module).
In the broader Recognition foundation this sits in the topological half of the forcing chain: establishing $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ by an explicit winding left-inverse, without axioms or project-local circle replacements. The generation (surjectivity) half remains open pending a simplicial prism or subdivision operator that Mathlib singular homology does not yet supply.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.