exists_orientedCyclicFamily_of_balanced_nonzero
plain-language theorem explainer
Every nonzero balanced free 1-chain on S¹ carries an oriented closed walk: finitely many distinct support edges whose sign-selected orientations meet terminal-to-initial around a cycle. Cycle-extraction and ℓ¹-peeling arguments cite it as the combinatorial seed. The proof splits on loops versus a pigeonhole period of the successor map on finite edge support.
Claim. Let $c$ be a free singular $1$-chain on $S^1$ with $\partial c = 0$ and $c \neq 0$. Then there exist $k > 0$ and an injective family $g : \{0,\ldots,k-1\} \to$ (singular $1$-simplices) with each $g(i)$ in the edge support of $c$, such that the sign-selected orientation of $g(i)$ has terminal vertex equal to the initial vertex of the orientation of $g(i+1 \bmod k)$.
background
The module lifts path winding on $S^1$ to singular $1$-simplices and proves that displacement kills boundaries, giving the split-injective half of $H_1(S^1;\mathbb{Z}) \cong \mathbb{Z}$. Singular $0$- and $1$-simplices are the actual simplices of TopCat.sphere 1; free $1$-chains are finitely supported integer combinations of those edges.
A chain is balanced when its free boundary vanishes. Edge support is the finite set of $1$-simplices with nonzero coefficient. For each supported edge one selects an orientation by the sign of the coefficient, yielding initial and terminal $0$-simplices. Balance forces, at every vertex, incoming and outgoing oriented mass to match, so a successor edge always exists off any non-loop terminal.
Upstream, chainL1_sub_orientedCyclic records that subtracting the oriented cyclic chain of such a walk drops the $\ell^1$ size by exactly the walk length. That decrease is what turns the existence result into an extraction step.
proof idea
Case split on whether some supported edge is a loop (initial equals terminal under the sign orientation).
If a loop exists, take $k=1$ and the constant family on that edge; injectivity is vacuous on Fin 1, and the cyclic terminal-initial identity is the loop equation.
If no loops, support is nonempty (else $c=0$ by edgeSupport_eq_empty_iff). On the finite subtype of support, define nextSupp by choosing, via exists_next_orientedEdge_from_terminal and balance, a successor whose initial equals the current terminal. The orbit of any start point under iteration is infinite into a finite set, so pigeonhole yields a periodic point. Take the minimal period $m+1$, index the orbit by Fin (m+1), and verify injectivity from the standard injectivity of iterates below the minimal period. The rotate-successor identity follows by comparing finRotate with one step of nextSupp, using that the period returns to the base point.
why it matters
This is the combinatorial engine behind one-step directed-cycle extraction on free balanced flows. Downstream, directedCycleExtraction packages the walk through the oriented homological engine and subtracts it, citing chainL1_sub_orientedCyclic for a strict $\ell^1$ drop and a balanced residual. orientedCyclicFamilyExtraction keeps the raw family data; largeSupportOrientedScaledExtractionStep_holds discharges the large-support extraction interface from the same seed (needing only nonzero balance).
In the module's program, repeated peeling feeds the generation half of $H_1(S^1;\mathbb{Z}) \cong \mathbb{Z}$: every $1$-cycle is homologous to an integer multiple of the fundamental loop once cycles can be extracted and residual size driven to zero. The winding side (kills-boundaries plus once-around evaluates to $1$) is already in place; this lemma supplies the missing cycle-finding step on free chains without simplicial prisms.
No Recognition forcing landmark (T5–T8, RCL, $\varphi$) is invoked here; the result is pure singular-chain combinatorics on $S^1$, foundational for the circle homology comparison the framework uses elsewhere.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.