zeroDefect_invariant_under_conjugation

formal source

 140    _ = zeroDefect ρ := (zeroDefect_eq_J_log ρ).symm
 141
 142/-- Conjugation preserves the zero-location defect. -/
 143theorem zeroDefect_invariant_under_conjugation (ρ : ℂ) :
 144    zeroDefect (conj ρ) = zeroDefect ρ := by
 145  calc
 146    zeroDefect (conj ρ)
 147        =
 148          Foundation.DiscretenessForcing.J_log
 149            (zeroDeviation (conj ρ)) := zeroDefect_eq_J_log _
 150    _ = Foundation.DiscretenessForcing.J_log (zeroDeviation ρ) := by
 151          rw [zeroDeviation_conj]
 152    _ = zeroDefect ρ := (zeroDefect_eq_J_log ρ).symm
 153
 154/-- Reflection plus conjugation preserves the zero-location defect. -/
 155theorem zeroDefect_invariant_under_reflection (ρ : ℂ) :
 156    zeroDefect (criticalReflection ρ) = zeroDefect ρ := by
 157  calc
 158    zeroDefect (criticalReflection ρ)
 159        =
 160          Foundation.DiscretenessForcing.J_log
 161            (zeroDeviation (criticalReflection ρ)) := zeroDefect_eq_J_log _
 162    _ = Foundation.DiscretenessForcing.J_log (-zeroDeviation ρ) := by
 163          rw [zeroDeviation_criticalReflection]
 164    _ = Foundation.DiscretenessForcing.J_log (zeroDeviation ρ) := by
 165          exact Foundation.DiscretenessForcing.J_log_symmetric (zeroDeviation ρ)
 166    _ = zeroDefect ρ := (zeroDefect_eq_J_log ρ).symm
 167
 168end
 169
 170end NumberTheory
 171end IndisputableMonolith