IndisputableMonolith.NumberTheory.CompletedXiSymmetry

   1import Mathlib
   2import IndisputableMonolith.NumberTheory.ZeroLocationCost
   3
   4/-!
   5# Completed Xi Symmetry
   6
   7This module records the minimal functional-equation symmetry surface needed for
   8Vector C.
   9
  10It is deliberately small and honest: at this stage we only encode the completed
  11zeta symmetries that give **pairing data** on zeros. This yields reflection and
  12conjugation invariants for `zeroDeviation` / `zeroDefect`, but not yet any
  13d'Alembert-style composition law.
  14-/
  15
  16namespace IndisputableMonolith
  17namespace NumberTheory
  18
  19open scoped ComplexConjugate
  20
  21noncomputable section
  22
  23/-- Minimal completed-ξ symmetry data for Vector C.
  24
  25`reflection` is the completed functional equation, and `conjugation` is the
  26standard reality symmetry. Any stronger zero-location constraint must be added
  27on top of this surface; it is not present here by default. -/
  28structure CompletedXiSurface where
  29  xi : ℂ → ℂ
  30  reflection : ∀ s : ℂ, xi (1 - s) = xi s
  31  conjugation : ∀ s : ℂ, xi (conj s) = conj (xi s)
  32
  33/-- The zero set of the completed-ξ surface. -/
  34def XiZeroSet (Ξ : CompletedXiSurface) : Set ℂ :=
  35  { s : ℂ | Ξ.xi s = 0 }
  36
  37/-- The set of zero deviations realized by zeros of a completed-ξ surface. -/
  38def zeroDeviationSet (Ξ : CompletedXiSurface) : Set ℝ :=
  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 :=
  73    zero_pairing_under_conjugation Ξ hs
  74  simpa [criticalReflection, functionalReflection] using
  75    zero_pairing_under_reflection Ξ hconj
  76
  77/-- Reflection and conjugation give the exact zero-location invariants currently
  78available from the completed-ξ surface. -/
  79theorem functionalEquation_gives_pairing_invariants
  80    (Ξ : CompletedXiSurface) {s : ℂ} (hs : Ξ.xi s = 0) :
  81    Ξ.xi (functionalReflection s) = 0 ∧
  82      Ξ.xi (conj s) = 0 ∧
  83      Ξ.xi (criticalReflection s) = 0 ∧
  84      zeroDeviation (functionalReflection s) = -zeroDeviation s ∧
  85      zeroDeviation (conj s) = zeroDeviation s ∧
  86      zeroDefect (functionalReflection s) = zeroDefect s ∧
  87      zeroDefect (conj s) = zeroDefect s ∧
  88      zeroDefect (criticalReflection s) = zeroDefect s := by
  89  refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩
  90  · exact zero_pairing_under_reflection Ξ hs
  91  · exact zero_pairing_under_conjugation Ξ hs
  92  · exact zero_pairing_under_critical_reflection Ξ hs
  93  · exact zeroDeviation_functionalReflection s
  94  · exact zeroDeviation_conj s
  95  · exact zeroDefect_invariant_under_functional_reflection s
  96  · exact zeroDefect_invariant_under_conjugation s
  97  · exact zeroDefect_invariant_under_reflection s
  98
  99/-- The functional equation makes the zero-deviation set symmetric under
 100negation. This is the strongest zero-location consequence currently available
 101from the minimal completed-ξ surface. -/
 102theorem zeroDeviationSet_neg_closed (Ξ : CompletedXiSurface) {t : ℝ}
 103    (ht : t ∈ zeroDeviationSet Ξ) :
 104    -t ∈ zeroDeviationSet Ξ := by
 105  rcases ht with ⟨s, hs, rfl⟩
 106  refine ⟨functionalReflection s, zero_pairing_under_reflection Ξ hs, ?_⟩
 107  simp
 108
 109/-- The functional equation preserves the realized zero-defect set. -/
 110theorem zeroDefectSet_reflection_invariant (Ξ : CompletedXiSurface) {d : ℝ}
 111    (hd : d ∈ zeroDefectSet Ξ) :
 112    d ∈ zeroDefectSet Ξ := by
 113  rcases hd with ⟨s, hs, rfl⟩
 114  exact ⟨functionalReflection s, zero_pairing_under_reflection Ξ hs,
 115    zeroDefect_invariant_under_functional_reflection s⟩
 116
 117end
 118
 119end NumberTheory
 120end IndisputableMonolith
 121