coneCirclePoint_faceMap_zero_of_lift_endpoint_eq
plain-language theorem explainer
When a circle path has equal lifted endpoints, the pointwise S¹ cone is constantly the path start on the entire δ₀ face. Homology workers cite this when matching side faces of a cone filler. The proof unfolds the cone, rewrites by the lifted-angle face constancy lemma, and projects via the covering identity.
Claim. Let $\gamma:I\to S^1$ be continuous. If the canonical real lift of $\gamma$ satisfies $\widetilde{\gamma}(1)=\widetilde{\gamma}(0)$, then for every $x$ in the standard $1$-simplex, the pointwise cone of $\gamma$ at the $0$-th face of $x$ equals $\gamma(0)$.
background
The module lifts the path-level winding/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 $F$, $\mathrm{disp}(\delta_0 F)-\mathrm{disp}(\delta_1 F)+\mathrm{disp}(\delta_2 F)=0$. That identity, with the generator sending the once-around loop to $1$, supplies the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
The covering $\mathbb{R}\to S^1$ is the trigonometric map. The canonical continuous lift pathLift $\gamma$ starts at a fixed angle and satisfies $\mathrm{trig}\circ\widetilde{\gamma}=\gamma$. The pointwise cone coneCirclePoint $\gamma$ on the standard $2$-simplex is $\mathrm{trig}$ of a lifted cone angle built from that path lift. Face maps $\delta_i:\Delta^1\to\Delta^2$ select the three edges of $\Delta^2$; the $0$-th face is the terminal-return side of the cone.
Upstream, coneLiftAngle_faceMap_zero_of_lift_endpoint_eq already shows the lifted cone angle is constant and equal to $\widetilde{\gamma}(0)$ on the whole $\delta_0$ face once the lifted endpoints agree.
proof idea
Term-mode, three steps. Unfold coneCirclePoint to $\mathrm{trig}\circ\mathrm{coneLiftAngle}$. Rewrite the angle on $\delta_0$ by coneLiftAngle_faceMap_zero_of_lift_endpoint_eq, which under equal lifted endpoints gives the constant value $\widetilde{\gamma}(0)$. Finish with congrFun (pathLift_lifts $\gamma$) 0, i.e. $\mathrm{trig}(\widetilde{\gamma}(0))=\gamma(0)$.
why it matters
Immediate parent is coneCirclePoint_side_faces_eq_of_lift_endpoint_eq: the two side faces of the pointwise cone agree once lifted endpoints match, the pointwise form of the future face equation $\mathrm{face},F,0=\mathrm{face},F,1$. That side-face equality is scaffolding toward a continuous cone filler whose boundary faces cancel in the winding chain complex.
In the module arc this supports the kills-boundaries identity for simplexDisplacement, hence the winding homomorphism on $1$-cycles that left-inverts the fundamental class. The generation/surjectivity half still needs a simplicial prism or subdivision operator Mathlib singular homology does not yet supply. No RS forcing-chain landmark (T5–T8, RCL, $\varphi$) is touched here; the result is pure $S^1$ covering and singular-simplex geometry inside the Foundation layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.