A small loop on a surface crossing a knot transversally has Gauss linking integral with the knot
ProvedHryniewiczCriterion.gaussLinkingIntegral_small_transverse_loopLet be on a ball with there, so is a small surface in . Let be a knot (period , injective modulo ) which meets only at , transversally:
(rows of a matrix). Let miss and . Then for all sufficiently small the loop has Gauss linking integral (gaussLinkingIntegral, stereographic projection from ) with equal to .
Suggested proof. Shift the parameter of so . Taylor expansion gives , while a tube estimate (the knot is embedded and is transverse to inside ) keeps both and , , at distance from , so the straight-line homotopy between them (normalized to ) misses for small . By homotopy invariance the Gauss integral equals that of the round meridian , , which is when (gaussLinkingIntegral_meridian_eq_one, using the symmetry of the Gauss integrand in the two loops). If , reverse the meridian (), which changes the sign.
import Definitions.Def_HryniewiczCriterion_GlobalSection import Definitions.Def_HryniewiczCriterion_SelfLinking open HryniewiczCriterion
theorem HryniewiczCriterion.gaussLinkingIntegral_small_transverse_loop (E : Plane → R4) (z : Plane) (r : ℝ) (hr : 0 < r)
(hE : ContDiffOn ℝ 2 E (Metric.ball z r))
(hEunit : ∀ v ∈ Metric.ball z r, euclidNorm (E v) = 1)
(γ : ℝ → R4) (hγ : ContDiff ℝ 2 γ) (hγper : ∀ t, γ (t + 1) = γ t)
(hγunit : ∀ t, euclidNorm (γ t) = 1) (hγinj : ∀ s t, γ s = γ t → ∃ n : ℤ, t = s + n)
(t₀ : ℝ) (hz : E z = γ t₀)
(hmiss : ∀ v ∈ Metric.ball z r, v ≠ z → ∀ t, E v ≠ γ t)
(hdet : Matrix.det (Matrix.of ![γ t₀, deriv γ t₀,
fderiv ℝ E z (Pi.single 0 1), fderiv ℝ E z (Pi.single 1 1)]) ≠ 0)
(N : R4) (hN : euclidNorm N = 1) (hNγ : ∀ t, γ t ≠ N)
(hNE : ∀ v ∈ Metric.ball z r, E v ≠ N) :
∃ ρ₀ : ℝ, 0 < ρ₀ ∧ ∀ ρ : ℝ, 0 < ρ → ρ < ρ₀ →
gaussLinkingIntegral N (fun s => E (z + ρ • circlePoint s)) γ =
if 0 < Matrix.det (Matrix.of ![γ t₀, deriv γ t₀,
fderiv ℝ E z (Pi.single 0 1), fderiv ℝ E z (Pi.single 1 1)]) then 1 else -1 := by sorry