zeroDefect_pos_iff_off_critical_line
plain-language theorem explainer
zeroDefect_pos_iff_off_critical_line shows that the zero-location defect is strictly positive precisely when ρ lies off the critical line Re ρ = 1/2. Number theorists translating zeta zeros into Recognition Science costs would cite this equivalence. The tactic proof rewrites zeroDefect to J_log of the deviation then splits on the zero and positivity characterizations of J_log.
Claim. For any complex number ρ, $0 <$ zeroDefect(ρ) holds if and only if Re(ρ) ≠ 1/2, where zeroDefect(ρ) := defect(exp(2(Re ρ − 1/2))) and defect coincides with the J functional satisfying J(e^t) = cosh(t) − 1.
background
The module formalizes the RS dictionary between zeta-zero location and zero-defect cost: zeroDeviation ρ := 2(Re ρ − 1/2) and zeroDefect ρ := defect(exp(zeroDeviation ρ)). The critical line Re ρ = 1/2 is therefore the exact zero-defect locus. OnCriticalLine ρ is the predicate Re ρ = 1/2. Upstream, J_log t := cosh t − 1 is zero precisely at t = 0 and strictly positive elsewhere; zeroDefect ρ equals J_log(zeroDeviation ρ), so the sign of the defect directly tracks deviation from the line.
proof idea
The proof rewrites zeroDefect ρ to J_log(zeroDeviation ρ). It splits into two directions. Assuming positive defect together with OnCriticalLine ρ yields J_log(0) = 0 via the zeroDeviation zero-iff lemma, contradicting J_log positivity by linarith. Conversely, not OnCriticalLine ρ implies zeroDeviation ρ ≠ 0, so J_log_pos supplies the strict inequality.
why it matters
This equivalence places the critical line exactly at the minimum of the defect functional, linking zero location to the J-uniqueness step (T5) in the forcing chain where J(x) = cosh(log x) − 1. It supports the broader claim that zeros minimize J-cost. No downstream uses are recorded yet, leaving open its insertion into explicit mass ladders or alpha-band bounds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.