directedCycleFreeTerm_of_orientedCyclicFamily
plain-language theorem explainer
A cyclically connected finite family of oriented singular edges assembles into a directed-cycle free term: the signed free edge-sum lifts to a genuine degree-1 cycle on S¹ with integer winding. Anyone extracting directed cycles from balanced free edge-flows cites this packaging step. The construction lifts the free boundary-zero identity through the free-to-integer chain bridge and the cycle-lifting map, then reads off integrality from the oriented winding sum.
Claim. Given $k\in\mathbb{N}$ and a family $o:\mathrm{Fin}\,k\to$ (oriented singular edges) such that the terminal vertex of $o_i$ equals the initial vertex of $o_{i+1}$ (indices mod $k$), there is a directed-cycle free term whose free chain is $\sum_i (o_i).\mathrm{chain}$, whose underlying object is a genuine $1$-cycle in the singular integer chain complex of $S^1$, and whose winding number is an integer.
background
The module lifts path-level winding on $S^1$ to singular $1$-simplices and proves that displacement kills boundaries of $2$-simplices, so winding descends to a homology invariant on $H_1(S^1;\mathbb{Z})$. The singular integer chain complex of the topological $1$-sphere is the ambient complex; free edge-chains sit in a parallel free module with a free-to-integer comparison map and a free boundary operator.
An oriented singular edge pairs a singular $1$-simplex with a forward/backward orientation, fixing initial and terminal vertices. A directed-cycle free term packages a multi-edge directed cycle in free-chain coordinates: a genuine degree-$1$ cycle, a free chain equal to its free image, and the existence of an integer equal to the cycle winding (winding of a cycle is the winding chain map applied after inclusion of cycles into $C_1$).
The input hypothesis is cyclic connectivity under finRotate: each oriented edge feeds the next, so the family is a closed oriented walk. Upstream, the free boundary of such a sum vanishes, and the oriented winding sum is integral.
proof idea
Start from cyclicOrientedFamily_freeBoundary_zero: the free boundary of $\sum_i (o_i).\mathrm{chain}$ is zero. Transport that vanishing across the free-to-integer comparison to get $d_1$ of the integer image zero.
Build the $\mathbb{Z}$-module map $\varphi_{\mathrm{free}}$ sending $1$ to the free sum, compose with free-to-chain to get $\psi:C_0(\mathrm{pt})\to C_1(S^1)$. A bridge identity equates free-to-chain composed with $d$ to free-boundary composed with zero-chain free-to-chain; with free-boundary of $\varphi_{\mathrm{free}}$ zero, $\psi$ is a cycle map. Lift via liftCycles to a map into cycles, evaluate at $1$ for the cycle field, and set the free chain to the sum.
chain_eq is the free-to-chain round-trip. Integrality of winding uses orientedWindingSum_cyclic_integral plus the free-to-chain winding evaluation identity.
why it matters
This is the oriented packaging engine for directed-cycle extraction from balanced free edge-flows. Downstream, directedCycleExtraction splits every nonzero balanced free $1$-chain as one directed-cycle free term plus a strictly smaller $\ell^1$ residual; the piece is built by finding an oriented cyclic family and feeding it here. OrientedCyclicFamilyTerm is the concrete data type of such families.
In the module's program, winding on cycles is the left-inverse half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ (split-injectivity of the fundamental class). Packaging multi-edge oriented closed walks as genuine cycles with integer winding is the combinatorial half of reading that invariant off balanced flows, not a single closed edge. It generalises the unoriented cyclic-family constructor to the sign-selected orientations produced by balanced-flow walk extraction.
Framework-wise this sits in the foundation layer that computes $H_1(S^1)$ strictly (the T8-adjacent singular-homology target), not in the forcing chain T0–T8 itself. No open scaffold remains in this definition; it is complete packaging.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.