zeroDeviationSet_neg_closed_not_enough

formal source

  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 =
  93          (((1 / 2 - 3 / 4) ^ 2 * (1 / 2 - 1 / 4) ^ 2 : ℝ) : ℂ) := by
  94      simp [toyCompletedXiSurface, toyXi, show s.re = 1 / 2 by exact hline]
  95    have hnonzero :
  96        ((((1 / 2 - 3 / 4) ^ 2 * (1 / 2 - 1 / 4) ^ 2 : ℝ) : ℂ)) ≠ 0 := by
  97      norm_num
  98    have hxine : toyCompletedXiSurface.xi s ≠ 0 := by
  99      simpa [hvalue] using hnonzero
 100    exact hxine hs