circleH1ZIsoInt_of_pathConeCorrection
plain-language theorem explainer
Assuming every oriented cyclic family admits a 2-chain correcting the path-cone residual, the integer singular homology of the circle is isomorphic to ℤ. Anyone closing the Mathlib H₁(S¹;ℤ) ≅ ℤ computation via the winding/prism pipeline would cite this. The proof is a one-line term wrapper: convert the path-cone correction hypothesis into free-prism generation, then apply the free-prism form of the iso.
Claim. Assume decidable equality on singular $0$- and $1$-simplices of $S^1$. If for every oriented cyclic family $T$ there exist an integer $n$ and a singular $2$-chain $K$ whose boundary equals the path-cone residual of $T$ at $n$, then $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ in the Mathlib singular-homology sense.
background
The module lifts path-level winding on $S^1$ to singular $1$-simplices: simplexDisplacement reparameterizes $\Delta^1$ to $[0,1]$ and takes path displacement ($2\pi$ times winding). The key identity is that alternating face sums of displacements vanish on every singular $2$-simplex (winding kills boundaries), by convexity of $\Delta^2$ and homotopy invariance of path displacement. With the fundamental loop mapping to winding $1$, this gives the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
Surjectivity needs a generation statement: every $1$-cycle is homologous to an integer multiple of the fundamental cycle. Mathlib lacks a built-in simplicial prism/subdivision operator, so the project builds generation through a ladder of targets. The path-cone correction target asks, for each oriented cyclic family $T$, for a $2$-chain $K$ whose boundary is the residual between the summed path-cone boundary and the desired free-prism boundary. The free-prism target is the next rung; the final package is circleH1ZIsoInt in the Mathlib cohomology bridge.
proof idea
Pure term-mode composition of two upstream results. First apply orientedCyclicFamilies_freePrism_generate_of_pathConeCorrection to the hypothesis hcorr: for each family $T$ one obtains $n$ and a residual filler $K$, then packages the free-prism witness as the path-cone chain minus $K$. Feed that free-prism generation proof into circleH1ZIsoInt_of_freePrism, which itself reduces through the explicit-raw-prism rung to the full Mathlib iso. No new algebraic work occurs at this node.
why it matters
This is the top of the path-cone branch of the circle $H_1$ generation ladder in CircleWindingChain. The module doc states that winding already supplies the left-inverse (split-injective) half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$; the missing half is generation of cycles by the fundamental class. By showing that the residual path-cone correction target alone discharges the free-prism target and hence the full iso, the declaration collapses one checklist item into the Mathlib comparison map.
No downstream consumers are recorded yet (used_by is empty), so the result is presently a terminal packaging theorem rather than an intermediate lemma. In the broader Recognition foundation it anchors the topological side of the eight-tick/octave story (T7): integer winding on $S^1$ is the homology avatar of the discrete period that later feeds dimensional and clock arguments. It does not itself invoke J-cost, $\varphi$, or the forcing chain T5–T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.