DirectedCycleFreeTerm
plain-language theorem explainer
Packages one multi-edge directed cycle in free singular 1-chain coordinates on S¹: a 1-cycle, its free-chain image, the matching equality, and integrality of winding. Anyone proving the generation half of H₁(S¹;ℤ) ≅ ℤ via balanced edge-flow decomposition cites it. Pure structure: fields only, no proof obligation.
Claim. A directed multi-edge cycle piece on $S^1$ is a tuple $(c,\gamma)$ where $c$ is a singular $1$-cycle with integer coefficients, $\gamma$ is a free singular $1$-chain, the free-chain image of $c$ equals $\gamma$, and the winding number of $c$ is an integer (i.e. lies in the image of $\mathbb{Z}\hookrightarrow\mathbb{R}$).
background
The module lifts path-level winding on $S^1$ to singular simplices and proves that simplex displacement kills boundaries of $2$-simplices, so winding descends to a homology invariant. Together with the once-around generator mapping to $1$, this gives the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The converse (every $1$-cycle is homologous to an integer multiple of the fundamental cycle) needs a generation argument from finite balanced edge flows.
Free singular $1$-chains are the explicit finitely supported $\mathbb{Z}$-linear combinations of singular $1$-simplices used for combinatorial bookkeeping. The comparison map sends raw singular chains into that free module. Winding of a cycle is the real-valued invariant obtained by summing simplex displacements.
A closed single-edge term forces the two faces of one simplex to agree. This structure drops that restriction: the piece may be a multi-edge directed cycle, exactly what a finite-graph extraction theorem produces from a balanced nonzero edge flow.
proof idea
Definitional structure with four fields and no proof body. The cycle field is an element of the $1$-cycles of the integer singular chain complex of $S^1$. The chain field is the corresponding free $1$-chain. The equality field asserts that applying the free-chain comparison to the inclusion of cycles recovers that free chain. The winding field is an existence witness that cycle winding lands in $\mathbb{Z}\subset\mathbb{R}$. Downstream constructors (oriented cyclic families, extraction) inhabit the fields; the structure itself only records the interface.
why it matters
This is the atomic summand for the generation half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ in the circle winding chain development. The one-step extraction theorem splits every nonzero balanced free edge-flow into one such piece plus a strictly smaller $\ell^1$ residual. Finite lists of these pieces assemble into cycle and free-chain sums, with theorems equating the free image of the list-cycle to the list-chain and transporting boundary-generation from single terms to lists.
A concrete cyclic edge-list term specialises the same pattern with an explicit edge list and global coefficient. The module doc flags that Mathlib still lacks the simplicial prism or subdivision operator for a fully automatic singular-homology generation proof; this structure is the combinatorial carrier that the project-local finite-graph route fills in. Framework-wise it supports the topological side of the eight-tick / circle recognition story (period and winding as integer invariants), not the T5–T8 forcing chain directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.