displacementSum_cyclic_intMul
plain-language theorem explainer
A cyclically connected family of continuous paths on S¹ has total path-displacement equal to an integer multiple of 2π. Anyone building multi-edge winding sums or cyclic edge-list pieces cites this as the path-level integrality engine. The proof lifts each path, reads deck-group jumps at junctions via the trigonometric covering, reindexes by cyclic rotation, and telescopes.
Claim. Let $k\in\mathbb{N}$ and let $f_i:I\to S^1$ be continuous paths for $i\in\mathrm{Fin}\,k$. Suppose the family is cyclically connected: $f_i(1)=f_{i+1}(0)$ for every $i$ (indices mod $k$). Then there exists $m\in\mathbb{Z}$ such that $\sum_i \mathrm{disp}(f_i)=m\cdot 2\pi$, where $\mathrm{disp}$ is the endpoint difference of the canonical real lift of the path.
background
The module lifts the path-level winding/displacement invariant of CircleWinding to singular simplices of $S^1$ and proves that displacement kills boundaries, the chain-level fact needed for a homology invariant. Path displacement of $\gamma:I\to S^1$ is $\mathrm{pathLift}(\gamma)(1)-\mathrm{pathLift}(\gamma)(0)$: how far the canonical real lift travels.
The covering map is the trigonometric parametrization $\mathrm{trigCirclePoint}:\mathbb{R}\to S^1$. Its fibers are the deck group $2\pi\mathbb{Z}$: $\mathrm{trigCirclePoint}(a)=\mathrm{trigCirclePoint}(b)$ iff $a=b+m\cdot 2\pi$ for some $m\in\mathbb{Z}$ (CircleLifting). At each junction of a closed walk the two lifts sit in the same fiber, so they differ by a deck transformation.
This theorem is the multi-edge generalization of single-loop displacement integrality. It needs no prism or subdivision operator; pure lift arithmetic and cyclic reindexing suffice.
proof idea
For each junction $i$, the lift endpoints $\mathrm{pathLift}(f_i)(1)$ and $\mathrm{pathLift}(f_{i+1})(0)$ project to the same point of $S^1$ by the cyclic connection hypothesis and the fact that pathLift actually lifts. Apply $\mathrm{trigCirclePoint_eq_iff}$ to obtain integers $m_i$ with difference $m_i\cdot 2\pi$.
Rewrite each displacement as an endpoint difference via $\mathrm{pathDisplacement_self}$. Sum, distribute the difference, and reindex the second sum by $\mathrm{finRotate}$ (equivariant sum). The sum becomes $\sum_i(\mathrm{pathLift}(f_i)(1)-\mathrm{pathLift}(f_{i+1})(0))$, which equals $\sum_i m_i\cdot 2\pi$, hence $(\sum m_i)\cdot 2\pi$.
why it matters
Integrality of total displacement on closed multi-edge walks is the path-form input for the winding_integral field of cyclic edge-list pieces. Downstream, singularWindingSum_cyclic_integral and orientedWindingSum_cyclic_integral reduce singular-edge and oriented-edge cyclic sums to this fact (after translating face-matching into path endpoint matching).
Together with the kills-boundaries identity for 2-simplices and the fact that the once-around generator has winding 1, the module aims at the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. That comparison is the strict T8 target on the singular chain complex of $\mathrm{TopCat.sphere},1$. Surjectivity still needs a simplicial prism/subdivision operator Mathlib does not yet supply; this lemma is on the injectivity/integrality side and avoids that gap.
Also feeds the null-homotopy lemma for closed singular edges of winding zero, path-level input for the remaining singular prism construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.