pt2
plain-language theorem explainer
Constructs the Euclidean plane point with coordinates (a, b) as an element of the ambient space of the circle S¹. Downstream circle-membership and coordinate lemmas cite it, as does the semicircle arc map used in high-dimensional linking-vanishing arguments. The body is a one-line embedding of the coordinate pair into ℓ² Euclidean space.
Claim. For $a,b\in\mathbb{R}$, write $(a,b)$ for the corresponding point of the ambient Euclidean plane of $S^1$ (i.e., $\mathbb{R}^2$ with the standard $\ell^2$ structure).
background
The ambient space Esp n is the Euclidean space $\mathbb{R}^{n+1}$ (Mathlib EuclideanSpace ℝ (Fin (n+1))), so Esp 1 is the plane that carries the unit circle $S^1$. Points of that plane are ℓ² vectors indexed by Fin 2.
This module develops linking-vanishing statements in high dimension, building on singular sphere geometry and the low-dimensional linking package. Concrete arcs on $S^1$ are needed as test curves; those arcs are written in plane coordinates and then projected to the sphere.
The definition simply packages a coordinate pair $(a,b)$ as such a plane point, so later lemmas can talk about norms, coordinate projections, and sphere membership without repeating the embedding.
proof idea
Definitional one-liner: embed the Mathlib vector ![a, b] into the ℓ² Euclidean structure via WithLp.toLp 2. No proof obligations; the type is exactly Esp 1.
why it matters
Local scaffolding for every concrete $S^1$ calculation in the high-dimensional linking-vanishing development. The simp lemmas for the two coordinates, the norm identity $|(a,b)|=\sqrt{a^2+b^2}$, and the unit-circle membership criterion all apply to this constructor. The semicircle arc map is defined by feeding the standard parametrization $(1-2t,,s\sqrt{1-(1-2t)^2})$ through it and discharging sphere membership with the companion lemma. That arc is the geometric input to acyclicity and linking-detection statements in the same module, which sit in the Foundation layer supporting the forcing chain's geometric side (dimension and linking constraints).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.