zeroDefect_pos_iff_off_critical_line
plain-language theorem explainer
The zero-location defect is strictly positive exactly when a complex number lies off the line Re(ρ) = 1/2. Researchers formalizing the Riemann hypothesis inside Recognition Science would cite this biconditional. The proof rewrites the defect via its J_log representation and reduces both directions to the known sign properties of J_log away from zero.
Claim. For any complex number ρ, 0 < zeroDefect(ρ) if and only if Re(ρ) ≠ 1/2, where zeroDefect(ρ) := defect(exp(2(Re(ρ) − 1/2))) and defect coincides with the J functional.
background
The module ZeroLocationCost encodes the RS dictionary between zeta zeros and defect cost. It defines zeroDeviation(ρ) := 2(Re(ρ) − 1/2) and zeroDefect(ρ) := defect(exp(zeroDeviation(ρ))), so that the critical line Re(ρ) = 1/2 is exactly the zero-defect locus. OnCriticalLine(ρ) is the predicate Re(ρ) = 1/2. Upstream, J_log(t) := cosh(t) − 1 is the log-coordinate form of the J functional; J_log(t) = 0 if and only if t = 0, and J_log(t) > 0 otherwise.
proof idea
The tactic proof first rewrites zeroDefect ρ to J_log(zeroDeviation ρ). It then splits the biconditional. The forward direction assumes a positive defect and a critical-line hypothesis, derives J_log(zeroDeviation ρ) = 0 via the zero-equivalence lemma, and obtains a contradiction by linarith. The reverse direction assumes the point is off the line, deduces zeroDeviation ρ ≠ 0, and applies the strict-positivity lemma for J_log.
why it matters
This equivalence completes the local dictionary in the Zero Location Cost module: the critical line is the unique zero-defect locus. It sits between the definition of zeroDefect and any later global statements about zero distribution. The surrounding framework identifies the critical line with the minimum of the J-cost bowl (T5 J-uniqueness) and treats defect as the Recognition Composition Law cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.