doubledZeroDefect_nonneg
plain-language theorem explainer
The doubled zero defect of any complex number ρ is nonnegative. Researchers studying the Riemann hypothesis via the Recognition Science defect functional cite this to confirm that the observable stays nonnegative after the doubling map induced by functional-equation symmetry. The proof is a direct reduction to the elementary inequality cosh(y) ≥ 1 for real y.
Claim. For every complex number ρ, let δ(ρ) = 2(ℜ(ρ) − 1/2). Then 0 ≤ cosh(2 ⋅ δ(ρ)) − 1.
background
The Zero Doubling Law module records the doubling recurrence D(2t) = 2 D(t)² + 4 D(t) obtained from the functional-equation/J-symmetry bridge. The doubled zero defect is defined as J_log(2 ⋅ zeroDeviation ρ), where zeroDeviation ρ = 2(ℜ(ρ) − 1/2) measures the real deviation from the critical line in the log-coordinate scale compatible with the RS defect functional. Its closed form equals cosh(2 ⋅ zeroDeviation ρ) − 1, as stated by the companion theorem in the same module.
proof idea
The proof is a term-mode one-liner. It rewrites the doubled zero defect via the closed-form equality to cosh(2 ⋅ zeroDeviation ρ) − 1, then applies linarith to the library fact that cosh y ≥ 1 for every real y, evaluated at y = 2 ⋅ zeroDeviation ρ.
why it matters
This nonnegativity is assembled into the current_vectorC_attempt_data theorem, which packages the zero defect vanishing exactly on the critical line, the nonnegativity of the doubled defect, and the doubling recurrence. It supplies concrete evidence that the RS defect observable is consistent with the J-uniqueness and self-composition structure. The module notes that the resulting doubling law remains weaker than the full d'Alembert interface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.