IndisputableMonolith.NumberTheory.Port.RiemannHypothesis
The RiemannHypothesis module ports Mathlib results on the completed zeta function having no zeros for real part exceeding one into the Recognition Science number theory layer. It builds directly on the primes basic module to preserve an axiom-free base. Analytic number theorists reference these statements to mark the zero-free region outside the critical strip. The argument consists of direct applications of the Euler product for the zeta function together with gamma factor properties.
claimThe completed Riemann zeta function satisfies $ξ(s) ≠ 0$ for all $s$ with Re$(s) > 1$. This follows from the Euler product formula ensuring the ordinary zeta function is nonzero in that half-plane, combined with the fact that the gamma factor has no zeros and only finitely many poles.
background
This module occupies the analytic number theory slot inside the NumberTheory port. It imports the primes basic module, whose design reuses Mathlib natural-number primality while remaining axiom-free and sorry-free so the layer can sit inside the main monolith. The local setting therefore extends algebraic footholds upward into complex analysis without introducing new axioms. The supplied doc-comment records that the completed function inherits non-vanishing from the ordinary zeta function via the Euler product.
proof idea
The module consists of direct translations of the Mathlib non-vanishing lemma. The central statement applies the source result on zeta non-vanishing for real part greater than one, then notes that the gamma factor contributes no zeros. Companion statements handle the closed half-plane and introduce the conditional package. No additional tactics appear; each item is a one-line wrapper around the imported lemma.
why it matters in Recognition Science
The module supplies the exterior zero-free region that feeds the NumberTheory.Port layer. It thereby supports the conditional package for the Riemann hypothesis by securing the prerequisite non-vanishing outside the critical strip. Within the Recognition Science chain this step closes the analytic prerequisite needed before any attempt to locate zeros on the critical line or to connect number theory to the forcing chain and dimension count.
scope and limits
- Does not prove the Riemann hypothesis.
- Does not locate zeros inside the critical strip.
- Does not supply new growth estimates for the zeta function.
- Does not address the functional equation or explicit formulae.
- Applies only to the half-plane Re(s) > 1 and its boundary.