circleH1ZIsoInt_of_explicitRawPrism
plain-language theorem explainer
If every oriented cyclic family on S¹ admits a fully explicit raw prism 2-chain whose boundary cancels the oriented edge sum against a multiple of the fundamental cycle, then Mathlib's integer singular homology satisfies H₁(S¹;ℤ) ≅ ℤ. Cite this when discharging the generation half of the circle comparison from concrete prism data. The proof is a one-line reduction: package the explicit prisms as raw prisms, then apply the raw-prism iso theorem.
Claim. Assume decidable equality on singular $0$- and $1$-simplices of $S^1$. If for every oriented cyclic family $T$ there exist $n\in\mathbb{Z}$ and a singular $2$-chain $b$ with $\partial b$ equal to the free $1$-chain of the oriented edges of $T$ minus $n$ times the fundamental $1$-cycle, then the Mathlib comparison isomorphism $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ holds.
background
This module lifts path-level winding on $S^1$ to singular simplices of TopCat.sphere 1. Displacement of a singular $1$-simplex is path displacement after reparameterizing $\Delta^1$ to $[0,1]$. The key identity is that displacement kills boundaries: for any singular $2$-simplex the alternating face sum of displacements vanishes, by convexity of $\Delta^2$ and homotopy invariance of path displacement. Together with the fact that the fundamental loop has winding $1$, this gives a left inverse $H_1(S^1;\mathbb{Z})\to\mathbb{Z}$.
Surjectivity (every $1$-cycle homologous to an integer multiple of the fundamental cycle) needs prism/subdivision data Mathlib does not yet supply. The hypothesis here is the fully explicit raw form of that prism target: for each concrete oriented cyclic family term, a singular $2$-chain whose boundary is the raw oriented edge sum minus a matching fundamental-cycle multiple. Singular $0$- and $1$-simplices are the actual vertices of the singular simplicial set of the sphere.
Upstream, the packaged raw-prism generation hypothesis already implies the iso via boundary generation and the oriented-cyclic-family comparison. Explicit raw prisms imply packaged raw prisms by a direct unpacking.
proof idea
One-line term wrapper. Apply orientedCyclicFamilies_rawPrism_generate_of_explicit to the given explicit-prism hypothesis, obtaining the packaged raw-prism generation hypothesis. Feed that into circleH1ZIsoInt_of_rawPrism, which itself reduces raw prisms to oriented-cyclic-family boundary generation and thence to the Mathlib circle $H_1$ isomorphism. No extra algebraic work occurs at this layer.
why it matters
Closes one step in the prism ladder that finishes the generation half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ inside Mathlib singular homology. The module already has the split-injective half from winding kills boundaries plus winding of the fundamental loop; what remains is surjectivity of the integer comparison, which needs prism fillings for oriented cyclic families.
Downstream, circleH1ZIsoInt_of_freePrism cites this theorem: a free-coordinate prism construction is converted to an explicit raw prism and then handed here. That free-prism form is the practical discharge point for concrete geometric constructions.
In the Recognition foundation stack this is pure topological scaffolding for the circle as the eight-tick / octave carrier (T7), not a physics identity itself. It does not touch J-uniqueness, $\varphi$, or the mass ladder; it only certifies that the integer homology of the geometric circle matches the expected $\mathbb{Z}$ generator used by winding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.