esp1_ext
plain-language theorem explainer
Two vectors in the ambient Euclidean plane of the circle are equal once both coordinates agree. Circle and linking lemmas that rebuild ambient points from coordinate formulas cite this. The argument is PiLp extensionality plus a two-case split on Fin 2.
Claim. Let $a,b$ lie in the ambient Euclidean plane of $S^1$ (i.e. $\mathbb{R}^{\mathrm{Fin}\,2}$ with the Euclidean structure). If $a_0=b_0$ and $a_1=b_1$, then $a=b$.
background
In this module, Esp n is the ambient Euclidean space of the $n$-sphere: $\mathrm{EuclideanSpace},\mathbb{R},(\mathrm{Fin}(n+1))$. Thus Esp 1 is the plane $\mathbb{R}^2$ indexed by $\mathrm{Fin},2$, and the unit circle Sph 1 sits inside it as the set of unit-norm points.
Equality of EuclideanSpace points is pointwise equality of the underlying coordinate functions. Geometry on the circle (stereographic covers, arc parametrizations, east/west points) constantly needs the $n=1$ instance: match the two coordinates, conclude the ambient vectors coincide. The lemma packages that two-line case split once and for all.
proof idea
Apply PiLp.ext to reduce $a=b$ to equality at every index $i:\mathrm{Fin},2$. Split on $i$ via Fin.cases: the zero branch is the given $a_0=b_0$; the successor branch forces the residual index $j:\mathrm{Fin},1$ to be $0$ by omega, rewrites $0.\mathrm{succ}=(1:\mathrm{Fin},2)$ by decide, and finishes with $a_1=b_1$.
why it matters
Downstream, arcFun_arcParam in LinkingVanishingHighDim applies this after matching ambient coordinates to invert the arc parametrization on $S^1$. The same module uses it (indirectly via range identities) for range_arcPlus_inter_arcMinus, which pins the two semicircles to meet exactly at the east and west points. Inside this file it feeds coord_zero_ne_zero: on the doubly punctured circle the first ambient coordinate never vanishes. Together these are the low-dimensional geometric facts that higher-dimensional linking-vanishing arguments rest on in the foundation layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.