zeroDefect_nonneg
plain-language theorem explainer
The zero-location defect is nonnegative for every complex number ρ. Researchers formalizing the Riemann hypothesis inside the Recognition Science framework would cite this to confirm that defect cost reaches its global minimum exactly on the critical line. The proof is a one-line reduction that rewrites the defect via an equality lemma and applies the non-negativity of the J-log function.
Claim. For every complex number ρ, 0 ≤ zeroDefect(ρ), where zeroDefect(ρ) = J_log(2(Re ρ − 1/2)) and J_log(t) = cosh(t) − 1.
background
This module formalizes the Recognition Science dictionary between zeta-zero location and zero-defect cost. zeroDeviation ρ is defined as 2(Re ρ − 1/2), and zeroDefect ρ is the defect attached to exp(zeroDeviation ρ). The critical line Re ρ = 1/2 is therefore the zero-defect locus.
proof idea
The proof is a one-line wrapper. It rewrites zeroDefect ρ by the equality zeroDefect_eq_J_log to obtain J_log(zeroDeviation ρ), then invokes the upstream theorem J_log_nonneg on that real argument.
why it matters
This result establishes non-negativity of the zero-location defect, confirming the critical line as the global minimum of the RS cost functional. It supports the sibling equivalences zeroDefect_zero_iff_on_critical_line and zeroDefect_pos_iff_off_critical_line. In the framework it rests on the J-log non-negativity derived from the discreteness-forcing chain and the defect functional of LawOfExistence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.