Row 23 RH support: RHLowSlabThirteenthCell13
Definitionrow23_rh_supp_RHLowSlabThirteenthCell13finite-verificationnumber-theoryriemann-zeta
A Lean-checked supporting component of the finite-height Riemann hypothesis and Chebyshev psi reduction for the b=23 Dusart Table 1 bound. Its declarations and hypotheses are stated exactly in the attached Lean source; this module alone does not assert the complete row estimate.
Definition code
import Definitions.Def_row23_rh_supp_RHLowSlabThirteenthPilot set_option autoImplicit false set_option maxRecDepth 100000 set_option maxHeartbeats 0 set_option exponentiation.threshold 20000 noncomputable section namespace RHLowSlabThirteenthPilot theorem cell13_checked : Arb4.cellOK slab 13 = true := by decide +kernel end RHLowSlabThirteenthPilot #print axioms RHLowSlabThirteenthPilot.cell13_checked
Source
Supporting arithmetic and analytic certificate for P. Dusart, Ramanujan J. 45 (2018), Table 1 and explicit psi bounds, pp. 233–235, DOI 10.1007/s11139-016-9839-4.