pt2_norm
plain-language theorem explainer
The Euclidean norm of the plane point with coordinates (a, b) equals √(a² + b²). Sphere-membership and arc-geometry lemmas in the linking-vanishing development cite it to convert algebraic circle equations into metric statements. The proof rewrites the Esp norm as a two-term sum of squared absolute values and cancels the absolute values via sq_abs.
Claim. For all real numbers $a$ and $b$, if $p$ denotes the point of the Euclidean plane with coordinates $(a,b)$, then $\|p\| = \sqrt{a^2 + b^2}$.
background
The ambient space is Esp 1, the 2-dimensional Euclidean space (L² product on coordinates indexed by Fin 2). The helper pt2 a b packages the pair (a, b) as a point of that space via WithLp.toLp 2 ![a, b].
This module develops linking-vanishing statements in high dimension, building on singular-sphere geometry and the low-dimensional linking companion. Norm identities for coordinate points are the bridge from algebraic circle equations (sums of squares) to metric membership in spheres centered at the origin.
Upstream, only the definition of the coordinate point is essential; the other dependency edges are ambient framework imports and do not enter the short calculation.
proof idea
Term/tactic hybrid, four rewrites. First apply EuclideanSpace.norm_eq so the norm becomes the square root of a finite sum of squared coordinate norms, then Fin.sum_univ_two expands the sum to the two coordinates. The goal reduces to √(‖a‖² + ‖b‖²) = √(a² + b²). Rewrite each real norm as absolute value (Real.norm_eq_abs) and cancel the absolute values under squaring (sq_abs twice).
why it matters
Immediate parent is pt2_mem_sphere: membership of (a,b) in the unit circle from a² + b² = 1, obtained by rewriting through this norm identity and Real.sqrt_one. That membership lemma is the metric entry point for arc and linking constructions in the high-dimensional vanishing development (complements, acyclicity, detection of nontrivial linking).
In the broader Recognition foundation this sits under singular-sphere geometry supporting dimensional and linking constraints along the forcing chain (notably the D = 3 / eight-tick geometry landmarks). It is pure Euclidean bookkeeping, not a physics claim, but without it the circle-equation side of the linking arguments cannot talk to the sphere metric.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.