sphereOneBaseVector_mem_sphere
plain-language theorem explainer
The first standard basis vector of the Euclidean plane lies on the unit circle about the origin. Anyone assembling Mathlib's exact TopCat.sphere 1 basepoint cites this membership. The proof rewrites sphere membership as a distance identity and closes by simplification of the Euclidean norm.
Claim. The first coordinate unit vector $e_0=(1,0)$ in Euclidean space $\mathbb{R}^{\mathrm{Fin}\,2}$ belongs to the metric sphere of radius $1$ centered at the origin.
background
This module starts a by-hand circle-$H_1$ derivation against the imported Mathlib object TopCat.sphere 1. It fixes the exact carrier, a checked basepoint, and constant singular 1-simplex face identities in the singular simplicial set of that sphere. The constant simplex is only an API anchor: later once-around simplices are meant to live in the same singular set with the same face maps.
The ambient space is Euclidean space $\mathbb{R}^2$ on Fin 2. The base vector is the first-coordinate unit vector obtained by placing $1$ in slot $0$. Metric-sphere membership means distance to the origin equals radius $1$.
proof idea
Sphere membership is definitionally the equality $\mathrm{dist}(v,0)=1$. The proof changes the goal to that distance identity for the single-coordinate unit vector, then finishes with simp, which evaluates the Euclidean norm of the standard basis vector to $1$.
why it matters
Downstream, the exact basepoint of TopCat.sphere 1 is the ULift of the subtype pair consisting of this vector and this membership proof. That basepoint is the first checked anchor for the module's singular-set face identities and for later once-around simplices in the same carrier.
In the broader Recognition Foundation stack this is pure Euclidean bookkeeping that makes the imported sphere object usable without ad-hoc casts. It does not itself touch the forcing chain (T0-T8), the Recognition Composition Law, or the eight-tick octave; it only supplies a verified geometric basepoint those later constructions can sit on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.