directedCycleFreeTerm_of_cyclicFamily
plain-language theorem explainer
A cyclically head-to-tail family of singular 1-simplices on S¹ packages as a DirectedCycleFreeTerm: free edge-chain ∑⟨eᵢ⟩ is a genuine degree-1 cycle with integer winding. Downstream cyclic extraction and oriented-walk engines cite it to discharge all homological obligations, leaving only combinatorial flow decomposition. Construction routes the sum through the free module, lifts via liftCycles after free-boundary vanishing, and reads integrality from the cyclic winding sum.
Claim. Given $k\in\mathbb{N}$ and singular $1$-simplices $e_0,\ldots,e_{k-1}$ on $S^1$ with $\mathrm{term}(e_i)=\mathrm{init}(e_{i+1\bmod k})$ for all $i$, there is a directed-cycle free term whose free chain is $\sum_i\langle e_i\rangle$, whose underlying singular chain is a genuine $1$-cycle, and whose winding number is an integer.
background
The module lifts path-level winding on $S^1$ to singular simplices and proves that displacement kills boundaries of $2$-simplices, yielding a winding homomorphism on $1$-cycles that is a left inverse to the fundamental class (the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$).
A SingularOneSimplex is a singular $1$-simplex in the singular simplicial set of $\mathrm{TopCat.sphere},1$. A DirectedCycleFreeTerm records a multi-edge directed cycle in free-chain coordinates: a genuine cycle in the integer singular chain complex of $S^1$, a free edge-chain, an equality relating them via the free/raw comparison, and a witness that cycle winding is an integer.
Cyclic connectivity means each edge's terminal vertex equals the next edge's initial vertex under rotation of $\mathrm{Fin},k$. The free boundary of such a family vanishes, so the sum is a cycle; the cyclic winding sum is integral.
proof idea
First apply cyclicEdgeFamily_freeBoundary_zero so the free boundary of $\sum_i\langle e_i\rangle$ is zero, then transport to the raw complex via d_singularOneChainFreeToChain_eq_zero_of_freeBoundary_zero.
Build $\varphi_{\mathrm{free}}:\mathbb{Z}\to C_1^{\mathrm{free}}$ as the span-singleton map on that sum, set $\psi=\varphi_{\mathrm{free}}\circ\mathrm{freeToChain}$, and prove $\psi\circ\partial=0$ by bridging free and raw boundaries through the $C_0$ iso (singularOneChainFreeToChain_boundary_free, hom_inv_id). Lift $\psi$ into cycles with liftCycles.
Package: cycle is the lifted generator at $1$, chain is the free sum, chain_eq from the free/raw round-trip, and winding_integral from singularWindingSum_cyclic_integral after unfolding cycleWinding and applying windingChainMap_singularOneChainFreeToChain_sum.
why it matters
Doc-comment states this discharges the entire homological and winding obligation of cyclic extraction; only combinatorial exhibition of a cyclic family inside a balanced flow remains. It is the forward-engine keystone that the oriented closed-walk section generalises (backward edges contribute $-\langle e\rangle$ and negated winding).
Used by cyclicSingularEdgeListTerm_of_cyclicFamily, the compatibility surface between older forward-only extraction and the newer oriented-cycle engine, and by windingChainMap_freeToChain_orientedChain_sum, which evaluates winding on oriented walk chains.
In the module's program this supplies concrete multi-edge cycle witnesses for the winding left-inverse to the fundamental class on $S^1$, supporting the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. Surjectivity still needs simplicial prism/subdivision not yet in Mathlib singular homology.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.