CyclicSingularEdgeListTerm
plain-language theorem explainer
A data package for one concrete cyclic singular 1-chain on S¹: a finite list of singular edges, an integer coefficient, a certified 1-cycle, equality of that cycle's free-chain image with the scaled edge-list sum, and integrality of the cycle winding. Algebraic topologists comparing the oriented-cycle engine to the older edge-list extraction target cite it. As a structure it is pure packaging, not a proved identity.
Claim. A cyclic singular edge-list term consists of a finite list $E$ of singular $1$-simplices on $S^1$, an integer coefficient $c\in\mathbb{Z}$, and a $1$-cycle $\gamma$ in the singular integer chain complex of $S^1$, such that the image of $\gamma$ in the free chain group equals $c$ times the chain sum of the edges in $E$, and the winding number of $\gamma$ is an integer.
background
The module lifts the path-level winding/displacement invariant of the circle to singular simplices of $\mathrm{TopCat.sphere},1$. A singular $1$-simplex is a continuous map $\Delta^1\to S^1$ in the singular simplicial set. Displacement (equivalently $2\pi$ times winding) is assigned by reparameterizing $\Delta^1$ to the unit interval and taking path displacement; the key identity is that alternating face sums of displacements vanish on every singular $2$-simplex, so winding kills boundaries and descends to homology.
Together with the fact that the once-around generator has winding $1$, this yields a left inverse to the fundamental class on $H_1(S^1;\mathbb{Z})$, the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The present structure sits at the concrete bookkeeping layer: it records an explicit finite edge list together with a certified cycle whose free-chain image is a scalar multiple of that list sum, plus the integrality side-condition on winding.
The surrounding comment marks this as the compatibility surface between a newer oriented-cycle engine and an older forward-only cyclic edge-list extraction target.
proof idea
No proof body: the declaration is a structure (definitional packaging). The fields are the list of singular $1$-simplices, the global integer coefficient in $\mathrm{ModuleCat}$ of $\mathbb{Z}$, the cycle object in degree $1$ of the singular integer chain complex of the circle, the equality that the free-chain image of that cycle (via the inclusion of cycles) equals the coefficient times the singular edge-list chain of the listed edges, and the existence of an integer equal to the real-valued cycle winding. Inhabitants are built by supplying those five pieces of data; lemmas that package a forward cyclic family into this interface discharge the two Prop fields.
why it matters
This structure is the concrete cyclic edge-list piece used as the older extraction target in the circle-winding chain development. It lets genuinely forward cyclic families be re-exported in the form expected by edge-list consumers, without changing the homology-level winding story (kills-boundaries plus generator winding $1$).
In the Recognition Science foundation stack this sits under the singular-homology computation of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$, which underwrites circle-valued phases, winding, and the eight-tick octave bookkeeping (T7) once discrete recognition cycles are compared to continuous circle homology. The module doc notes that the converse generation half (every $1$-cycle homologous to an integer multiple of the fundamental cycle) still needs a simplicial prism/subdivision operator that Mathlib singular homology does not yet supply; this structure does not close that gap, it only standardizes the forward cyclic data format.
No downstream used_by edges are recorded yet; the immediate role is the compatibility lemma that packages oriented cycles into this interface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.