bW_notMem_arcA
plain-language theorem explainer
The west intersection point on the doubly punctured circle lies outside the open east arc. Anyone building the point-difference class in H₀ needs this membership fact so the east-arc augmentation evaluates to zero on that point. The proof reduces the coordinate of the west point to −1 and checks −1 ≰ 0.
Claim. Let $b_W$ be the west point of the two-arc intersection on the doubly punctured unit circle, and let $\mathrm{arc}_A=\{w:0<\mathrm{coord}_W(w)\}$ be the open east arc. Then $b_W\notin\mathrm{arc}_A$.
background
The module develops singular-sphere geometry used to realize distinction and homology data on the circle. Points live in the unit sphere Sph 1 inside Euclidean space Esp 1; amb is the ambient-coordinate coercion of a sphere point.
The doubly punctured circle carries a real coordinate coordW. The open east arc is the positive half {w | 0 < coordW w}. The west point bW is the sphere point westP packaged as a member of the two-arc intersection. An upstream computation records that the zeroth ambient coordinate of westP equals $-1$.
Locally one only needs the sign of that coordinate: membership in the east arc is exactly positivity of coordW.
proof idea
Unfold non-membership in arcA to the negation $0 < \mathrm{coord}_W(b_W)$. By definition the coordinate of $b_W$ is the zeroth ambient coordinate of westP. Rewrite that coordinate via amb_westP_zero to $-1$, then finish with norm_num ($-1$ is not strictly positive).
why it matters
Feeds diffClass_pairing, which shows that the point-difference class in $H_0$ pairs to $1$ against the east-arc augmentation (hence is nonzero). The pairing proof subtracts the two point evaluations and uses if_neg bW_notMem_arcA so the west contribution vanishes while the east point contributes $1$.
In the Recognition foundation this is a small but necessary geometric fact: the two intersection points of the cover must sit on opposite sides of the arc cut so that the difference class is nontrivial in reduced homology. It sits in the singular-sphere scaffolding that supports later distinction and forcing-chain geometry, not a T0–T8 landmark itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.