h1_s1_ne_zero
plain-language theorem explainer
The first singular homology of the circle is nonzero as an abelian group. Anyone building the Stage D nonvanishing of top sphere homology cites this base case. The argument is a short exactness chase: vanishing would force the Mayer–Vietoris connecting map to kill the integer point-difference class, contradicting its unit pairing under the arc augmentation.
Claim. The first singular homology group of the unit circle $S^1\subset\mathbb{R}^2$ is not the zero group: $H_1(S^1)\neq 0$.
background
The ambient module builds singular homology of Euclidean spheres inside Recognition Science Stage D. Sph n is the unit sphere in Euclidean space of dimension $n+1$, viewed as a topological space; here $n=1$ is the ordinary circle.
The cover is the standard two-chart open cover of $S^1$ by northern and southern arcs (complements of the south and north poles). Mayer–Vietoris supplies a long exact sequence relating the homology of the two opens, their intersection, and the whole sphere. The connecting homomorphism $\delta$ out of $H_1(S^1)$ is the map used below.
A distinguished class is the integer point-difference (or degree) class on the intersection; its pairing against a fixed clopen arc via the augmentation map evaluates to $1\in\mathbb{Z}$. Upstream, one_ne_zero records that $1\neq 0$ in $\mathbb{Z}$, and mv_exact₁ packages exactness of the relevant short complex in the module category.
proof idea
Assume for contradiction that $H_1(S^1)$ is the zero object. Then every map out of it vanishes, so the Mayer–Vietoris connecting map $\delta$ at degree $0$ is the zero map.
Exactness of the Mayer–Vietoris short complex (mv_exact₁, rewritten via the module-category exactness criterion) says that a class in the middle term lies in the image of $\delta$ precisely when it is killed by the pair map. The point-difference class is killed by that pair map (by the identity relating pair and difference), hence equals $\delta(w)$ for some $w$.
But $\delta$ is zero, so the class is zero. Pushing through the arc augmentation pairing then yields $1=0$ in $\mathbb{Z}$, contradicting one_ne_zero.
why it matters
This is the $n=1$ base case for Stage D: nonvanishing of top-dimensional singular homology of spheres. The sole direct consumer is sphere_top_ne_zero, which states that for every $n\ge 1$, $H_n(S^n)\neq 0$, proved by induction on dimension with this circle fact as the starting step.
In the Recognition forcing chain, Stage D sits after the pre-temporal stages and supplies the topological input that spheres carry a nontrivial fundamental class. That nonvanishing underwrites orientation, degree, and linking arguments used later when spatial dimension is forced to $D=3$ (T8) and when eight-tick octave structure meets geometric cycles. Without $H_1(S^1)\neq 0$, the inductive lift to higher spheres collapses and the geometric half of the foundation chain loses its generator.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.