theorem proved term proof

`zeroDefect_nonneg`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 100theorem zeroDefect_nonneg (ρ : ℂ) : 0 ≤ zeroDefect ρ := by

Term-mode proof.

 101  rw [zeroDefect_eq_J_log]
 102  exact Foundation.DiscretenessForcing.J_log_nonneg (zeroDeviation ρ)
 103

Lean names referenced from this declaration's body.

J_log_nonneg in IndisputableMonolith.Foundation.DiscretenessForcing decl_use
zeroDefect in IndisputableMonolith.NumberTheory.ZeroLocationCost decl_use
zeroDefect_eq_J_log in IndisputableMonolith.NumberTheory.ZeroLocationCost decl_use
zeroDeviation in IndisputableMonolith.NumberTheory.ZeroLocationCost decl_use