trigCirclePoint_eq_iff
plain-language theorem explainer
Two real angles hit the same point of $S^1$ under the trigonometric covering exactly when they differ by an integer multiple of $2\pi$. This is the deck group $2\pi\mathbb{Z}$ of the universal cover $\mathbb{R}\to S^1$. Winding-number and path-lifting arguments on the circle cite it constantly. The proof is a two-step rewrite through the exponential form and Mathlib's circle-exp equality.
Claim. For $a,b\in\mathbb{R}$, the trigonometric covering map sends $a$ and $b$ to the same point of $S^1$ if and only if there exists $m\in\mathbb{Z}$ such that $a=b+m\cdot 2\pi$.
background
The module supplies lifting prerequisites for the winding (degree) invariant on singular 1-chains of the exact Mathlib object TopCat.sphere 1. Singular simplices are lifted through the trigonometric covering $\mathbb{R}\to S^1$; two ingredients are needed: contractibility of the standard simplex (so monodromy kills boundaries) and the fiber structure of the covering.
The covering itself is the once-around map sending a real parameter $t$ to the point $(\cos t,\sin t)$ on $S^1$, packaged as a point of TopCat.sphere 1. An upstream sibling states that two parameters hit the same sphere point under this map iff their Circle.exp values agree. Mathlib already knows that Circle.exp a = Circle.exp b precisely when $a-b\in 2\pi\mathbb{Z}$.
Together these give the classical deck-transformation description of the fiber: equality on $S^1$ means the angles differ by an integer number of full turns.
proof idea
Term-mode, two rewrites. First apply the sibling that reduces sphere-point equality under the trigonometric covering to equality of Circle.exp values. Then invoke Mathlib's Circle.exp_eq_exp, which characterises that equality as differing by an integer multiple of $2\pi$. No further casework.
why it matters
This is the algebraic heart of well-definedness of the circle winding number and of the normalisation $w(\mathrm{fundamental})=1$, as the module doc states. Downstream it is used to prove period invariance of the covering (shifting by $k\cdot 2\pi$ leaves the point fixed), lift-independence of path displacement (two lifts of the same path differ by a constant in the deck group, so endpoint differences agree), and integrality of displacement for closed paths and for cyclically connected multi-edge walks.
Those integrality lemmas feed the simplicial winding chain and the terminal-side correction that closes oriented cyclic families. In the Recognition forcing chain this is the continuum side of the T7 eight-tick / circle defect: the discrete octave realises as a circle, and the deck group $2\pi\mathbb{Z}$ is what makes the winding integer-valued on closed walks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.