pith. machine review for the scientific record. sign in
theorem

zeroDefect_invariant_under_reflection

proved
show as:
view math explainer →
module
IndisputableMonolith.NumberTheory.ZeroLocationCost
domain
NumberTheory
line
155 · github
papers citing
none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.NumberTheory.ZeroLocationCost on GitHub at line 155.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.