toyCompletedXiSurface_has_off_critical_zero

formal source

  50  conjugation := toyXi_conjugation
  51
  52/-- The toy surface has a zero at `s = 3/4`. -/
  53theorem toyCompletedXiSurface_has_off_critical_zero :
  54    toyCompletedXiSurface.xi (3 / 4 : ℂ) = 0 ∧
  55      ¬ OnCriticalLine (3 / 4 : ℂ) := by
  56  constructor
  57  · norm_num [toyCompletedXiSurface, toyXi]
  58  · norm_num [OnCriticalLine]
  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 :=