orientedCyclicFamilyTermListCycle
plain-language theorem explainer
Packages a finite list of oriented cyclic families (sign-oriented closed walks of singular 1-edges on S¹) as a single integer 1-cycle. Cited by anyone proving that the fundamental class generates H₁(S¹;ℤ) from concrete family data. Proof is a one-line map-and-sum wrapper through the directed free-term cycle constructor.
Claim. Given a finite list of oriented cyclic family terms (each a finite sign-oriented closed walk of singular $1$-simplices on $S^1$), form the associated degree-$1$ cycle in the integer singular chain complex of $S^1$.
background
The module lifts path-level winding on the circle to singular simplices of $S^1$ and proves that displacement kills boundaries, the chain-level fact needed for a homology invariant. Together with the once-around generator evaluating to winding $1$, this supplies the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The remaining generation half needs concrete cycle representatives built from closed walks.
An oriented cyclic family term is a finite list of oriented singular edges whose terminals match the next initials under cyclic rotation: a concrete closed walk with signs. The directed free-term packaging forgets the oriented-family bookkeeping and retains only the free-term cycle data. The ambient complex is Mathlib's singular chain complex of $\mathrm{TopCat.sphere},1$ with coefficients in $\mathbb{Z}$, whose degree-$1$ homology is the strict T8 target in this foundation layer.
The list-level directed free-term cycle is the recursive sum of the individual free-term cycles (empty list to zero). This definition is the oriented-family front-end to that sum.
proof idea
One-line wrapper. Map each oriented cyclic family term to its directed free-term packaging via the structure's conversion (which builds a free term from the oriented edge family and the cyclic connectivity hypothesis), then apply the existing list-of-free-terms cycle constructor. No new boundary or homology argument is performed here.
why it matters
This is the concrete cycle object that the generation lemmas quantify over. Downstream, orientedCyclicFamilyTermList_boundary_generates states: if every single oriented cyclic family is homologous to an integer multiple of the fundamental cycle, then every finite list is as well, with the equality written against this cycle. That list lemma is then fed into fundamentalCycle_boundary_generates_of_orientedCyclicFamilies, which discharges the global chain-level generation theorem from a per-family hypothesis.
In the Recognition foundation chain this sits on the generation half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$, complementary to the winding-kills-boundaries identity already proved in the module. The module doc notes that full surjectivity of the integer comparison still needs a simplicial prism or subdivision operator Mathlib does not yet supply; this packaging keeps the oriented-family data available for that remaining step rather than collapsing early to free terms only.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.