Row 23 RH support: RHLowSlabFourteenthCell01
Definitionrow23_rh_supp_RHLowSlabFourteenthCell01finite-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_RHLowSlabFourteenthPilot set_option autoImplicit false set_option maxRecDepth 100000 set_option maxHeartbeats 0 set_option exponentiation.threshold 20000 noncomputable section namespace RHLowSlabFourteenthPilot theorem cell01_checked : Arb4.cellOK slab 1 = true := by decide +kernel end RHLowSlabFourteenthPilot #print axioms RHLowSlabFourteenthPilot.cell01_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.