The smooth plane vortex equation and its deformation complex

Write a field as x = (b₁, b₂, p, q), representing the imaginary connection a = i (b₁ ds + b₂ dt) and section α = 2 (p + i q). The coefficient metric |b|² + |δα|² / 4 is then the Euclidean metric on variations of x. Fields take values in EuclideanSpace ℝ (Fin 4) and equation defects in EuclideanSpace ℝ (Fin 3), with these Euclidean coefficient norms. equation x has three real components: the defect in *iF_a = (1 - |α|²) / 8 and the real and imaginary parts of ∂bar_a α. The convention is ∂bar_a α = (∇₁α + i ∇₂α) / 2, with ∇ = d + a. phaseGauge realizes the action of exp (i f); its composition law holds for differentiable phases, and its first variation requires no phase regularity. Covariance of the equation requires C² phases. Where the section does not vanish, ∂bar_a α = 0 determines the connection from the section (eq_of_forall_section_eq). Where ∂bar_a α = 0, the covariant derivative is complex linear, d_a α (v) = v · d_a α (1) (covariantDerivative_eq_mul_of_equation_eq_zero), and it controls the gradient of |α|² through (∂_s |α|²)² + (∂_t |α|²)² = 4 |α|² |d_a α (1)|² (fderiv_normSq_apply_one_sq_add_apply_I_sq), so |d_a α (1)| ≤ |∇ |α|²| where |α|² ≥ 1 / 2 (norm_covariantDerivative_one_le_norm_fderiv_normSq).

equation_add_smul gives the exact quadratic expansion, and hasDerivAt_equation identifies linearizedEquation as its first variation. For the charge-one infinitesimal gauge action gaugeDirection x f, the off-shell composition is (0, -f * (equation x)₂, f * (equation x)₁). Consequently it vanishes at every solution, giving the differential-complex identity without a gauge-fixing assumption. The vacuum is (0, 0, 1/2, 0); its linearization agrees with the last three rows of vacuumOperator. This is a smooth differential expression; no completed field space, Fredholm property or quotient construction is asserted.

The normalization follows TauCeti.Vortex.vacuumOperator and A. Jaffe and C. H. Taubes, Vortices and Monopoles, Progress in Physics 2, Birkhäuser, 1980.

noncomputable def TauCeti.Vortex.equation (x : ℂ → EuclideanSpace ℝ (Fin 4)) (z : ℂ) : EuclideanSpace ℝ (Fin 3)

The three real defects of the plane vortex equation in the coordinates a = i (x₀ ds + x₁ dt), α = 2 (x₂ + i x₃).

def TauCeti.Vortex.sectionValue (x : ℂ → EuclideanSpace ℝ (Fin 4)) (z : ℂ) : ℂ

The actual section α = 2(p + i q) represented by a real vortex field.

theorem TauCeti.Vortex.sectionValue_apply (x : ℂ → EuclideanSpace ℝ (Fin 4)) (z : ℂ) : sectionValue x z = 2 * (↑((x z).ofLp 2) + ↑((x z).ofLp 3) * Complex.I)

The section in the real field coordinates.

theorem TauCeti.Vortex.sectionValue_sub (x y : ℂ → EuclideanSpace ℝ (Fin 4)) (z : ℂ) : sectionValue (x - y) z = sectionValue x z - sectionValue y z

The section of a difference of fields is the difference of their sections.

theorem TauCeti.Vortex.apply_eq_of_sectionValue_eq {x y : ℂ → EuclideanSpace ℝ (Fin 4)} {z : ℂ} (h₀ : (x z).ofLp 0 = (y z).ofLp 0) (h₁ : (x z).ofLp 1 = (y z).ofLp 1) (hs : sectionValue x z = sectionValue y z) : x z = y z

Two fields agree at a point when their connection coordinates and their sections agree there.

theorem TauCeti.Vortex.sq_norm_sectionValue (x : ℂ → EuclideanSpace ℝ (Fin 4)) (z : ℂ) : ‖sectionValue x z‖ ^ 2 = 4 * ((x z).ofLp 2 ^ 2 + (x z).ofLp 3 ^ 2)

The squared modulus |α|² = 4 (p² + q²) of the section in the real field coordinates.

theorem TauCeti.Vortex.norm_sectionValue_le (x : ℂ → EuclideanSpace ℝ (Fin 4)) (z : ℂ) : ‖sectionValue x z‖ ≤ 2 * ‖x z‖

The section of a field is bounded by the field: |α| ≤ 2 |x|.

theorem TauCeti.Vortex.sectionValue_eq_zero_iff (x : ℂ → EuclideanSpace ℝ (Fin 4)) (z : ℂ) : sectionValue x z = 0 ↔ (x z).ofLp 2 ^ 2 + (x z).ofLp 3 ^ 2 = 0

The section of a field vanishes exactly where p ^ 2 + q ^ 2 does, for p, q its real coordinates.

theorem TauCeti.Vortex.tendsto_sectionValue_zero {l : Filter ℂ} {x : ℂ → EuclideanSpace ℝ (Fin 4)} (hx : Filter.Tendsto x l (nhds 0)) : Filter.Tendsto (sectionValue x) l (nhds 0)

If a field tends to zero along a filter, then so does its section.

theorem TauCeti.Vortex.tendsto_normSq_of_tendsto_sectionValue_mul {phase : ℂ → ℂ} {x : ℂ → EuclideanSpace ℝ (Fin 4)} (hphase : Filter.Tendsto (fun (z : ℂ) => ‖phase z‖) (Filter.cocompact ℂ) (nhds 1)) (hfr : Filter.Tendsto (fun (z : ℂ) => sectionValue x z * phase z) (Filter.cocompact ℂ) (nhds 1)) : Filter.Tendsto (fun (z : ℂ) => 4 * ((x z).ofLp 2 ^ 2 + (x z).ofLp 3 ^ 2)) (Filter.cocompact ℂ) (nhds 1)

The end framing α(z) · phase(z) → 1, with |phase| → 1 at infinity, gives the squared modulus |α|² = 4 (p² + q²) tending to one at infinity.

theorem TauCeti.Vortex.tendsto_normSq_of_tendsto_sectionValue_mul_inv_pow {m : ℕ} {x : ℂ → EuclideanSpace ℝ (Fin 4)} (hframe : Filter.Tendsto (fun (z : ℂ) => sectionValue x z * ((z / ↑‖z‖) ^ m)⁻¹) (Filter.cocompact ℂ) (nhds 1)) : Filter.Tendsto (fun (z : ℂ) => 4 * ((x z).ofLp 2 ^ 2 + (x z).ofLp 3 ^ 2)) (Filter.cocompact ℂ) (nhds 1)

A field whose section has the degree-m end framing α(z) (z / |z|)^(-m) → 1 has squared modulus |α|² = 4 (p² + q²) tending to one at infinity.

theorem TauCeti.Vortex.contDiff_normSq {x : ℂ → EuclideanSpace ℝ (Fin 4)} {n : WithTop ℕ∞} (hp : ContDiff ℝ n fun (w : ℂ) => (x w).ofLp 2) (hq : ContDiff ℝ n fun (w : ℂ) => (x w).ofLp 3) : ContDiff ℝ n fun (w : ℂ) => 4 * ((x w).ofLp 2 ^ 2 + (x w).ofLp 3 ^ 2)

The squared modulus |α|² = 4 (p² + q²) is as regular as the real coordinates of the section.

theorem TauCeti.Vortex.fderiv_normSq_apply {x : ℂ → EuclideanSpace ℝ (Fin 4)} {z : ℂ} (hp : DifferentiableAt ℝ (fun (w : ℂ) => (x w).ofLp 2) z) (hq : DifferentiableAt ℝ (fun (w : ℂ) => (x w).ofLp 3) z) (v : ℂ) : (fderiv ℝ (fun (w : ℂ) => 4 * ((x w).ofLp 2 ^ 2 + (x w).ofLp 3 ^ 2)) z) v = 8 * ((x z).ofLp 2 * (fderiv ℝ (fun (w : ℂ) => (x w).ofLp 2) z) v + (x z).ofLp 3 * (fderiv ℝ (fun (w : ℂ) => (x w).ofLp 3) z) v)

The derivative of the squared modulus |α|² = 4 (p² + q²) in terms of those of the real coordinates of the section: d |α|² (v) = 8 (p ∂_v p + q ∂_v q).

theorem TauCeti.Vortex.contDiff_sectionValue {x : ℂ → EuclideanSpace ℝ (Fin 4)} {n : WithTop ℕ∞} (hp : ContDiff ℝ n fun (w : ℂ) => (x w).ofLp 2) (hq : ContDiff ℝ n fun (w : ℂ) => (x w).ofLp 3) : ContDiff ℝ n (sectionValue x)

The section α = 2 (p + i q) is as regular as its real coordinates.

theorem TauCeti.Vortex.differentiableAt_sectionValue {x : ℂ → EuclideanSpace ℝ (Fin 4)} {z : ℂ} (hp : DifferentiableAt ℝ (fun (w : ℂ) => (x w).ofLp 2) z) (hq : DifferentiableAt ℝ (fun (w : ℂ) => (x w).ofLp 3) z) : DifferentiableAt ℝ (sectionValue x) z

The section α = 2 (p + i q) is differentiable wherever its real coordinates are.

theorem TauCeti.Vortex.differentiableAt_sectionValue_of_differentiableAt {x : ℂ → EuclideanSpace ℝ (Fin 4)} {z : ℂ} (hx : DifferentiableAt ℝ x z) : DifferentiableAt ℝ (sectionValue x) z

The section of a field differentiable at a point is differentiable there.

theorem TauCeti.Vortex.contDiffAt_sectionValue_of_contDiffAt {x : ℂ → EuclideanSpace ℝ (Fin 4)} {z : ℂ} {n : WithTop ℕ∞} (hx : ContDiffAt ℝ n x z) : ContDiffAt ℝ n (sectionValue x) z

The section of a field C^n at a point is C^n there.

theorem TauCeti.Vortex.fderiv_sectionValue_apply {x : ℂ → EuclideanSpace ℝ (Fin 4)} {z : ℂ} (hp : DifferentiableAt ℝ (fun (w : ℂ) => (x w).ofLp 2) z) (hq : DifferentiableAt ℝ (fun (w : ℂ) => (x w).ofLp 3) z) (v : ℂ) : (fderiv ℝ (sectionValue x) z) v = 2 * (↑((fderiv ℝ (fun (w : ℂ) => (x w).ofLp 2) z) v) + ↑((fderiv ℝ (fun (w : ℂ) => (x w).ofLp 3) z) v) * Complex.I)

The derivative of the section α = 2 (p + i q) in terms of those of its real coordinates.

noncomputable def TauCeti.Vortex.covariantDerivative (x : ℂ → EuclideanSpace ℝ (Fin 4)) (z v : ℂ) : ℂ

The covariant derivative d_a α, with the charge-one connection a = i(b₁ ds + b₂ dt). The argument v is an actual real tangent vector to the plane.

theorem TauCeti.Vortex.covariantDerivative_apply (x : ℂ → EuclideanSpace ℝ (Fin 4)) (z v : ℂ) : covariantDerivative x z v = (fderiv ℝ (sectionValue x) z) v + Complex.I * ↑((x z).ofLp 0 * v.re + (x z).ofLp 1 * v.im) * sectionValue x z

Coordinate evaluation of the covariant derivative of the actual section.

theorem TauCeti.Vortex.covariantDerivative_eq_re_mul_add_im_mul (x : ℂ → EuclideanSpace ℝ (Fin 4)) (z v : ℂ) : covariantDerivative x z v = ↑v.re * covariantDerivative x z 1 + ↑v.im * covariantDerivative x z Complex.I

The covariant derivative is real-linear in the tangent vector, so it is determined by its values on the coordinate frame (1, i).

theorem TauCeti.Vortex.covariantDerivative_one_eq {x : ℂ → EuclideanSpace ℝ (Fin 4)} {z : ℂ} (hx : DifferentiableAt ℝ x z) : covariantDerivative x z 1 = 2 * (↑((fderiv ℝ (fun (w : ℂ) => (x w).ofLp 2) z) 1 - (x z).ofLp 0 * (x z).ofLp 3) + ↑((fderiv ℝ (fun (w : ℂ) => (x w).ofLp 3) z) 1 + (x z).ofLp 0 * (x z).ofLp 2) * Complex.I)

The covariant derivative ∇₁ α in the real field coordinates: for a field differentiable at z, ∇₁ α = 2 ((∂₁ p - b₁ q) + i (∂₁ q + b₁ p)).

theorem TauCeti.Vortex.covariantDerivative_re {x : ℂ → EuclideanSpace ℝ (Fin 4)} {z : ℂ} (hp : DifferentiableAt ℝ (fun (w : ℂ) => (x w).ofLp 2) z) (hq : DifferentiableAt ℝ (fun (w : ℂ) => (x w).ofLp 3) z) (v : ℂ) : (covariantDerivative x z v).re = 2 * ((fderiv ℝ (fun (w : ℂ) => (x w).ofLp 2) z) v - ((x z).ofLp 0 * v.re + (x z).ofLp 1 * v.im) * (x z).ofLp 3)

The real part of the covariant derivative in the real field coordinates: Re ∇_v α = 2 (∂_v p - b(v) q).

theorem TauCeti.Vortex.covariantDerivative_im {x : ℂ → EuclideanSpace ℝ (Fin 4)} {z : ℂ} (hp : DifferentiableAt ℝ (fun (w : ℂ) => (x w).ofLp 2) z) (hq : DifferentiableAt ℝ (fun (w : ℂ) => (x w).ofLp 3) z) (v : ℂ) : (covariantDerivative x z v).im = 2 * ((fderiv ℝ (fun (w : ℂ) => (x w).ofLp 3) z) v + ((x z).ofLp 0 * v.re + (x z).ofLp 1 * v.im) * (x z).ofLp 2)

The imaginary part of the covariant derivative in the real field coordinates: Im ∇_v α = 2 (∂_v q + b(v) p).

theorem TauCeti.Vortex.continuous_covariantDerivative {x : ℂ → EuclideanSpace ℝ (Fin 4)} (hx : ContDiff ℝ 1 x) (v : ℂ) : Continuous fun (z : ℂ) => covariantDerivative x z v

The covariant derivative of the section of a C¹ field in a fixed direction is continuous.

noncomputable def TauCeti.Vortex.curvature (x : ℂ → EuclideanSpace ℝ (Fin 4)) (z : ℂ) : ℝ

The real curvature coefficient: F_a = i curvature ds ∧ dt.

theorem TauCeti.Vortex.curvature_apply (x : ℂ → EuclideanSpace ℝ (Fin 4)) (z : ℂ) : curvature x z = (fderiv ℝ (fun (w : ℂ) => (x w).ofLp 1) z) 1 - (fderiv ℝ (fun (w : ℂ) => (x w).ofLp 0) z) Complex.I

The curvature coefficient in the oriented coordinate frame (1, i).

noncomputable def TauCeti.Vortex.energyDensity (x : ℂ → EuclideanSpace ℝ (Fin 4)) (z : ℂ) : ℝ

The physical energy density |F_a|² + |d_a α|² + (1 - |α|²)² in the Euclidean plane. No finite-energy condition is built into a field's type.

theorem TauCeti.Vortex.energyDensity_apply (x : ℂ → EuclideanSpace ℝ (Fin 4)) (z : ℂ) : energyDensity x z = curvature x z ^ 2 + ‖covariantDerivative x z 1‖ ^ 2 + ‖covariantDerivative x z Complex.I‖ ^ 2 + (1 - ‖sectionValue x z‖ ^ 2) ^ 2

The physical energy density as a sum of curvature, kinetic and potential terms.

noncomputable def TauCeti.Vortex.linearizedEquation (x y : ℂ → EuclideanSpace ℝ (Fin 4)) (z : ℂ) : EuclideanSpace ℝ (Fin 3)

The first-order linearization of equation at the field x, applied to a variation y. The coordinates of y represent δa = i (y₀ ds + y₁ dt) and δα = 2 (y₂ + i y₃).

noncomputable def TauCeti.Vortex.quadraticTerm (y : ℂ → EuclideanSpace ℝ (Fin 4)) (z : ℂ) : EuclideanSpace ℝ (Fin 3)

The quadratic remainder of the vortex equation, independent of the base field.

noncomputable def TauCeti.Vortex.gaugeDirection (x : ℂ → EuclideanSpace ℝ (Fin 4)) (f : ℂ → ℝ) (z : ℂ) : EuclideanSpace ℝ (Fin 4)

The infinitesimal charge-one gauge action of i f: δa = -i df, δα = i f α.

noncomputable def TauCeti.Vortex.phaseGauge (x : ℂ → EuclideanSpace ℝ (Fin 4)) (f : ℂ → ℝ) (z : ℂ) : EuclideanSpace ℝ (Fin 4)

The gauge transformation with phase exp (i f), in real field coordinates. Its connection part is a - i df and its section part is exp (i f) α.

noncomputable def TauCeti.Vortex.vacuumField : ℂ → EuclideanSpace ℝ (Fin 4)

The normalized vacuum field, with zero connection and section α = 1.

@[simp]

theorem TauCeti.Vortex.equation_apply_zero (x : ℂ → EuclideanSpace ℝ (Fin 4)) (z : ℂ) : (equation x z).ofLp 0 = (fderiv ℝ (fun (w : ℂ) => (x w).ofLp 0) z) Complex.I - (fderiv ℝ (fun (w : ℂ) => (x w).ofLp 1) z) 1 + (4 * ((x z).ofLp 2 ^ 2 + (x z).ofLp 3 ^ 2) - 1) / 8

The curvature defect of the vortex equation.

@[simp]

theorem TauCeti.Vortex.equation_apply_one (x : ℂ → EuclideanSpace ℝ (Fin 4)) (z : ℂ) : (equation x z).ofLp 1 = (fderiv ℝ (fun (w : ℂ) => (x w).ofLp 2) z) 1 - (fderiv ℝ (fun (w : ℂ) => (x w).ofLp 3) z) Complex.I - (x z).ofLp 0 * (x z).ofLp 3 - (x z).ofLp 1 * (x z).ofLp 2

The real complex-equation defect.

@[simp]

theorem TauCeti.Vortex.equation_apply_two (x : ℂ → EuclideanSpace ℝ (Fin 4)) (z : ℂ) : (equation x z).ofLp 2 = (fderiv ℝ (fun (w : ℂ) => (x w).ofLp 3) z) 1 + (fderiv ℝ (fun (w : ℂ) => (x w).ofLp 2) z) Complex.I + (x z).ofLp 0 * (x z).ofLp 2 - (x z).ofLp 1 * (x z).ofLp 3

The imaginary complex-equation defect.

theorem TauCeti.Vortex.equation_congr_nhds {x y : ℂ → EuclideanSpace ℝ (Fin 4)} {z : ℂ} (h : x =ᶠ[nhds z] y) : equation x z = equation y z

The vortex defects at a point depend only on the germ of the field there.

theorem TauCeti.Vortex.contDiff_equation {x : ℂ → EuclideanSpace ℝ (Fin 4)} {n m : WithTop ℕ∞} (hx : ContDiff ℝ n x) (hmn : m + 1 ≤ n) : ContDiff ℝ m (equation x)

The vortex defects of a Cⁿ⁺¹ field form a Cⁿ field.

theorem TauCeti.Vortex.curvature_eq_of_equation_eq_zero {x : ℂ → EuclideanSpace ℝ (Fin 4)} {z : ℂ} (hsol : equation x z = 0) : (fderiv ℝ (fun (w : ℂ) => (x w).ofLp 1) z) 1 - (fderiv ℝ (fun (w : ℂ) => (x w).ofLp 0) z) Complex.I = -((1 - 4 * ((x z).ofLp 2 ^ 2 + (x z).ofLp 3 ^ 2)) / 8)

At a solution of the vortex equation the curvature coefficient ∂₁ b₂ - ∂₂ b₁ of F_a = i (∂₁ b₂ - ∂₂ b₁) ds ∧ dt is -(1 - |α|²) / 8.

theorem TauCeti.Vortex.covariantDerivative_eq_mul_of_equation_eq_zero {x : ℂ → EuclideanSpace ℝ (Fin 4)} {z : ℂ} (hp : DifferentiableAt ℝ (fun (w : ℂ) => (x w).ofLp 2) z) (hq : DifferentiableAt ℝ (fun (w : ℂ) => (x w).ofLp 3) z) (h₁ : (equation x z).ofLp 1 = 0) (h₂ : (equation x z).ofLp 2 = 0) (v : ℂ) : covariantDerivative x z v = v * covariantDerivative x z 1

Where the holomorphicity rows ∂bar_a α = 0 hold, the covariant derivative is complex linear in the tangent vector: d_a α (v) = v · d_a α (1).

theorem TauCeti.Vortex.sq_norm_covariantDerivative_one {x : ℂ → EuclideanSpace ℝ (Fin 4)} {z : ℂ} (hp : DifferentiableAt ℝ (fun (w : ℂ) => (x w).ofLp 2) z) (hq : DifferentiableAt ℝ (fun (w : ℂ) => (x w).ofLp 3) z) : ‖covariantDerivative x z 1‖ ^ 2 = 4 * (((fderiv ℝ (fun (w : ℂ) => (x w).ofLp 2) z) 1 - (x z).ofLp 0 * (x z).ofLp 3) ^ 2 + ((fderiv ℝ (fun (w : ℂ) => (x w).ofLp 3) z) 1 + (x z).ofLp 0 * (x z).ofLp 2) ^ 2)

The squared modulus of d_a α (1) = 2 ((∂_s p - b₁ q) + i (∂_s q + b₁ p)).

theorem TauCeti.Vortex.fderiv_normSq_apply_one_sq_add_apply_I_sq {x : ℂ → EuclideanSpace ℝ (Fin 4)} {z : ℂ} (hp : DifferentiableAt ℝ (fun (w : ℂ) => (x w).ofLp 2) z) (hq : DifferentiableAt ℝ (fun (w : ℂ) => (x w).ofLp 3) z) (h₁ : (equation x z).ofLp 1 = 0) (h₂ : (equation x z).ofLp 2 = 0) : (fderiv ℝ (fun (w : ℂ) => 4 * ((x w).ofLp 2 ^ 2 + (x w).ofLp 3 ^ 2)) z) 1 ^ 2 + (fderiv ℝ (fun (w : ℂ) => 4 * ((x w).ofLp 2 ^ 2 + (x w).ofLp 3 ^ 2)) z) Complex.I ^ 2 = 4 * (4 * ((x z).ofLp 2 ^ 2 + (x z).ofLp 3 ^ 2)) * ‖covariantDerivative x z 1‖ ^ 2

Where the holomorphicity rows ∂bar_a α = 0 hold, the gradient of |α|² and the covariant derivative of α satisfy (∂_s |α|²)² + (∂_t |α|²)² = 4 |α|² |d_a α (1)|².

theorem TauCeti.Vortex.norm_covariantDerivative_one_le_norm_fderiv_normSq {x : ℂ → EuclideanSpace ℝ (Fin 4)} {z : ℂ} (hp : DifferentiableAt ℝ (fun (w : ℂ) => (x w).ofLp 2) z) (hq : DifferentiableAt ℝ (fun (w : ℂ) => (x w).ofLp 3) z) (h₁ : (equation x z).ofLp 1 = 0) (h₂ : (equation x z).ofLp 2 = 0) (hhalf : 1 / 2 ≤ 4 * ((x z).ofLp 2 ^ 2 + (x z).ofLp 3 ^ 2)) : ‖covariantDerivative x z 1‖ ≤ ‖fderiv ℝ (fun (w : ℂ) => 4 * ((x w).ofLp 2 ^ 2 + (x w).ofLp 3 ^ 2)) z‖

Where the holomorphicity rows ∂bar_a α = 0 hold and |α|² ≥ 1 / 2, the covariant derivative is bounded by the gradient of |α|²: |d_a α (1)| ≤ |∇ |α|²|.

@[simp]

theorem TauCeti.Vortex.linearizedEquation_apply_zero (x y : ℂ → EuclideanSpace ℝ (Fin 4)) (z : ℂ) : (linearizedEquation x y z).ofLp 0 = (fderiv ℝ (fun (w : ℂ) => (y w).ofLp 0) z) Complex.I - (fderiv ℝ (fun (w : ℂ) => (y w).ofLp 1) z) 1 + (x z).ofLp 2 * (y z).ofLp 2 + (x z).ofLp 3 * (y z).ofLp 3

The curvature component of the linearized equation.

@[simp]

theorem TauCeti.Vortex.linearizedEquation_apply_one (x y : ℂ → EuclideanSpace ℝ (Fin 4)) (z : ℂ) : (linearizedEquation x y z).ofLp 1 = (fderiv ℝ (fun (w : ℂ) => (y w).ofLp 2) z) 1 - (fderiv ℝ (fun (w : ℂ) => (y w).ofLp 3) z) Complex.I - (x z).ofLp 0 * (y z).ofLp 3 - (y z).ofLp 0 * (x z).ofLp 3 - (x z).ofLp 1 * (y z).ofLp 2 - (y z).ofLp 1 * (x z).ofLp 2

The real complex component of the linearized equation.

@[simp]

theorem TauCeti.Vortex.linearizedEquation_apply_two (x y : ℂ → EuclideanSpace ℝ (Fin 4)) (z : ℂ) : (linearizedEquation x y z).ofLp 2 = (fderiv ℝ (fun (w : ℂ) => (y w).ofLp 3) z) 1 + (fderiv ℝ (fun (w : ℂ) => (y w).ofLp 2) z) Complex.I + (x z).ofLp 0 * (y z).ofLp 2 + (y z).ofLp 0 * (x z).ofLp 2 - (x z).ofLp 1 * (y z).ofLp 3 - (y z).ofLp 1 * (x z).ofLp 3

The imaginary complex component of the linearized equation.

@[simp]

theorem TauCeti.Vortex.quadraticTerm_apply_zero (y : ℂ → EuclideanSpace ℝ (Fin 4)) (z : ℂ) : (quadraticTerm y z).ofLp 0 = ((y z).ofLp 2 ^ 2 + (y z).ofLp 3 ^ 2) / 2

The curvature component of the quadratic remainder.

@[simp]

theorem TauCeti.Vortex.quadraticTerm_apply_one (y : ℂ → EuclideanSpace ℝ (Fin 4)) (z : ℂ) : (quadraticTerm y z).ofLp 1 = -(y z).ofLp 0 * (y z).ofLp 3 - (y z).ofLp 1 * (y z).ofLp 2

The real complex component of the quadratic remainder.

@[simp]

theorem TauCeti.Vortex.quadraticTerm_apply_two (y : ℂ → EuclideanSpace ℝ (Fin 4)) (z : ℂ) : (quadraticTerm y z).ofLp 2 = (y z).ofLp 0 * (y z).ofLp 2 - (y z).ofLp 1 * (y z).ofLp 3

The imaginary complex component of the quadratic remainder.

@[simp]

theorem TauCeti.Vortex.gaugeDirection_apply_zero (x : ℂ → EuclideanSpace ℝ (Fin 4)) (f : ℂ → ℝ) (z : ℂ) : (gaugeDirection x f z).ofLp 0 = -(fderiv ℝ f z) 1

The first connection component of the infinitesimal gauge action.

@[simp]

theorem TauCeti.Vortex.gaugeDirection_apply_one (x : ℂ → EuclideanSpace ℝ (Fin 4)) (f : ℂ → ℝ) (z : ℂ) : (gaugeDirection x f z).ofLp 1 = -(fderiv ℝ f z) Complex.I

The second connection component of the infinitesimal gauge action.

@[simp]

theorem TauCeti.Vortex.gaugeDirection_apply_two (x : ℂ → EuclideanSpace ℝ (Fin 4)) (f : ℂ → ℝ) (z : ℂ) : (gaugeDirection x f z).ofLp 2 = -f z * (x z).ofLp 3

The real section component of the infinitesimal gauge action.

@[simp]

theorem TauCeti.Vortex.gaugeDirection_apply_three (x : ℂ → EuclideanSpace ℝ (Fin 4)) (f : ℂ → ℝ) (z : ℂ) : (gaugeDirection x f z).ofLp 3 = f z * (x z).ofLp 2

The imaginary section component of the infinitesimal gauge action.

@[simp]

theorem TauCeti.Vortex.phaseGauge_apply_zero (x : ℂ → EuclideanSpace ℝ (Fin 4)) (f : ℂ → ℝ) (z : ℂ) : (phaseGauge x f z).ofLp 0 = (x z).ofLp 0 - (fderiv ℝ f z) 1

The first connection component of a phase gauge transformation.

@[simp]

theorem TauCeti.Vortex.phaseGauge_apply_one (x : ℂ → EuclideanSpace ℝ (Fin 4)) (f : ℂ → ℝ) (z : ℂ) : (phaseGauge x f z).ofLp 1 = (x z).ofLp 1 - (fderiv ℝ f z) Complex.I

The second connection component of a phase gauge transformation.

@[simp]

theorem TauCeti.Vortex.phaseGauge_apply_two (x : ℂ → EuclideanSpace ℝ (Fin 4)) (f : ℂ → ℝ) (z : ℂ) : (phaseGauge x f z).ofLp 2 = Real.cos (f z) * (x z).ofLp 2 - Real.sin (f z) * (x z).ofLp 3

The real section component of a phase gauge transformation.

@[simp]

theorem TauCeti.Vortex.phaseGauge_apply_three (x : ℂ → EuclideanSpace ℝ (Fin 4)) (f : ℂ → ℝ) (z : ℂ) : (phaseGauge x f z).ofLp 3 = Real.sin (f z) * (x z).ofLp 2 + Real.cos (f z) * (x z).ofLp 3

The imaginary section component of a phase gauge transformation.

theorem TauCeti.Vortex.linearizedEquation_add (x : ℂ → EuclideanSpace ℝ (Fin 4)) {y v : ℂ → EuclideanSpace ℝ (Fin 4)} {z : ℂ} (hy : ∀ (i : Fin 4), DifferentiableAt ℝ (fun (w : ℂ) => (y w).ofLp i) z) (hv : ∀ (i : Fin 4), DifferentiableAt ℝ (fun (w : ℂ) => (v w).ofLp i) z) : linearizedEquation x (y + v) z = linearizedEquation x y z + linearizedEquation x v z

The linearized equation preserves addition of variations differentiable at the point.

theorem TauCeti.Vortex.linearizedEquation_smul (x y : ℂ → EuclideanSpace ℝ (Fin 4)) (t : ℝ) (z : ℂ) : linearizedEquation x (t • y) z = t • linearizedEquation x y z

The linearized equation commutes with real scalar multiplication of variations.

@[simp]

theorem TauCeti.Vortex.linearizedEquation_zero (x : ℂ → EuclideanSpace ℝ (Fin 4)) : linearizedEquation x 0 = 0

The zero variation has zero linearized equation.

theorem TauCeti.Vortex.gaugeDirection_add (x : ℂ → EuclideanSpace ℝ (Fin 4)) {f g : ℂ → ℝ} {z : ℂ} (hf : DifferentiableAt ℝ f z) (hg : DifferentiableAt ℝ g z) : gaugeDirection x (f + g) z = gaugeDirection x f z + gaugeDirection x g z

The infinitesimal gauge action preserves addition of phases differentiable at the point.

theorem TauCeti.Vortex.gaugeDirection_smul (x : ℂ → EuclideanSpace ℝ (Fin 4)) (f : ℂ → ℝ) (t : ℝ) (z : ℂ) : gaugeDirection x (t • f) z = t • gaugeDirection x f z

The infinitesimal gauge action commutes with real scalar multiplication of phases.

@[simp]

theorem TauCeti.Vortex.gaugeDirection_zero (x : ℂ → EuclideanSpace ℝ (Fin 4)) : gaugeDirection x 0 = 0

The zero phase has zero infinitesimal gauge action.

@[simp]

theorem TauCeti.Vortex.vacuumField_apply (z : ℂ) : vacuumField z = !₂[0, 0, 1 / 2, 0]

The coordinates of the vacuum field.

@[simp]

theorem TauCeti.Vortex.phaseGauge_zero (x : ℂ → EuclideanSpace ℝ (Fin 4)) : phaseGauge x 0 = x

The zero phase acts as the identity.

theorem TauCeti.Vortex.phaseGauge_phaseGauge (x : ℂ → EuclideanSpace ℝ (Fin 4)) {f g : ℂ → ℝ} {z : ℂ} (hf : DifferentiableAt ℝ f z) (hg : DifferentiableAt ℝ g z) : phaseGauge (phaseGauge x f) g z = phaseGauge x (f + g) z

Composition of phase gauges corresponds to addition of their real phases.

theorem TauCeti.Vortex.hasDerivAt_phaseGauge (x : ℂ → EuclideanSpace ℝ (Fin 4)) (f : ℂ → ℝ) (z : ℂ) (i : Fin 4) : HasDerivAt (fun (t : ℝ) => (phaseGauge x (t • f) z).ofLp i) ((gaugeDirection x f z).ofLp i) 0

The infinitesimal charge-one action is the derivative of the actual phase gauge action.

theorem TauCeti.Vortex.equation_phaseGauge {x : ℂ → EuclideanSpace ℝ (Fin 4)} {f : ℂ → ℝ} {z : ℂ} (hx : ∀ (i : Fin 4), DifferentiableAt ℝ (fun (w : ℂ) => (x w).ofLp i) z) (hf : ContDiffAt ℝ 2 f z) : equation (phaseGauge x f) z = !₂[(equation x z).ofLp 0, Real.cos (f z) * (equation x z).ofLp 1 - Real.sin (f z) * (equation x z).ofLp 2, Real.sin (f z) * (equation x z).ofLp 1 + Real.cos (f z) * (equation x z).ofLp 2]

The curvature defect is gauge invariant, and the complex defect transforms by the same unit phase as the section. This statement includes non-solution fields.

@[simp]

theorem TauCeti.Vortex.equation_phaseGauge_eq_zero_iff {x : ℂ → EuclideanSpace ℝ (Fin 4)} {f : ℂ → ℝ} {z : ℂ} (hx : ∀ (i : Fin 4), DifferentiableAt ℝ (fun (w : ℂ) => (x w).ofLp i) z) (hf : ContDiffAt ℝ 2 f z) : equation (phaseGauge x f) z = 0 ↔ equation x z = 0

A phase gauge transformation preserves the solution condition in both directions.

theorem TauCeti.Vortex.eq_of_forall_section_eq {x y : ℂ → EuclideanSpace ℝ (Fin 4)} (hx₀ : Continuous fun (z : ℂ) => (x z).ofLp 0) (hx₁ : Continuous fun (z : ℂ) => (x z).ofLp 1) (hy₀ : Continuous fun (z : ℂ) => (y z).ofLp 0) (hy₁ : Continuous fun (z : ℂ) => (y z).ofLp 1) (hxsol : ∀ (z : ℂ), (equation x z).ofLp 1 = 0 ∧ (equation x z).ofLp 2 = 0) (hysol : ∀ (z : ℂ), (equation y z).ofLp 1 = 0 ∧ (equation y z).ofLp 2 = 0) (h₂ : ∀ (z : ℂ), (x z).ofLp 2 = (y z).ofLp 2) (h₃ : ∀ (z : ℂ), (x z).ofLp 3 = (y z).ofLp 3) (hdense : Dense {z : ℂ | (y z).ofLp 2 ^ 2 + (y z).ofLp 3 ^ 2 ≠ 0}) : x = y

The section of a vortex determines its connection where it does not vanish. If two fields satisfy the holomorphicity equation ∂bar_a α = 0, have continuous connection components and the same section, and the zero set of that section has empty interior, then the fields are equal.

theorem TauCeti.Vortex.equation_add_smul {x y : ℂ → EuclideanSpace ℝ (Fin 4)} {z : ℂ} (hx : ∀ (i : Fin 4), DifferentiableAt ℝ (fun (w : ℂ) => (x w).ofLp i) z) (hy : ∀ (i : Fin 4), DifferentiableAt ℝ (fun (w : ℂ) => (y w).ofLp i) z) (t : ℝ) : equation (x + t • y) z = equation x z + t • linearizedEquation x y z + t ^ 2 • quadraticTerm y z

Exact quadratic expansion of the vortex equation, with no higher remainder.

theorem TauCeti.Vortex.hasDerivAt_equation {x y : ℂ → EuclideanSpace ℝ (Fin 4)} {z : ℂ} (hx : ∀ (i : Fin 4), DifferentiableAt ℝ (fun (w : ℂ) => (x w).ofLp i) z) (hy : ∀ (i : Fin 4), DifferentiableAt ℝ (fun (w : ℂ) => (y w).ofLp i) z) : HasDerivAt (fun (t : ℝ) => equation (x + t • y) z) (linearizedEquation x y z) 0

The differential expression linearizedEquation is the first variation along every differentiable field direction, evaluated at any fixed point of the plane.

theorem TauCeti.Vortex.linearizedEquation_gaugeDirection {x : ℂ → EuclideanSpace ℝ (Fin 4)} {f : ℂ → ℝ} {z : ℂ} (hp : DifferentiableAt ℝ (fun (w : ℂ) => (x w).ofLp 2) z) (hq : DifferentiableAt ℝ (fun (w : ℂ) => (x w).ofLp 3) z) (hf : ContDiffAt ℝ 2 f z) : linearizedEquation x (gaugeDirection x f) z = !₂[0, -f z * (equation x z).ofLp 2, f z * (equation x z).ofLp 1]

At every field (off-shell), the composition of the linearized equation with the infinitesimal gauge action is the infinitesimal rotation of the complex equation defect.

theorem TauCeti.Vortex.linearizedEquation_gaugeDirection_eq_zero {x : ℂ → EuclideanSpace ℝ (Fin 4)} {f : ℂ → ℝ} {z : ℂ} (hp : DifferentiableAt ℝ (fun (w : ℂ) => (x w).ofLp 2) z) (hq : DifferentiableAt ℝ (fun (w : ℂ) => (x w).ofLp 3) z) (hf : ContDiffAt ℝ 2 f z) (hsol : equation x z = 0) : linearizedEquation x (gaugeDirection x f) z = 0

At a solution, the infinitesimal gauge action followed by the linearized equation is zero. This is the differential-complex identity d₁ d₀ = 0.

@[simp]

theorem TauCeti.Vortex.equation_vacuumField (z : ℂ) : equation vacuumField z = 0

The vacuum solves the nonlinear vortex equation.

theorem TauCeti.Vortex.linearizedEquation_vacuumField (y : SchwartzMap ℂ (EuclideanSpace ℝ (Fin 4))) (z : ℂ) : linearizedEquation vacuumField (⇑y) z = !₂[((vacuumOperator y) z).ofLp 1, ((vacuumOperator y) z).ofLp 2, ((vacuumOperator y) z).ofLp 3]

The smooth linearization at the vacuum is exactly the curvature and two complex rows of the existing gauge-fixed Schwartz operator.