constantSingularOneCycle_bounds
plain-language theorem explainer
At any point p on S¹, the constant closed singular 1-cycle is a boundary in the cycle object: some integer 2-chain maps under toCycles to that generator. Homology workers proving the trivial class vanishes in H₁(S¹;ℤ) cite this base case. The proof takes the free constant 2-simplex chain and reduces equality by injectivity of iCycles plus the raw-boundary and cycle-inclusion identities.
Claim. For every point $p\in S^1$, there exists a degree-$2$ singular chain $b$ with integer coefficients such that the chain-complex map from $2$-chains into $1$-cycles sends $b$ to the cycle-object generator of the constant singular $1$-simplex at $p$ (whose two faces agree).
background
The module lifts path winding on $S^1$ to singular $1$-simplices and proves that displacement kills boundaries, the chain-level fact needed for a homology invariant. The ambient complex is Mathlib's singular chain complex of $\mathrm{TopCat.sphere},1$ with coefficients in $\mathbb{Z}$, whose $H_1$ is the strict T8 target.
A constant singular $1$-simplex at $p$ is the continuous map $\Delta^1\to S^1$ with value $p$. Its two faces agree, so it defines a closed generator and, via liftCycles, an element of the cycle object in degree $1$. The companion constant singular $2$-simplex at $p$ is the free generator used as a bounding chain.
Upstream, closedSingularOneCycle packages a closed singular $1$-simplex as a map into cycles; including that cycle back into $C_1$ recovers the coproduct summand. The raw boundary of the constant $1$-simplex vanishes in the expected free sense, which is what lets the constant $2$-chain serve as a nullhomotopy at chain level.
proof idea
Build the candidate $2$-chain $b$ as the image of the free generator on the constant singular $2$-simplex at $p$ under the free-to-chain map. It remains to check that toCycles sends $b$ to the closed constant $1$-cycle generator evaluated at $1$.
Because the inclusion of cycles into $C_1$ is mono, it is enough to compare after composing with iCycles. Rewrite the left side by the complex identity toCycles ≫ iCycles = differential, then apply the raw-boundary computation for the constant $1$-simplex and the inclusion identity for closedSingularOneCycle; both sides match by rfl.
why it matters
Constant loops are the zero class in $\pi_1(S^1)$ and must bound in singular homology. This lemma records that fact at the cycle-object level for the free constant generator, so later prism or subdivision arguments can treat the trivial summand cleanly when comparing winding to the fundamental class.
The module's goal is the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$: winding is a left inverse to the fundamental cycle, using simplexDisplacement_boundary (kills boundaries) and the once-around generator. Surjectivity still needs a simplicial prism operator Mathlib does not yet supply. No downstream consumers are wired yet; the declaration is infrastructure for that generation half and for any algebraic consumer of a free prism nullhomotopy.
In the Recognition forcing chain this sits under the T8 spatial-dimension / circle-homology package: a fully formal $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ is the topological input that locks the eight-tick octave geometry to three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.