circleH1MathlibComputationOfGeometricBridge
plain-language theorem explainer
Assuming the geometric chain-level bridge (singular chains of the circle homotopy-equivalent to the ordinary two-cell cellular model), the Mathlib computation certificate that $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ is filled. Anyone wiring the strict T8 handoff cites this. Proof is a one-line term: feed the bridge-derived integer isomorphism into the certificate constructor.
Claim. If Mathlib's singular chain complex of $\mathrm{TopCat.sphere}\,1$ is chain-homotopy equivalent to the ordinary two-cell cellular circle model, then the Mathlib computation certificate holds: the singular-homology API is available, the target object is the imported $H_1(S^1;\mathbb{Z})$, and that group is isomorphic to $\mathbb{Z}$.
background
This module is the local workbench for the missing computation $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. It does not replace Mathlib's sphere object and does not feed the strict T8 bridge until a real equivalence to the imported singular homology object is proved. The algebraic core already shows that a chain complex supported by $\mathbb{Z}$ in degree 1 has degree-1 homology $\mathbb{Z}$.
The geometric bridge is the remaining chain-level hypothesis: a nonempty homotopy equivalence between Mathlib's singular integer chain complex of the circle and the ordinary two-cell cellular circle model. From that bridge one immediately obtains the strong target isomorphism used by the cohomology bridge module.
CircleH1MathlibComputation is the final import interface: singular-homology API available, target identity pinned to the imported circle $H_1$, and an explicit isomorphism to $\mathbb{Z}$. A companion lemma says any proof of that strong iso fills the certificate, since API availability and target identity are already import-checked.
proof idea
One-line term proof. Apply circleH1MathlibComputation_of_iso_int to the isomorphism produced by circleH1ZIsoIntOfGeometricBridge h. The latter unpacks the nonempty homotopy equivalence and routes through the ordinary-cellular-at-one comparison; the former packages the resulting circleH1ZIsoInt into the three-field certificate structure (API flag, target identity by rfl, and the iso).
why it matters
Doc-comment places this as the filler of the Mathlib computation certificate used by the strict T8 handoff. In the Recognition forcing chain, T8 forces $D=3$ spatial dimensions; the circle $H_1$ computation is the topological atom that handoff depends on. No downstream declarations currently use this theorem (used_by is empty), so it sits at the tip of the geometric-bridge branch: once the bridge Prop is discharged, this term immediately yields the certificate the T8 path expects. It does not invent a project-local homology; it insists the target is Mathlib's imported singular $H_1$ of the sphere.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.