largeSupportUniformOrientedExtractionStep
plain-language theorem explainer
Packages the uniform-orientation large-support extraction property for free singular 1-chains on S¹: any nontrivial cycle with support size >1 splits as a uniformly forward or uniformly backward oriented cyclic family term plus a strictly smaller residual cycle. Cited by the bridge from oriented closed-walk extraction to the older one-scalar cyclic-edge-list interface. Pure Prop definition, not a proved theorem.
Claim. For every free singular $1$-chain $c$ on $S^1$ with vanishing free boundary, $c \neq 0$, and edge-support cardinality $>1$, there exist a uniformly oriented cyclic family term $T$ and a residual free $1$-chain $r$ such that $c$ equals the directed-cycle chain of $T$ plus $r$, the free boundary of $r$ vanishes, the edge-support of $r$ is strictly smaller than that of $c$, and every oriented edge of $T$ is either all forward or all backward.
background
The module lifts path-level winding on $S^1$ to singular simplices and proves that simplex displacement kills boundaries, giving the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. Generation (every $1$-cycle homologous to an integer multiple of the fundamental cycle) needs support-reducing extraction of cyclic pieces from free $1$-cycles.
Here singularOneChainFree is the free $\mathbb{Z}$-module on singular $1$-simplices of $S^1$, and singularOneBoundaryFree sends each directed edge to terminal minus initial $0$-face. edgeSupportCard is the cardinality of the Finsupp support. EdgeOrientation tags each walk edge as forward or backward (backward meaning the negative singular edge).
The Prop strengthens ordinary large-support extraction by demanding the extracted oriented cyclic family be sign-uniform: all forward or all backward. That uniformity is exactly what the older one-scalar cyclic-edge-list interface needs.
proof idea
No proof body: the declaration is a bare Prop abbreviation. It quantifies over free $1$-cycles $c$ with support size $>1$ and asserts existence of an OrientedCyclicFamilyTerm $T$ and residual chain $r$ with additive decomposition, residual cycle condition, strict support drop, and the uniform-orientation disjunction on $T$'s edge orientations. Downstream theorems treat this Prop as a named hypothesis to discharge.
why it matters
Feeds largeSupportCyclicEdgeListExtractionStep_of_uniformOriented, whose doc states: a large-support extraction whose oriented cycle is uniformly forward or backward proves the older concrete cyclic-edge-list extraction target, isolating the remaining finite-flow obstruction to uniformity of the extracted sign-selected cycle.
In the module's program this is scaffolding for the generation half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$: after winding kills boundaries and hits the fundamental loop, one still needs every free $1$-cycle to reduce, by repeated support-decreasing cyclic extraction, to an integer multiple of the generator. Uniform orientation is the bridge from the newer oriented closed-walk machinery back to the one-scalar cyclic-edge-list API. Not itself a forcing-chain (T0–T8) step; it is local homology infrastructure under CircleWindingChain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.