orientedCyclicFamilies_rawPrism_generate_of_explicit
plain-language theorem explainer
If every oriented cyclic family admits an explicit singular 2-chain whose boundary is the raw signed edge sum minus a fundamental-cycle multiple, then the packaged raw-prism target holds for those families. Cited by anyone routing an explicit prism construction into the generation half of H₁(S¹;ℤ) ≅ ℤ. Proof is a short term rewrite: unpack the explicit witness and apply the cycle-object/edge-sum identification.
Claim. Suppose that for every oriented cyclic family $T$ there exist an integer coefficient $n$ and a singular $2$-chain $b$ on $S^1$ such that $\partial b$ equals the free-to-chain image of the signed edge sum of $T$ minus $n$ times the fundamental $1$-cycle. Then for every such $T$ there exist $n$ and $b$ with $\partial b$ equal to the cycles-inclusion image of $T$'s directed free cycle term minus that same multiple of the fundamental cycle.
background
This module lifts path-level winding on the circle to singular simplices of $\mathrm{TopCat.sphere},1$. Displacement of a singular $1$-simplex is path displacement after reparameterizing $\Delta^1$ to the unit interval. The key identity is that alternating face sums of displacements vanish on every singular $2$-simplex (winding kills boundaries), so the invariant descends to homology and splits the fundamental class: the injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
The surjective/generation half needs a prism (or subdivision) filling: every oriented closed walk must be homologous to an integer multiple of the fundamental cycle. Two Prop-targets package that demand. The fully explicit raw form asks for a $2$-chain whose boundary is the concrete signed edge sum minus $n$ times the fundamental cycle. The packaged raw form asks the same with the family's cycle object under the cycles inclusion in place of that edge sum.
Upstream, the explicit target is the form a geometric prism construction should prove directly; the packaged target is the form later comparison lemmas consume.
proof idea
Term-mode implication, not a geometric argument. Fix an oriented cyclic family $T$. Apply the explicit hypothesis to obtain $n$ and a singular $2$-chain $b$ with the free-to-chain edge-sum boundary identity. Reuse the same $n$ and $b$. Rewrite the packaged right-hand side via the already-proved equality identifying the cycles-inclusion image of $T$'s directed free cycle with the oriented edge-sum chain. The explicit boundary equation then matches the packaged target exactly.
why it matters
This is the coordinate-change bridge between the form a singular prism construction naturally produces and the form the homology pipeline consumes. Downstream, circleH1ZIsoInt_of_explicitRawPrism feeds the explicit hypothesis through this lemma into the packaged raw-prism route and obtains the final Mathlib circle $H_1$ isomorphism. The same pattern closes zero-winding filling via zeroWindingCycles_bound_of_explicitRawPrism.
It also sits inside the free/raw equivalence: after free-coordinate and raw packaged targets are identified, and raw is tied to zero-winding bounds, the only remaining content is the geometric prism itself, not bookkeeping of coordinates. In the module's program this is the last algebraic reduction before the generation half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ is discharged. No Recognition forcing-chain step (T0–T8) is invoked here; the landmark is classical singular homology of the circle, used as foundation infrastructure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.