Certificate tables for the finite Rosser-Schoenfeld totient verification: the first 66 primes, the log-log table, and the primorial ratio table

import Definitions.Def_TaoFivePrimes_theta_cert_tables
import Mathlib.Data.Rat.Defs
import Mathlib.Algebra.BigOperators.Group.Finset.Basic

/-!
# Numerical tables for the finite totient verification

This file records the numerical data used for the finite verification of the
Rosser--Schoenfeld totient bound (Theorem 15 of Rosser--Schoenfeld 1962, used
in Tao's five-primes paper).

* `ptab m` for `m < 66` is the `(m+1)`-st prime: `ptab 0 = 2`, ..., `ptab 65 = 317`.
* `Snum m` is the certified integer sum `sum_{i<m} clbZ (ptab i)`, where
  `clbZ p / 10^4 < log p` is the certified logarithm table from
  `Def_TaoFivePrimes_theta_cert_tables`.
* `rll m` for `4 <= m <= 65` is a certified rational lower bound for
  `log (log (Snum m / 10^4))`, given to four decimal places (`m = 9` sharper).
* `Pnum m` and `Pden m` are the numerator and denominator of the partial
  product `prod_{i<m} ptab i / (ptab i - 1)`, i.e. `Pnum m = prod_{i<m} ptab i`
  and `Pden m = prod_{i<m} (ptab i - 1)`.
* `Qpt m = Pnum m / Pden m` is that partial product.

The companion theorem `tao_totient_cert_loglog_table` relates these tables to
`Nat.primorial (Nat.nth Nat.Prime _)`, and `tao_totient_cert_finite_step`
uses them in the finite verification.
-/

open Finset
open scoped BigOperators

namespace TaoFivePrimes
/-- The first 66 primes as a table: `ptab m = p_{m+1}`, indexed from 0. -/
def ptab : ℕ → ℕ
  | 0 => 2
  | 1 => 3
  | 2 => 5
  | 3 => 7
  | 4 => 11
  | 5 => 13
  | 6 => 17
  | 7 => 19
  | 8 => 23
  | 9 => 29
  | 10 => 31
  | 11 => 37
  | 12 => 41
  | 13 => 43
  | 14 => 47
  | 15 => 53
  | 16 => 59
  | 17 => 61
  | 18 => 67
  | 19 => 71
  | 20 => 73
  | 21 => 79
  | 22 => 83
  | 23 => 89
  | 24 => 97
  | 25 => 101
  | 26 => 103
  | 27 => 107
  | 28 => 109
  | 29 => 113
  | 30 => 127
  | 31 => 131
  | 32 => 137
  | 33 => 139
  | 34 => 149
  | 35 => 151
  | 36 => 157
  | 37 => 163
  | 38 => 167
  | 39 => 173
  | 40 => 179
  | 41 => 181
  | 42 => 191
  | 43 => 193
  | 44 => 197
  | 45 => 199
  | 46 => 211
  | 47 => 223
  | 48 => 227
  | 49 => 229
  | 50 => 233
  | 51 => 239
  | 52 => 241
  | 53 => 251
  | 54 => 257
  | 55 => 263
  | 56 => 269
  | 57 => 271
  | 58 => 277
  | 59 => 281
  | 60 => 283
  | 61 => 293
  | 62 => 307
  | 63 => 311
  | 64 => 313
  | 65 => 317
  | _ => 0

/-- `Snum m` is the certified integer sum of `clbZ` over the first `m` primes. -/
def Snum (m : ℕ) : ℕ := ∑ i ∈ Finset.range m, clbZ (ptab i)

/-- Lower bounds for `log (log (Snum m / 10^4))`, for `4 ≤ m ≤ 65` (four
decimal digits; `m = 9` sharper). -/
def rll : ℕ → ℚ
  | 4 => 1.6764
  | 5 => 2.0469
  | 6 => 2.3329
  | 7 => 2.5757
  | 8 => 2.7779
  | 9 => 2.9561126
  | 10 => 3.1174
  | 11 => 3.2589
  | 12 => 3.3888
  | 13 => 3.5069
  | 14 => 3.6137
  | 15 => 3.7124
  | 16 => 3.8049
  | 17 => 3.8918
  | 18 => 3.9724
  | 19 => 4.0485
  | 20 => 4.1203
  | 21 => 4.1876
  | 22 => 4.2518
  | 23 => 4.3128
  | 24 => 4.3712
  | 25 => 4.4274
  | 26 => 4.4811
  | 27 => 4.5322
  | 28 => 4.5812
  | 29 => 4.6282
  | 30 => 4.6733
  | 31 => 4.7176
  | 32 => 4.7602
  | 33 => 4.8015
  | 34 => 4.8412
  | 35 => 4.8800
  | 36 => 4.9174
  | 37 => 4.9537
  | 38 => 4.9890
  | 39 => 5.0233
  | 40 => 5.0566
  | 41 => 5.0891
  | 42 => 5.1207
  | 43 => 5.1515
  | 44 => 5.1815
  | 45 => 5.2108
  | 46 => 5.2393
  | 47 => 5.2673
  | 48 => 5.2948
  | 49 => 5.3216
  | 50 => 5.3478
  | 51 => 5.3734
  | 52 => 5.3985
  | 53 => 5.4230
  | 54 => 5.4471
  | 55 => 5.4707
  | 56 => 5.4939
  | 57 => 5.5166
  | 58 => 5.5389
  | 59 => 5.5608
  | 60 => 5.5822
  | 61 => 5.6032
  | 62 => 5.6239
  | 63 => 5.6444
  | 64 => 5.6645
  | 65 => 5.6842
  | _ => 0

/-- `Pnum m = ∏_{i<m} ptab i`. -/
def Pnum : ℕ → ℕ
  | 0 => 1
  | 1 => 2
  | 2 => 6
  | 3 => 30
  | 4 => 210
  | 5 => 2310
  | 6 => 30030
  | 7 => 510510
  | 8 => 9699690
  | 9 => 223092870
  | 10 => 6469693230
  | 11 => 200560490130
  | 12 => 7420738134810
  | 13 => 304250263527210
  | 14 => 13082761331670030
  | 15 => 614889782588491410
  | 16 => 32589158477190044730
  | 17 => 1922760350154212639070
  | 18 => 117288381359406970983270
  | 19 => 7858321551080267055879090
  | 20 => 557940830126698960967415390
  | 21 => 40729680599249024150621323470
  | 22 => 3217644767340672907899084554130
  | 23 => 267064515689275851355624017992790
  | 24 => 23768741896345550770650537601358310
  | 25 => 2305567963945518424753102147331756070
  | 26 => 232862364358497360900063316880507363070
  | 27 => 23984823528925228172706521638692258396210
  | 28 => 2566376117594999414479597815340071648394470
  | 29 => 279734996817854936178276161872067809674997230
  | 30 => 31610054640417607788145206291543662493274686990
  | 31 => 4014476939333036189094441199026045136645885247730
  | 32 => 525896479052627740771371797072411912900610967452630
  | 33 => 72047817630210000485677936198920432067383702541010310
  | 34 => 10014646650599190067509233131649940057366334653200433090
  | 35 => 1492182350939279320058875736615841068547583863326864530410
  | 36 => 225319534991831177328890236228992001350685163362356544091910
  | 37 => 35375166993717494840635767087951744212057570647889977422429870
  | 38 => 5766152219975951659023630035336134306565384015606066319856068810
  | 39 => 962947420735983927056946215901134429196419130606213075415963491270
  | 40 => 166589903787325219380851695350896256250980509594874862046961683989710
  | 41 => 29819592777931214269172453467810429868925511217482600306406141434158090
  | 42 => 5397346292805549782720214077673687806275517530364350655459511599582614290
  | 43 => 1030893141925860008499560888835674370998623848299590975192766715520279329390
  | 44 => 198962376391690981640415251545285153602734402721821058212203976095413910572270
  | 45 => 39195588149163123383161804554421175259738677336198748467804183290796540382737190
  | 46 => 7799922041683461553249199106329813876687996789903550945093032474868511536164700810
  | 47 => 1645783550795210387735581011435590727981167322669649249414629852197255934130751870910
  | 48 => 367009731827331916465034565550136732339800312955331782619462457039988073311157667212930
  | 49 => 83311209124804345037562846379881038241134671040860314654617977748077292641632790457335110
  | 50 => 19078266889580195013601891820992757757219839668357012055907516904309700014933909014729740190
  | 51 => 4445236185272185438169240794291312557432222642727183809026451438704160103479600800432029464270
  | 52 => 1062411448280052319722448549835623701226301211611796930357321893850294264731624591303255041960530
  | 53 => 256041159035492609053110100510385311995538591998443060216114576417920917800321526504084465112487730
  | 54 => 64266330917908644872330635228106713310880186591609208114244758680898150367880703152525200743234420230
  | 55 => 16516447045902521732188973253623425320896207954043566485360902980990824644545340710198976591011245999110
  | 56 => 4343825573072363215565699965702960859395702691913457985649917484000586881515424606782330843435957697765930
  | 57 => 1168489079156465704987173290774096471177444024124720198139827803196157871127649219224446996884272620699035170
  | 58 => 316660540451402206051523961799780143689087330537799173695893334666158783075592938409825136155637880209438531070
  | 59 => 87714969705038411076272137418539099801877190558970371113762453702525982911939243939521562715111692818014473106390
  | 60 => 24647906487115793512432470614609487044327490547070674282967249490409801198254927547005559122946385681862066942895590
  | 61 => 6975357535853769564018389183934484833544679824821000822079731605785973739106144495802573231793827147966964944839451970
  | 62 => 2043779758005154482257388030892804056228591188672553240869361360495290305558100337270153956915591354354320728837959427210
  | 63 => 627440385707582426053018125484090845262177494922473844946893937672054123806336803541937264773086545786776463753253544153470
  | 64 => 195133959955058134502488637025552252876537200920889365778484014616008832503770745901542489344429915739687480227261852231729170
  | 65 => 61076929465933196099278943388997855150356143888238371488665496574810764573680243467182799164806563626522181311132959748531230210
  | 66 => 19361386640700823163471425054312320082662897612571563761906962414215012369856637179096947335243680669607531475629148240284399976570
  | _ => 0

/-- `Pden m = ∏_{i<m} (ptab i - 1)`. -/
def Pden : ℕ → ℕ
  | 0 => 1
  | 1 => 1
  | 2 => 2
  | 3 => 8
  | 4 => 48
  | 5 => 480
  | 6 => 5760
  | 7 => 92160
  | 8 => 1658880
  | 9 => 36495360
  | 10 => 1021870080
  | 11 => 30656102400
  | 12 => 1103619686400
  | 13 => 44144787456000
  | 14 => 1854081073152000
  | 15 => 85287729364992000
  | 16 => 4434961926979584000
  | 17 => 257227791764815872000
  | 18 => 15433667505888952320000
  | 19 => 1018622055388670853120000
  | 20 => 71303543877206959718400000
  | 21 => 5133855159158901099724800000
  | 22 => 400440702414394285778534400000
  | 23 => 32836137597980331433839820800000
  | 24 => 2889580108622269166177904230400000
  | 25 => 277399690427737839953078806118400000
  | 26 => 27739969042773783995307880611840000000
  | 27 => 2829476842362925967521403822407680000000
  | 28 => 299924545290470152557268805175214080000000
  | 29 => 32391850891370776476185030958923120640000000
  | 30 => 3627887299833526965332723467399389511680000000
  | 31 => 457113799779024397631923156892323078471680000000
  | 32 => 59424793971273171692150010396002000201318400000000
  | 33 => 8081771980093151350132401413856272027379302400000000
  | 34 => 1115284533252854886318271395112165539778343731200000000
  | 35 => 165062110921422523175104166476600499887194872217600000000
  | 36 => 24759316638213378476265624971490074983079230832640000000000
  | 37 => 3862453395561287042297437495552451697360360009891840000000000
  | 38 => 625717450080928500852184874279497174972378321602478080000000000
  | 39 => 103869096713434131141462689130396531045414801386011361280000000000
  | 40 => 17865484634710670556331582530428203339811345838393954140160000000000
  | 41 => 3180056264978499359027021690416220194486419559234123836948480000000000
  | 42 => 572410127696129884624863904274919635007555520662142290650726400000000000
  | 43 => 108757924262264678078724141812234730651435548925807035223638016000000000000
  | 44 => 20881521458354818191115035227949068285075625393754950762938499072000000000000
  | 45 => 4092778205837544365458546904678017383874822577175970349535945818112000000000000
  | 46 => 810370084755833784360792287126247442007214870280842129208117271986176000000000000
  | 47 => 170177717798725094715766380296511962821515122758976847133704627117096960000000000000
  | 48 => 37779453351316971026900136425825655746376357252492860063682427219995525120000000000000
  | 49 => 8538156457397635452079430832236598198681056739063386374392228551718988677120000000000000
  | 50 => 1946699672286660883074110229749944389299280936506452093361428109791929418383360000000000000
  | 51 => 451634323970505324873193573301987098317433177269496885659851321471727625064939520000000000000
  | 52 => 107488969104980267319820070445872929399549096190140258787044614510271174765455605760000000000000
  | 53 => 25797352585195264156756816907009503055891783085633662108890707482465081943709345382400000000000000
  | 54 => 6449338146298816039189204226752375763972945771408415527222676870616270485927336345600000000000000000
  | 55 => 1651030565452496906032436282048608195577074117480554374969005278877765244397398104473600000000000000000
  | 56 => 432570008148554189380498305896735347241193418779905246241879383065974494032118303372083200000000000000000
  | 57 => 115928762183812522753973545980325073060639836233014605992823674661681164400607705303718297600000000000000000
  | 58 => 31300765789629381143572857414687769726372755782913943618062392158653914388164080432003940352000000000000000000
  | 59 => 8639011357937709195626108646453824444478880596084248438585220235788480371133286199233087537152000000000000000000
  | 60 => 2418923180222558574775310421007070844454086566903589562803861666020774503917320135785264510402560000000000000000000
  | 61 => 682136336822761518086637538723993978136052411866812256710688989817858410104684278291444591933521920000000000000000000
  | 62 => 199183810352246363281298161307406241615727304265109178959521185026814655750567809261101820844588400640000000000000000000
  | 63 => 60950245967787387164077237360066309934412555105123408761613482618205284659673749633897157178444050595840000000000000000000
  | 64 => 18894576250014090020863943581620556079667892082588256716100179611643638244498862386508118725317655684710400000000000000000000
  | 65 => 5895107790004396086509550397465613496856382329767536095423256038832815132283645064590533042299108573629644800000000000000000000
  | 66 => 1862854061641389163337017925599133865006616816206541406153748908271169581801631840410608441366518309266967756800000000000000000000
  | _ => 0

/-- `Qpt m = ∏_{i<m} ptab i / (ptab i - 1)`, computed as the ratio of the
numerator and denominator tables. -/
def Qpt (m : ℕ) : ℚ := (Pnum m : ℚ) / (Pden m : ℚ)

end TaoFivePrimes