IndisputableMonolith.NumberTheory.ZetaLedgerBridge

declarations in this module (17)

• theorem zetaDefectSensor_charge_one L52
• theorem zetaDefectSensor_charge_ne_zero L58
• theorem nonzero_charge_not_physical L66
• theorem unit_sensor_not_physical L75
• theorem strip_zero_gives_nonphysical_sensor L87
• def RSPhysicalThesis L115
• theorem no_strip_zeros_from_rs L131
• theorem zeta_ne_zero_re_ge_one L141
• theorem rh_right_half_from_rs L154
• theorem gammaR_ne_zero_of_nontrivial_zero L165
• theorem completedZeta_zero_of_nontrivial_zero L177
• theorem zeta_one_sub_zero_of_zero L191
• theorem rh_from_rs_thesis L213
• theorem rh_certificate L250
• theorem rh_right_half_certificate L258
• theorem witnessed_sensor_not_physical L278
• theorem witnessed_physical_contradiction L286