circleH1ZIsoInt_of_freePrism
plain-language theorem explainer
A free-coordinate prism filling for every oriented cyclic family is enough to obtain the Mathlib isomorphism $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. Anyone discharging the generation half of the circle homology computation cites this reduction. The proof is a one-line term wrapper: free-prism data is transported to an explicit raw prism, then the prior explicit-raw-prism theorem applies.
Claim. Assume decidable equality on singular $0$- and $1$-simplices of $S^1$. If every oriented cyclic family admits a free-coordinate prism filling (an explicit free $C_2$ chain whose free boundary equals the oriented edge sum minus the free-coordinate image of the matching fundamental cycle), then the Mathlib bridge isomorphism $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ holds.
background
This module lifts the path-level winding/displacement invariant of CircleWinding to singular simplices of $\mathrm{TopCat.sphere},1$. The key chain-level fact is that simplex displacement kills boundaries: for every singular $2$-simplex the alternating face sum of displacements vanishes, by $2$-simplex telescoping inside the convex standard simplex plus path additivity and homotopy invariance. Together with the once-around generator mapping to $1$, that gives the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
The converse (generation: every $1$-cycle is homologous to an integer multiple of the fundamental cycle) needs a simplicial prism/subdivision operator that Mathlib singular homology does not yet supply. The free-prism target is the cleanest hand-built finite prism hypothesis: for each oriented cyclic family term $T$, there exist $n$ and a free $C_2$ chain $B$ with free boundary equal to $\sum_i (T.o,i).\mathrm{chain}$ minus the free image of the matching fundamental cycle.
Singular $0$- and $1$-simplices here are the actual objects of $\mathrm{TopCat.toSSet}$ on the sphere, not project-local replacements. The residual import is incidental to the bridge stack and plays no role in the argument.
proof idea
One-line term wrapper. Apply the conversion lemma that turns a free-coordinate prism hypothesis into a fully explicit raw-prism generation hypothesis (transport the free $C_2$ boundary through Mathlib's raw chain complex via the free-to-chain map). Feed that witness into the upstream theorem stating that an explicit raw prism filling for each oriented cyclic family already yields the Mathlib circle $H_1$ isomorphism. No new algebraic work occurs at this layer.
why it matters
This sits in the generation half of the circle homology computation that the module doc identifies as still open relative to Mathlib: injectivity of the winding comparison is already in hand; surjectivity needs prism fillings. The declaration lowers the bar from fully explicit raw prisms to free-coordinate prisms, the cleanest target for a finite hand construction.
Downstream, the path-cone residual correction theorem cites it: path-cone correction data is reduced to free-prism generation, then this result closes $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. That isomorphism is the topological backbone for winding as a homology invariant on the circle, which underwrites the eight-tick octave bookkeeping (T7) and the integer comparison map used elsewhere in the foundation stack. No Recognition forcing step (T5–T8) is proved here; the contribution is the pure topological comparison.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.