directedCycleTerms_boundary_generate
plain-language theorem explainer
Packages the remaining geometric generation target for singular homology of the circle: every directed-cycle free term is homologous to an integer multiple of the fundamental 1-cycle. Downstream H₁(S¹;ℤ) ≅ ℤ arguments cite this Prop as a single hypothesis. It is a bare Prop definition, not a proved theorem.
Claim. The proposition asserting that for every directed-cycle free term $t$ (a 1-cycle together with a free singular 1-chain representative), there exist an integer $n$ and a singular 2-chain $b$ such that $t$'s cycle equals the image of $b$ under the boundary-to-cycles map plus $n$ times the fundamental cycle of $S^1$.
background
The module lifts path-level winding on $S^1$ to singular simplices and proves that simplex displacement kills boundaries: for every singular 2-simplex the alternating face sum of displacements vanishes. Combined with the fact that the once-around loop has winding 1, this yields a left inverse $H_1(S^1;\mathbb{Z})\to\mathbb{Z}$. The missing half is generation: every 1-cycle should be homologous to an integer multiple of the fundamental cycle.
A DirectedCycleFreeTerm records a general directed multi-edge cycle piece in free-chain coordinates: a degree-1 cycle of the integer singular chain complex of TopCat.sphere 1, plus a free singular 1-chain equal to its image under the free-chain comparison. The fundamental cycle is the lift of the once-around singular 1-simplex into the cycles object.
The ambient complex is Mathlib's singular chain complex of the topological 1-sphere with $\mathbb{Z}$ coefficients; its degree-1 homology is the strict T8-adjacent computational target of the circle computation.
proof idea
No proof: this is a Prop-valued definition. The body is the universal quantification over directed-cycle free terms of the existence of an integer coefficient and a degree-2 chain whose boundary-to-cycles image corrects the term to an integer multiple of the fundamental cycle. Downstream lemmas treat the name as a single hypothesis and discharge listwise and global generation from it by finite summation and free-chain bookkeeping.
why it matters
This is the local remaining geometric target named in the doc-comment: chain-level homology of each directed-cycle term to a multiple of the fundamental cycle. Four immediate consumers take it as hypothesis: listwise generation for finite directed-cycle lists; the global fundamentalCycle_boundary_generates statement; the zero-winding filling target; and finally circleH1ZIsoInt_of_directedCycleTerms, which states that one-directed-cycle generation is enough for the Mathlib circle $H_1$ isomorphism.
In the module narrative, the kills-boundaries identity already gives the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. Surjectivity of the integer comparison map needs generation; Mathlib lacks a simplicial prism/subdivision operator, so the project isolates that gap as this Prop. Closing it (or the equivalent single directed closed walk) finishes the homology computation that underwrites the circle side of the foundation chain toward T8 ($D=3$) and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.