directedCycleFreeTermList_winding_integral
plain-language theorem explainer
Any finite list of packaged directed-cycle pieces on S¹ has integer total winding: the winding of their cycle-sum equals some integer viewed in ℝ. Homology and circle-winding arguments cite it when assembling free-boundary kernel decompositions into an integrality statement for all 1-cycles. The proof is list induction: empty sum is zero; the cons case adds the piece’s built-in integer winding to the inductive hypothesis via additivity of the winding chain map.
Claim. For every finite list $ts$ of directed cycle pieces (each a $1$-cycle on $S^1$ with a free-chain representative and integer winding), there exists an integer $n$ such that the winding of the sum of the cycles in $ts$ equals $n$ as a real number.
background
This module lifts path-level winding on the circle to singular $1$-simplices of $S^1$ and proves that displacement kills boundaries of $2$-simplices, so winding descends to a homology invariant. Together with the fact that the fundamental loop has winding $1$, that gives the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
A DirectedCycleFreeTerm is a general directed cycle piece in free-chain coordinates: a $1$-cycle, an explicit free edge-chain, a coherence equation relating them under the free-chain comparison map, and a field asserting that the piece already has integer winding. The list sum directedCycleFreeTermListCycle is the inductive sum of those cycle objects (empty list to $0$, cons by addition in the cycles module).
cycleWinding includes a degree-$1$ cycle into $C_1(S^1;\mathbb{Z})$ and applies the winding chain map, yielding a real. The theorem packages the elementary fact that finite sums of integer-winding pieces remain integer-winding.
proof idea
Proof by structural induction on the list.
Empty case: refine with integer $0$; unfold the list-sum and cycleWinding, then simp gives winding of the zero cycle is $0$.
Cons case $t::ts$: obtain $n_1$ from the structure field t.winding_integral, and $n_2$ from the inductive hypothesis on $ts$. Refine with $n_1+n_2$. Unfold the list-sum definition and cycleWinding in the goals and hypotheses; rewrite with map_add (additivity of the composite winding map on cycles) and the two integrality equalities, then simp closes the real equality.
why it matters
Integer winding for finite directed-cycle assemblies is the bridge from per-piece data to global integrality on singular $1$-cycles. The sole downstream consumer is cycleWinding_integral_of_freeBoundaryKernel_decomposesIntoDirectedCycles, whose doc-comment states that the general directed-cycle kernel decomposition implies integer winding for all singular $1$-cycles: once a free boundary-kernel chain decomposes into directed cycle pieces, this theorem supplies the integer for the summed cycle.
In the module’s program, that integrality is half of identifying $H_1(S^1;\mathbb{Z})$ with $\mathbb{Z}$ via winding (the left-inverse / split-injective half already rests on kills-boundaries plus the fundamental loop). The generation half still needs simplicial prism or subdivision structure Mathlib does not yet provide. Within Recognition Science foundation work, the circle winding chain is infrastructure for discrete period and octave counting (eight-tick / $2^3$ structure) rather than a direct T5–T8 forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.