trigCircleVector_mem_sphere
plain-language theorem explainer
The ambient trigonometric vector (cos t, sin t) lies on the exact metric unit circle in R^2 that Mathlib uses for TopCat.sphere 1. Anyone packaging continuous maps or singular simplices into that sphere cites this membership lemma. The proof is a short norm-squared calculation via cos^2+sin^2=1, closed by nlinarith.
Claim. For every real $t$, the Euclidean vector $(\cos t, \sin t)$ belongs to the metric sphere of radius $1$ centered at the origin in $\mathbb{R}^2$ (the ambient space of Mathlib's topological $1$-sphere).
background
This module begins a by-hand circle-$H_1$ derivation 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 space is Euclidean $\mathbb{R}^2$ (Mathlib EuclideanSpace R (Fin 2)), the precise ambient type behind TopCat.sphere 1. The trigonometric vector is the standard map $t \mapsto (\cos t, \sin t)$ into that ambient space. Membership in the metric unit sphere is the gate that lets one form a point of the topological sphere via the ULift carrier Mathlib uses.
proof idea
Unfold sphere membership to dist v 0 = 1, then rewrite to ‖v‖ = 1. Compute ‖v‖^2 via the Euclidean sum-of-squares formula on Fin 2: the two coordinates are cos and sin, so the sum is cos^2 t + sin^2 t = 1. With ‖v‖ ≥ 0, nlinarith upgrades the squared-norm identity to the norm identity.
why it matters
This is the membership certificate that turns the ambient trigonometric vector into a genuine point of Mathlib's TopCat.sphere 1. The immediate consumer is the once-around parametrization point, defined as ULift.up of the subtype pair (vector, this membership). Continuity of that point map, and all later singular-simplex constructions in the circle-$H_1$ program, sit on top of this fact.
In the Recognition foundation stack the goal is an exact, machine-checked generator of $H_1(S^1)$, not a hand-waved loop. Anchoring the trig parametrization to the real metric sphere (rather than an isomorphic copy) keeps face maps and singular-set identities aligned with Mathlib's topology library. No forcing-chain landmark (T5–T8) is invoked here; the lemma is pure geometric scaffolding for that later topological step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.