Pith. sign in
theorem

h1_s1_ne_zero

proved
show as:
module
IndisputableMonolith.Foundation.SingularSphereGeometry
domain
Foundation
line
633 · github
papers citing
none yet

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.