coneCirclePoint
plain-language theorem explainer
Pointwise conical filler on the standard 2-simplex valued in S¹: given a continuous loop γ on the circle and barycentric coordinates x, return the circle point whose covering angle is the radial contraction of a lift of γ toward the apex. Cited wherever a zero-winding closed edge must be filled by a singular 2-simplex. Definition is a one-line composition of the trigonometric cover with the real cone-lift angle.
Claim. For a continuous path $\gamma : I \to S^1$ and a point $x$ of the standard $2$-simplex $\Delta^2 \subset \mathbb{R}^3$, define a point of $S^1$ by sending $x$ to the trigonometric cover of the real cone-lift angle of $\gamma$ at $x$. Equivalently, if $\widetilde{\theta}(x)$ is the radially contracted lift $(1-x_2)\,\widetilde{\gamma}(x_1/(1-x_2))+x_2\,\widetilde{\gamma}(0)$ (with the usual apex convention), the value is $(\cos\widetilde{\theta}(x),\sin\widetilde{\theta}(x))$ on the unit circle.
background
The module lifts the path-level winding/displacement invariant of the circle to singular simplices on $S^1$ and proves that displacement kills boundaries: for every singular $2$-simplex the alternating face sum of displacements vanishes. That identity, with the fact that the once-around generator has winding $1$, supplies the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
Here $S^1$ is the exact TopCat.sphere 1 carrier. The trigonometric cover maps a real angle $t$ to the corresponding point of that sphere. For a continuous path $\gamma$ on $S^1$, a real lift along $\gamma$ exists; the cone-lift angle on $\Delta^2$ contracts that lift radially toward the apex value by the prefactor $(1-x_2)$, so the only analytic difficulty is continuity at the apex where the base parameter itself jumps but the prefactor vanishes.
The present definition simply pushes that real cone angle down the covering map, yielding a pointwise $S^1$-valued cone. It is not yet a continuous map; packaging it as a singular $2$-simplex is deferred until continuity at the apex is proved.
proof idea
Pure definitional composition: evaluate the real cone-lift angle of $\gamma$ at the barycentric point $x$, then apply the trigonometric circle parametrization. No tactics, no lemmas beyond the two constituent definitions. Continuity and face identities are proved separately against this pointwise formula.
why it matters
This is the pointwise geometric core of the zero-winding nullhomotopy on singular $1$-cycles. Downstream, once continuity of the pointwise cone is assumed, it is packaged as a singular $2$-simplex whose base face recovers the original edge and whose side faces are the constant apex edge; those face identities feed the endpoint-form and continuity-hypothesis cone handoffs that prove a closed zero-winding edge bounds.
In the module's program, that bounding statement is exactly what turns the winding homomorphism on $1$-cycles into a left inverse of the fundamental class, completing the injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The remaining open analytic obligation named in the doc-comment is continuity of this cone at the apex; the generation/surjectivity half of the comparison map still needs a simplicial prism or subdivision operator absent from Mathlib singular homology.
No Recognition forcing-chain landmark (T5–T8, RCL, $\varphi$) is invoked here: the declaration is pure circle topology supporting the foundation layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.