diffClass_mvPair
plain-language theorem explainer
The point-difference class in degree-0 homology of the two-chart intersection on S¹ maps to zero under the Mayer-Vietoris pair map into H₀(U) ⊕ H₀(V). Anyone running the exactness argument for H₁(S¹) ≠ 0 cites this vanishing. The proof equates the two point classes inside each path-connected punctured cover and cancels both biproduct legs.
Claim. For the standard open cover $U,V$ of $S^1$, the point-difference class in $H_0(U \cap V)$ composes with the Mayer-Vietoris pair map $H_0(U \cap V) \to H_0(U) \oplus H_0(V)$ to give the zero morphism. Equivalently, both points of the difference become homologous inside each chart.
background
The ambient module builds singular homology of spheres via an open two-chart cover of $S^1$: northern and southern punctured arcs coverU 1 and coverV 1, whose intersection is a pair of open arcs. The Mayer-Vietoris pair map sends a class $c$ in $H_n(U \cap V)$ to $([i_*c], -[j_*c])$ in the biproduct $H_n(U) \oplus H_n(V)$, induced by the space-level inclusions of the intersection into each chart.
The point class ptH is the degree-0 homology class of a chosen basepoint. The point-difference class is the difference of two such classes (the two connected components of the intersection). Upstream, path-joining of points yields equality of their degree-0 classes (ptH_eq_of_joined), and point classes are natural under continuous maps (ptH_natural).
proof idea
Two preliminary equalities: the images of the two intersection points under the inclusion into $U$ are path-joined in $U$, so ptH_eq_of_joined equates their ptH classes in $H_0(U)$; likewise in $V$. Then biprod.hom_ext splits the claim into the two legs of the biproduct. On the first leg, unfold the pair map and the difference class, push ptH through the inclusions by naturality, replace by the joined equality, and cancel by sub_self. On the second leg the same calculation appears with a sign, and neg_zero finishes.
why it matters
This vanishing is the exactness input for h1_s1_ne_zero: if $H_1(S^1)$ were zero, the Mayer-Vietoris connecting map out of it would vanish, exactness would force the point-difference class itself to zero, and that contradicts its nonzero pairing against a clopen augmentation. The parent theorem's doc-comment states the argument explicitly.
In the Recognition framework this is pure foundation: nonvanishing of $H_1(S^1)$ underwrites the circle as a nontrivial 1-cycle, which sits behind the eight-tick octave (T7, period $2^3$) and the topological side of the forcing chain. The lemma itself is local algebraic topology; its payload is the nonzero generator that later geometry and Clifford/Bott identifications consume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.