sphereOneBaseVector
plain-language theorem explainer
The ambient first standard basis vector (1,0) in the Euclidean plane underlying Mathlib's unit circle S¹. Anyone wiring a checked basepoint or trigonometric parametrization of TopCat.sphere 1 cites this. It is a one-line definition via EuclideanSpace.single on Fin 2.
Claim. Let the ambient space of Mathlib's unit circle $S^1$ be the Euclidean plane $\mathbb{R}^2$. Define the ambient base vector to be the first coordinate unit vector $e_0=(1,0)\in\mathbb{R}^2$.
background
The CircleParam module begins a by-hand derivation of circle $H_1$ against the imported TopCat.sphere 1 object. 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 must live in the same singular set and use the same face maps.
The ambient type is the Euclidean space $\mathbb{R}^{\mathrm{Fin},2}$. Mathlib's sphere object wraps the metric unit sphere in that plane under a ULift. The first coordinate unit vector is the natural choice of ambient representative before packing into the subtype and the topological sphere point.
proof idea
Pure definition: the ambient vector is EuclideanSpace.single (0 : Fin 2) (1 : ℝ), i.e. the standard basis vector with a 1 in coordinate 0 and 0 elsewhere. No proof obligations at this declaration.
why it matters
This is the ambient seed for the checked basepoint of TopCat.sphere 1. Downstream, membership on the metric unit sphere is proved from it, then the basepoint is assembled as the ULift of that subtype pair. The trigonometric circle map is shown to start at and return to that same basepoint at $t=0$ and $t=2\pi$, so the once-around loop is pinned to a single concrete point in Mathlib's sphere object.
In the Recognition foundation stack this is scaffolding for the circle-$H_1$ generator against the real singular simplicial set, not yet a forcing-chain step (T0–T8). It closes the gap between abstract $S^1$ and an explicit Euclidean representative usable in later singular-simplex constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.