aW_mem_arcA
plain-language theorem explainer
The distinguished east point of the doubly punctured unit circle lies on the open east arc. Anyone computing the integer pairing of the point-difference class against the east-arc augmentation cites this membership. The proof is a three-line reduction: unfold the arc predicate, rewrite the ambient first coordinate of the east pole to 1, and apply positivity of one.
Claim. Let $W_c$ be the doubly punctured unit circle (unit $S^1$ minus north and south poles), let $a_W\in W_c$ be the east point, and let $\mathrm{arc}_A=\{w\in W_c:\mathrm{coord}_W(w)>0\}$ be the open east arc. Then $a_W\in\mathrm{arc}_A$.
background
The module builds singular-sphere geometry used in the foundation layer: the unit sphere $S^n$ in Euclidean space, open covers by deleting poles, and the doubly punctured circle $W_c$ obtained by removing north and south from $S^1$. Points of $W_c$ carry an ambient first coordinate $\mathrm{coord}_W(w)=\mathrm{amb}(w)_0$, where $\mathrm{amb}$ is the coercion from the sphere subtype into Euclidean space.
The east point $a_W$ is the image of the standard east pole $\mathrm{eastP}$ (the basis vector $e_0$) inside the intersection of the two cover charts. The east arc $\mathrm{arc}_A$ is the open half of $W_c$ on which that first ambient coordinate is strictly positive; its complement is the west arc. An upstream computation records $\mathrm{amb}(\mathrm{eastP})_0=1$.
These sets feed a Čech/singular pairing: the point-difference class of the two intersection points is tested against the characteristic class of a clopen arc.
proof idea
Membership in $\mathrm{arc}_A$ is definitionally $0<\mathrm{coord}_W(a_W)$. Unfolding $\mathrm{coord}_W$ and $a_W$ yields the ambient first coordinate of $\mathrm{eastP}$. The lemma $\mathrm{amb_eastP_zero}$ rewrites that coordinate to $1$, and $\mathtt{one_pos}$ finishes. Pure term-mode reduction; no case splits.
why it matters
The sole downstream consumer is $\mathrm{diffClass_pairing}$, which proves that the point-difference class pairs to $1$ (hence is nonzero) against the east-arc augmentation: the proof branches on membership of the two intersection points in $\mathrm{arc}_A$, taking the positive branch exactly via this lemma and the negative branch via the companion non-membership of the west point.
In the Recognition foundation stack this is local singular geometry supporting the discrete homology of the eight-tick / octave picture (T7) and the sphere geometry that later forces $D=3$ (T8). It does not itself invoke the J-cost or the Recognition Composition Law; it only certifies a concrete generator needed for the pairing identity that keeps the difference class alive in $H_0$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.