completedXiSurface_symmetry_only_no_go

formal source

  59
  60/-- Reflection/conjugation symmetry of the completed-ξ surface alone is
  61insufficient to force the critical line. -/
  62theorem completedXiSurface_symmetry_only_no_go :
  63    ¬ (∀ Ξ : CompletedXiSurface, ∀ s : ℂ, Ξ.xi s = 0 → OnCriticalLine s) := by
  64  intro h
  65  obtain ⟨hzero, hline⟩ := toyCompletedXiSurface_has_off_critical_zero
  66  exact hline (h toyCompletedXiSurface (3 / 4 : ℂ) hzero)
  67
  68/-- The negation-closed deviation-set property obtained from the functional
  69equation does not force `0` to be the only realized deviation. -/
  70theorem zeroDeviationSet_neg_closed_not_enough :
  71    ∃ Ξ : CompletedXiSurface,
  72      (1 / 2 : ℝ) ∈ zeroDeviationSet Ξ ∧
  73      (-1 / 2 : ℝ) ∈ zeroDeviationSet Ξ ∧
  74      0 ∉ zeroDeviationSet Ξ := by
  75  refine ⟨toyCompletedXiSurface, ?_, ?_, ?_⟩
  76  · refine ⟨(3 / 4 : ℂ), ?_, ?_⟩
  77    · exact toyCompletedXiSurface_has_off_critical_zero.1
  78    · norm_num [zeroDeviation]
  79  · have hhalf : (1 / 2 : ℝ) ∈ zeroDeviationSet toyCompletedXiSurface := by
  80      refine ⟨(3 / 4 : ℂ), ?_, ?_⟩
  81      · exact toyCompletedXiSurface_has_off_critical_zero.1
  82      · norm_num [zeroDeviation]
  83    have hneg : (-(1 / 2 : ℝ)) ∈ zeroDeviationSet toyCompletedXiSurface :=
  84      zeroDeviationSet_neg_closed toyCompletedXiSurface hhalf
  85    norm_num at hneg ⊢
  86    exact hneg
  87  · intro hzero
  88    rcases hzero with ⟨s, hs, hdev⟩
  89    have hline : OnCriticalLine s :=
  90      (zeroDeviation_eq_zero_iff_on_critical_line s).mp hdev
  91    have hvalue :
  92        toyCompletedXiSurface.xi s =