diffClass
plain-language theorem explainer
The point-difference class is the degree-zero singular homology class of the east point minus that of the west point on the doubly punctured circle. Algebraic topologists running the Mayer-Vietoris argument for nonzero first homology of the circle cite it as the intersection generator that pairs to one. It is defined by subtracting the two point-class morphisms into H_0 of the intersection.
Claim. Let $W_c$ be the doubly punctured circle $U\cap V$ on $S^1$. Write $[a]$ and $[b]$ for the degree-$0$ singular homology classes (with $\mathbb{Z}$ coefficients) of the east and west points of $W_c$. The point-difference class is the morphism $\mathbb{Z}\to H_0(W_c)$ given by $[a]-[b]$.
background
The ambient space is the unit circle $S^1$, covered by two open arcs whose intersection $W_c$ is a doubly punctured circle (two disjoint open arcs). The east and west points sit one in each component of that intersection.
Degree-$n$ singular homology $H_n(X;\mathbb{Z})$ is packaged as an object of the category of $\mathbb{Z}$-modules. The degree-$0$ class of a point $x\in X$ is the morphism $\mathbb{Z}\to H_0(X)$ induced by the chain map that sends $1$ to the singular $0$-simplex at $x$.
Local setting is the singular-sphere geometry module: open covers of $S^1$, their intersection, and the Mayer-Vietoris sequence that relates $H_*(S^1)$ to the homology of the two arcs and of $W_c$.
proof idea
One-line definitional wrapper. Form the degree-$0$ point class of the east point of $W_c$, form the degree-$0$ point class of the west point, and subtract in the abelian group of morphisms $\mathbb{Z}\to H_0(W_c)$. No further lemmas are applied at the definition site.
why it matters
This class is the concrete generator that makes the Mayer-Vietoris argument for $H_1(S^1)\neq 0$ work. Downstream, the pairing lemma shows it pairs to $1$ against the east-arc augmentation, hence is nonzero; the companion lemma shows it dies under the map into $H_0(U)\oplus H_0(V)$ because both points become joinable inside each punctured arc. Exactness then forces the connecting map out of $H_1(S^1)$ to be nonzero, so $H_1(S^1)$ itself cannot vanish.
In the Recognition foundation stack this is pure topological scaffolding: it underwrites the circle's first homology before any physics constants or forcing-chain steps are attached. Parent results are the pairing identity, the vanishing under the Mayer-Vietoris pair map, and the theorem that $H_1(S^1)$ is not the zero module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.