diffClass_pairing
plain-language theorem explainer
The point-difference class on the doubly punctured circle pairs to 1 against the east-arc degree-0 augmentation, hence is nonzero in H₀. Anyone proving H₁(S¹) ≠ 0 via Mayer–Vietoris cites this pairing. The proof is a short rewrite: expand the difference of point classes, apply the point–augmentation lemma twice, and cancel.
Claim. On the doubly punctured circle $W_c$, the composition of the point-difference class with the degree-$0$ homology augmentation against the east arc equals the identity morphism $\mathrm{id}:\mathbb{Z}\to\mathbb{Z}$ (as $\mathbb{Z}$-modules).
background
The ambient space is the unit circle $S^1$, covered by two open arcs whose intersection is the doubly punctured circle $W_c$. The east arc $A\subset W_c$ is the clopen set of points with positive angular coordinate; it is the test set for a degree-$0$ augmentation.
In this module, singular homology is valued in $\mathbb{Z}$-modules. The augmentation $\mathrm{aug}_H(X,A)$ against a clopen $A$ is the degree-$0$ map $H_0(X)\to\mathbb{Z}$ that counts the algebraic mass of a $0$-cycle on $A$. Upstream, the point-class pairing lemma states that a point $x$ pairs to $1$ if $x\in A$ and to $0$ otherwise.
The point-difference class is the $H_0(W_c)$ class of one distinguished intersection point minus the other (east minus west). The companion observation is that this same difference dies in $H_0(U)\boxplus H_0(V)$, because each cover component joins the two points.
proof idea
Term-mode rewrite proof. Unfold the difference class as a difference of two point classes and distribute composition over subtraction (Preadditive.sub_comp). Apply the upstream point–augmentation pairing twice: the east point lies in the east arc, so its pairing is $\mathrm{id}$; the west point does not, so its pairing is $0$. The difference collapses by sub_zero to the identity on $\mathbb{Z}$.
why it matters
This lemma is the nonzero witness that powers h1_s1_ne_zero: if $H_1(S^1)$ vanished, the Mayer–Vietoris connecting map out of it would be zero, and exactness would force the point-difference class to vanish in $H_0(W_c)$, contradicting the pairing to $1$. Downstream doc: “If it vanished, the Mayer-Vietoris connecting map out of it would be zero, and exactness would kill the point-difference class, contradicting its nonzero pairing.”
In the Recognition foundation stack this is geometric scaffolding for the circle/octave topology (eight-tick period $2^3$, $D=3$ forcing chain neighbors), not a physical constant claim. It closes the algebraic topology step that $H_1(S^1)\neq 0$ inside the singular-sphere development.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.