A unit vector missing a differentiable surface and a loop in the 3-sphere

Proved

HryniewiczCriterion.exists_unit_pole_off_surface_and_loop

by Mazecto · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

geometry-topologysymplectic-geometry

Let $f:\mathbb{R}^2\to\mathbb{R}^4$ be differentiable on a set $U$ and let $g:\mathbb{R}\to\mathbb{R}^4$ be differentiable. Then there is a unit vector $N\in S^3$ that misses every unit point of the surface and of the curve:

f(v)\neq N\ \ (v\in U,\ |f(v)|=1),\qquad g(s)\neq N\ \ (|g(s)|=1).

The cones $\{c\,f(v):c\in\mathbb{R},v\in U\}$ and $\{c\,g(s)\}$ are images of subsets of a hyperplane of $\mathbb{R}^4$ under maps that are differentiable there, so they have Lebesgue measure zero. Normalizing a point $M$ outside both cones gives $N=M/|M|$ . In practice this provides an admissible stereographic pole for Gauss linking integrals of loops on a disk-like surface in $S^3$ .

Preamble

import Definitions.Def_HryniewiczCriterion_GlobalSection
import Definitions.Def_HryniewiczCriterion_SelfLinking

open HryniewiczCriterion

Formal statement

theorem HryniewiczCriterion.exists_unit_pole_off_surface_and_loop (f : Plane → R4) (U : Set Plane) (hf : DifferentiableOn ℝ f U)
    (g : ℝ → R4) (hg : Differentiable ℝ g) :
    ∃ N : R4, euclidNorm N = 1 ∧ (∀ v ∈ U, euclidNorm (f v) = 1 → f v ≠ N) ∧
      ∀ s, euclidNorm (g s) = 1 → g s ≠ N := by sorry

Source

Elementary (images of null sets under differentiable maps are null); used for the pole in U. Hryniewicz, arXiv:1105.2077, Lemma 3.12

View graph