gammaR_ne_zero_of_nontrivial_zero
plain-language theorem explainer
The theorem establishes that the real Gamma factor Γ_ℝ(s) is nonzero at any zero s of the Riemann zeta function that avoids the trivial zeros at negative even integers. Number theorists formalizing the completed zeta function or consequences of the Riemann hypothesis would cite this auxiliary result. The proof is a short term-mode argument that unfolds the zero condition for Γ_ℝ via simp and performs case analysis on the natural number index to reach a contradiction with either the known zeta zero at zero or the nontriviality hypothesis.
Claim. If the Riemann zeta function satisfies $ζ(s) = 0$ for $s ∈ ℂ$ and there is no natural number $n$ such that $s = -2(n + 1)$, then the real Gamma factor satisfies $Γ_ℝ(s) ≠ 0$.
background
The Zeta–Ledger Bridge module connects Mathlib's concrete riemannZeta to the Recognition Science DefectSensor and PhysicallyExists framework proved in UnifiedRH. It shows that any zero of riemannZeta in the open strip produces a DefectSensor with nonzero charge whose PhysicallyExists predicate is false under the ontological dichotomy. The upstream zeta abbreviation defines the arithmetic zeta function (constant 1 on positive integers), while the and theorem supplies an explicit log-derivative bound M that becomes the angular Lipschitz constant on the circle of radius r.
proof idea
The term proof first simplifies using the equivalence Gammaℝ_eq_zero_iff together with not_exists. It introduces the witness n from the negated existential and applies rcases to split into the zero and successor cases. The zero case substitutes into the zeta zero hypothesis and invokes riemannZeta_zero for contradiction. The successor case applies the nontrivial hypothesis directly to obtain the falsehood.
why it matters
It is invoked by completedZeta_zero_of_nontrivial_zero to conclude that the completed Riemann zeta function vanishes at nontrivial zeros, via the relation ζ(s) = Λ(s) / Γ_ℝ(s). This supports the module's derivation of Mathlib's RiemannHypothesis from the RSPhysicalThesis that every strip zero is a physical ledger event. Within Recognition Science it closes the formalization gap between analytic number theory and the physical predicates without directly invoking the forcing chain or RCL.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.