completedZeta_zero_of_nontrivial_zero
plain-language theorem explainer
The completed Riemann zeta function vanishes at any nontrivial zero of the ordinary zeta function away from the negative even integers. Researchers connecting Mathlib's zeta to the Recognition Science DefectSensor framework cite this to show that strip zeros yield non-physical sensors under the ontological dichotomy. The tactic proof first excludes s = 0, invokes the non-vanishing of the archimedean Gamma factor, and resolves the division relation to force the completed function to zero.
Claim. Let $s$ be a complex number. If the Riemann zeta function satisfies $ζ(s) = 0$ and $s$ is not equal to $-2(n+1)$ for any natural number $n$, then the completed Riemann zeta function $Λ(s)$ equals zero.
background
The Zeta–Ledger Bridge module closes the formalization gap between the abstract DefectSensor and PhysicallyExists predicates from UnifiedRH.lean and Mathlib's concrete riemannZeta. It constructs zetaDefectSensor from strip data and shows that zeros of riemannZeta in the open strip produce sensors with nonzero charge whose physical existence predicate is false. The completed zeta is defined via the relation $ζ(s) = Λ(s) / Γ_ℝ(s)$, where Γ_ℝ denotes the archimedean factor appearing in the functional equation.
proof idea
The tactic proof begins by deriving s ≠ 0 from the known zero of zeta at the origin. It then applies gammaR_ne_zero_of_nontrivial_zero to obtain Γ_ℝ(s) ≠ 0. Next it invokes riemannZeta_def_of_ne_zero to express the completed function, substitutes the zero assumption, rewrites via div_eq_zero_iff, and resolves the right disjunct using the nonzero Gamma factor.
why it matters
This theorem is invoked by zeta_one_sub_zero_of_zero to propagate vanishing to the reflected point 1 − s. It contributes to the chain deriving Mathlib's RiemannHypothesis from the RSPhysicalThesis hypothesis, as described in the module documentation. Within Recognition Science it supports the claim that nontrivial zeros correspond to ledger events that violate the physical existence predicate under the ontological dichotomy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.