closedSingularOneCycleList_iCycles
plain-language theorem explainer
Including a finite list of closed singular 1-generator cycles into ambient C₁ recovers the matching raw chain sum. Cited when lifting raw-chain spanning statements to cycle-object spanning via monomorphicity of the cycles inclusion. Proof is list induction: empty case by unfolding, cons case by additivity of the inclusion plus the single-term identity.
Claim. For every finite list $ts$ of closed singular one-cycle terms (each a singular $1$-simplex on $S^1$ with equal faces, plus an integer coefficient), the image of the associated $1$-cycle under the inclusion $Z_1\hookrightarrow C_1(S^1;\mathbb{Z})$ equals the raw degree-$1$ chain sum of those same terms.
background
The module lifts path-level winding on $S^1$ to singular simplices and proves that displacement kills boundaries, giving the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The generation half needs finite closed-generator spanning of cycles.
A ClosedSingularOneCycleTerm is one summand: a singular $1$-simplex whose two faces agree (so it is already a cycle) together with an integer coefficient. Lists of such terms assemble either as cycle objects (closedSingularOneCycleList) or as raw chains in degree $1$ (closedSingularOneChainList).
The ambient complex is Mathlib's singular chain complex of TopCat.sphere 1 with $\mathbb{Z}$ coefficients. The map iCycles 1 is the canonical inclusion of the submodule of $1$-cycles into $C_1$.
proof idea
Structural induction on the list ts.
Empty list: both sides unfold to zero; simp finishes.
Cons case t :: ts: unfold both list constructors, rewrite by additivity of the cycles-inclusion homomorphism (map_add), apply the single-term identity t.cycle_iCycles (inclusion of one closed generator recovers its raw chain), then invoke the inductive hypothesis on the tail.
why it matters
This is the bookkeeping bridge between cycle-object and raw-chain presentations of finite closed-generator sums. Downstream, closedSingularOneCycleList_spans_of_chainList_spansCycles uses it (with monomorphicity of iCycles) to transfer a raw-chain spanning hypothesis into the cycle-level spanning proposition closedSingularOneCycleList_spans.
That spanning statement is the finite-support combinatorial input needed for integrality of cycle winding and the surjective/generation half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. In the Recognition forcing chain the circle homology computation is the strict algebraic target feeding dimensional and octave constraints (T7 eight-tick, T8 $D=3$). The module notes Mathlib still lacks the prism/subdivision operator for a fully internal generation proof; this lemma keeps the finite-list side clean while that gap remains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.