circleH1ZIsoInt_of_rawPrism

This module lifts the path-level winding/displacement invariant of the circle to singular simplices of TopCat.sphere 1 and proves that winding kills boundaries: for every singular $2$-simplex the alternating face sum of displacements vanishes. Together with the fact that the once-around generator has winding $1$, that gives the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The remaining generation half (every $1$-cycle homologous to an integer multiple of the fundamental cycle) needs a simplicial prism/subdivision operator that Mathlib singular homology does not yet supply.

The raw-prism generation hypothesis states exactly the chain-level prism target an explicit construction should hit: for each oriented cyclic family term $T$, there exist an integer $n$ and a singular $2$-chain $b$ with $\partial b$ equal to the directed cycle of $T$ minus $n$ times the fundamental cycle (as a cycle object). Singular $0$- and $1$-simplices are the actual vertices and edges of the singular simplicial set of $S^1$.

Upstream, boundary generation from raw prisms is pure categorical transport through the inclusion of cycles; the oriented-family criterion then reduces the Mathlib circle $H_1$ isomorphism to that generation statement.

One-line term-mode wrapper. First apply orientedCyclicFamilies_boundary_generate_of_rawPrism to the raw-prism hypothesis, obtaining the cycle-object generation target (for each oriented cyclic family, a $2$-chain whose boundary realizes the closed walk minus a multiple of the fundamental cycle, after transport into cycles). Then feed that into circleH1ZIsoInt_of_orientedCyclicFamilies, which itself reduces through the fundamental-cycle generation lemma to the Mathlib bridge isomorphism circleH1ZIsoInt. No new algebraic work occurs here.

This is the middle rung of the prism-generation ladder that closes the surjectivity half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ against Mathlib's singular homology. Downstream, circleH1ZIsoInt_of_explicitRawPrism specializes the hypothesis further to a fully explicit raw-prism filling and cites this theorem as the sole step. The module doc frames the open gap: Mathlib lacks a built-in simplicial prism/subdivision operator, so the project must supply generation by hand; this declaration isolates that remaining obligation at the raw-chain level rather than at the more abstract cycle-object level. In the Recognition foundation stack it anchors the winding homomorphism as a true homology invariant with integer comparison, the topological backbone for later octave and forcing-chain arguments that treat $S^1$ periods as discrete recognition ticks.