aW
plain-language theorem explainer
Packages the east point of the unit circle as a point of the doubly punctured circle W_c (the U∩V cover intersection). Downstream homology constructions cite it as one endpoint of the H_0 point-difference class. The body is the subtype pair of eastP with its intersection-membership proof.
Claim. Let $W_c$ be the doubly punctured unit circle, realized as the intersection of the two standard open covers of $S^1$. Then $a_W\in W_c$ is the east point $(1,0)$, viewed as an element of that intersection.
background
The ambient space is the unit sphere $S^1$ in the Euclidean plane. Two open covers coverU and coverV remove opposite poles, so their intersection is a doubly punctured circle: two open arcs meeting at the east and west equatorial points.
Wc is that intersection promoted to a TopCat space. The east point eastP is the standard basis vector $e_0$ on the sphere; the lemma eastP_mem_inter records that it lies in both covers, hence in the intersection.
This module builds singular-sphere geometry used to extract a nontrivial $H_0$ class from the two-arc cover, in the style of a Mayer–Vietoris connecting argument on $S^1$.
proof idea
One-line subtype constructor: pair the already-defined east point with the lemma that it belongs to coverU 1 ∩ coverV 1. No further proof work; the membership obligation is discharged by eastP_mem_inter.
why it matters
Supplies one of the two basepoints of the intersection used to form diffClass := ptH W_c a_W - ptH W_c b_W, the integer point-difference class in $H_0(W_c)$. That class is shown nonzero by pairing against the east-arc augmentation (diffClass_mvPair and related lemmas), and it dies under the Mayer–Vietoris map into $H_0(U)\oplus H_0(V)$ because both points become path-connected inside each punctured cover.
Also feeds aW_mem_arcA, which places the point on the positive arc needed for the pairing. In the broader Recognition foundation this is pure topological scaffolding for singular-sphere / cover arguments, not a forcing-chain step (T0–T8) itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.