OrientedCyclicFamilyTerm
plain-language theorem explainer
A finite closed walk of oriented singular 1-edges on S¹: k edges whose terminals match the next initials under cyclic rotation. It packages multi-edge directed cycles for the free-chain winding calculus. Downstream lemmas convert it to a directed-cycle free term, equate total winding to the sum of edge windings, and set up path-cone prism cancellation. Citation target for anyone assembling concrete cycle generators before the H₁ comparison map.
Claim. An oriented cyclic family is a triple $(k, o, h)$ where $k\in\mathbb{N}$, $o:\{0,\ldots,k-1\}\to$ (oriented singular $1$-edges on $S^1$), and for every index $i$ the terminal vertex of $o(i)$ equals the initial vertex of $o(i+1\bmod k)$. Thus $o$ is a finite sign-oriented closed walk in singular $1$-simplices.
background
The ambient module lifts path-level winding on $S^1$ to singular simplices and proves that displacement kills boundaries: for every singular $2$-simplex the alternating face sum of displacements vanishes. Together with the fact that the fundamental loop has winding $1$, this supplies the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The generation (surjectivity) half needs multi-edge cycle bookkeeping and prism/subdivision arguments.
An oriented singular edge is a singular $1$-simplex plus a forward/backward orientation, so it has well-defined initial and terminal $0$-simplices. A directed-cycle free term is the free-chain package of a (possibly multi-edge) directed cycle: a homology cycle, its free $C_1$ representative, and an integrality witness for total winding.
This structure is the concrete combinatorial input: a finite oriented edge family closed under cyclic adjacency. It is the object one builds before converting into free-chain coordinates and applying winding and cone-boundary identities.
proof idea
Definitional structure, not a proved theorem. The only data are the edge count $k$, the family $o$ of oriented singular edges, and the cyclic gluing hypothesis that each terminal equals the next initial under finRotate.
Immediate packaging is one-line: toDirectedCycleFreeTerm applies the existing constructor that turns an oriented cyclic family plus the gluing hypothesis into a directed-cycle free term. Companion lemmas (not part of the structure body) then rewrite inclusion into raw $C_1$ as the sum of oriented edge chains, identify cycle winding with $\sum_i$ oriented edge windings, build the summed path-cone $2$-chain, expand its free boundary, and reindex constant-apex side sums by the cyclic shift.
why it matters
In the Recognition foundation stack this is the concrete multi-edge cycle object feeding the singular winding calculus on $S^1$. The module's goal is the homology-invariant winding map that left-inverts the fundamental class, the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. Single closed edges are not enough for the generation half; one needs finite oriented closed walks and prism cancellation of side chains.
The structure is the combinatorial carrier for those walks. Its companion results state the prism target explicitly: total winding is an integer, subtracting that multiple of the fundamental cycle leaves a zero-winding residual, and constant-apex side sums cancel after cyclic reindexing. No downstream graph edges are recorded yet, so it currently sits as infrastructure inside the circle-winding chain development rather than a named input to a higher forcing step (T0–T8).
It does not itself close the surjectivity/generation half; that still requires the simplicial prism or subdivision operator Mathlib singular homology does not yet supply.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.