largeSupportUniformOrientedScaledExtractionStep
plain-language theorem explainer
Defines the scaled, uniformly oriented large-support extraction property for free singular 1-chains on S¹: every nonzero boundary-free chain with support size >1 decomposes as a positive integer multiple of a uniformly forward or backward oriented cyclic family term plus a strictly smaller-support cycle. Homology workers extracting generators of H₁(S¹;ℤ) cite it. The body is a pure Prop package, not a proved theorem.
Claim. Every nonzero free singular $1$-cycle $c$ on $S^1$ with edge-support cardinality strictly greater than $1$ admits a decomposition $c = m\cdot T + r$ where $m>0$, $T$ is an oriented cyclic family term whose edge orientations are all forward or all backward, $r$ is again a free $1$-cycle, and the edge-support of $r$ is strictly smaller than that of $c$.
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}$. Free singular $1$-chains are the free $\mathbb{Z}$-module on actual singular $1$-simplices of $\mathrm{TopCat.sphere},1$. The free boundary sends each directed edge to terminal $0$-face minus initial $0$-face.
Edge-support cardinality is the finite support size of such a free chain. Edge orientation is an inductive tag (forward or backward) recording whether a walk traverses a singular edge or its negative. An oriented cyclic family term packages a closed walk of singular edges with orientations; its associated free chain is the alternating sum of those oriented edges.
The present Prop strengthens ordinary large-support extraction by requiring the extracted cycle to be uniformly oriented and allowing a positive integer scale factor $m$ (the minimum coefficient along the closed walk) so that support strictly decreases after subtraction.
proof idea
No proof: the declaration is a bare def of a Prop. It packages the universal quantifiers (cycle, boundary-free, nonzero, large support) and the existential data (oriented cyclic family term $T$, scale $m>0$, remainder cycle $r$) with the five conjuncts that make the extraction support-decreasing and uniformly oriented. Downstream theorems assume this Prop as a hypothesis and discharge concrete cyclic-edge-list targets from it.
why it matters
Feeds the single downstream theorem largeSupportCyclicEdgeListExtractionStep_of_uniformOrientedScaled, whose doc-comment states that a scaled large-support extraction whose oriented cycle is uniformly forward or backward proves the older concrete cyclic-edge-list extraction target. That older target is part of the generation half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$: every free $1$-cycle should be homologous to an integer multiple of the fundamental loop.
The module already has the kills-boundaries identity and the winding of the once-around generator; what remains is support-reducing extraction of cyclic pieces until only multiples of the fundamental class remain. Uniform orientation simplifies the passage from abstract oriented family terms to concrete edge lists. Within Recognition Science this sits in the foundation layer that underwrites the eight-tick octave and the winding comparison used later in the forcing chain, but the declaration itself is pure singular-homology scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.