zeroDefectSet

formal source

  39  { t : ℝ | ∃ s : ℂ, Ξ.xi s = 0 ∧ zeroDeviation s = t }
  40
  41/-- The set of zero defects realized by zeros of a completed-ξ surface. -/
  42def zeroDefectSet (Ξ : CompletedXiSurface) : Set ℝ :=
  43  { d : ℝ | ∃ s : ℂ, Ξ.xi s = 0 ∧ zeroDefect s = d }
  44
  45/-- Functional-equation invariance of the completed-ξ value. -/
  46theorem xi_reflection_invariant (Ξ : CompletedXiSurface) (s : ℂ) :
  47    Ξ.xi (functionalReflection s) = Ξ.xi s := by
  48  simpa [functionalReflection] using Ξ.reflection s
  49
  50/-- Conjugation symmetry of the completed-ξ value. -/
  51theorem xi_conjugation_invariant (Ξ : CompletedXiSurface) (s : ℂ) :
  52    Ξ.xi (conj s) = conj (Ξ.xi s) :=
  53  Ξ.conjugation s
  54
  55/-- Zeros come in reflection pairs under the functional equation. -/
  56theorem zero_pairing_under_reflection (Ξ : CompletedXiSurface) {s : ℂ}
  57    (hs : Ξ.xi s = 0) :
  58    Ξ.xi (functionalReflection s) = 0 := by
  59  simpa [functionalReflection, hs] using Ξ.reflection s
  60
  61/-- Zeros come in conjugate pairs under reality symmetry. -/
  62theorem zero_pairing_under_conjugation (Ξ : CompletedXiSurface) {s : ℂ}
  63    (hs : Ξ.xi s = 0) :
  64    Ξ.xi (conj s) = 0 := by
  65  rw [Ξ.conjugation, hs]
  66  simp
  67
  68/-- Zeros are stable under reflection composed with conjugation. -/
  69theorem zero_pairing_under_critical_reflection (Ξ : CompletedXiSurface) {s : ℂ}
  70    (hs : Ξ.xi s = 0) :
  71    Ξ.xi (criticalReflection s) = 0 := by
  72  have hconj : Ξ.xi (conj s) = 0 :=