freeBoundaryKernel_decomposesIntoDirectedCycles
plain-language theorem explainer
Names the finite-graph kernel target used throughout the circle H₁ development: every free singular 1-chain on S¹ with vanishing explicit boundary equals a finite sum of directed-cycle pieces. Anyone proving integer winding or the Mathlib comparison H₁(S¹;ℤ) ≅ ℤ cites this Prop as the abstract decomposition hypothesis. The body is a pure Prop definition, not a proof.
Claim. Every free singular $1$-chain $c$ on $S^1$ with vanishing free boundary ($\partial c = 0$) equals the free-chain sum of a finite list of directed-cycle terms.
background
The module lifts path-level winding on $S^1$ to singular simplices and proves that simplex displacement kills boundaries, giving the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The free module singularOneChainFree is the free $\mathbb{Z}$-module on actual singular $1$-simplices of $\mathrm{TopCat.sphere},1$. Its explicit boundary singularOneBoundaryFree sends each directed edge to terminal $0$-face minus initial $0$-face.
A DirectedCycleFreeTerm packages one multi-edge directed cycle: a genuine singular cycle together with the free-chain image it represents. The list sum directedCycleFreeTermListChain is the corresponding free-chain total. The present definition is the abstract finite-graph statement that every balanced free edge-flow is a finite sum of such pieces.
proof idea
Definitional: the declaration is the Prop
$\forall c,;\partial_{\mathrm{free}}(c)=0\Rightarrow\exists,ts,;c=\sum ts$,
with no proof body beyond that equation. Downstream theorems either assume it as a hypothesis or discharge it by induction on $\ell^1$ size (freeBoundaryKernel_decomposesIntoDirectedCycles_holds) or by reduction from cyclic edge-list decompositions.
why it matters
This is the correct general finite-graph target for the generation half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. Feeding it into cycleWinding_integral_of_freeBoundaryKernel_decomposesIntoDirectedCycles yields integer winding on all singular $1$-cycles. Together with a zero-winding filling bound it closes Mathlib's comparison via circleH1ZIsoInt_of_directedCycles_of_zeroWinding_bounds.
The unconditional discharge is freeBoundaryKernel_decomposesIntoDirectedCycles_holds (strong induction peeling oriented closed walks). A concrete cyclic-edge-list route also implies it. In the Recognition foundation stack this supplies the missing surjectivity half that, with the kills-boundaries identity already proved in-module, completes the integer winding homomorphism as left inverse to the fundamental class.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.