Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence4LookupScalar0MainPart0.Coefficients0To42

Recurrence 4 lookup certificate: Scalar0Main coefficient convolution #

This is a checked coefficient-lookup shard for the fourth pseudo-division recurrence in the order-seven certificate.

source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_0 :
Polynomial.coeff recurrence4Scalar0Main 0 = 0
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_1 :
Polynomial.coeff recurrence4Scalar0Main 1 = -435825609627186405888604163324323151216640
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_2 :
Polynomial.coeff recurrence4Scalar0Main 2 = 2116116209613328031798796630434159331093577728
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_3 :
Polynomial.coeff recurrence4Scalar0Main 3 = 13201802557796501963933618362579337219325910227456
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_4 :
Polynomial.coeff recurrence4Scalar0Main 4 = -119489780296283556312355559268225234944183539148182336
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_5 :
Polynomial.coeff recurrence4Scalar0Main 5 = 356361255999808623131583131131167291935524552689994504896
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_6 :
Polynomial.coeff recurrence4Scalar0Main 6 = -574411738728221473156549251771091254470352308527446853969120
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_7 :
Polynomial.coeff recurrence4Scalar0Main 7 = 575182431377434986845617404673338944019311256502555251720206208
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_8 :
Polynomial.coeff recurrence4Scalar0Main 8 = -360038273207254347568309589344126725292914825882910556437446403380
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_9 :
Polynomial.coeff recurrence4Scalar0Main 9 = 113699382593813184783524128811134550988326660151820960369544026146844
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_10 :
Polynomial.coeff recurrence4Scalar0Main 10 = 1 * 10 ^ 70 + 4298939520913294458117501030456356440461825634590980556613892120469364
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_11 :
Polynomial.coeff recurrence4Scalar0Main 11 = -(3297 * 10 ^ 70 + 4423109276605818013703360741947491050992987143982211874126232532147248)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_12 :
Polynomial.coeff recurrence4Scalar0Main 12 = 1298616 * 10 ^ 70 + 1220131634804700832098906603670739728863507295802743148691407835973120
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_13 :
Polynomial.coeff recurrence4Scalar0Main 13 = 178801167 * 10 ^ 70 + 6907642364822362038023054242851900285937695332915167382391618519738952
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_14 :
Polynomial.coeff recurrence4Scalar0Main 14 = -(439823500908 * 10 ^ 70 + 5385662356183846923844999122824588355492001319163587208912450424452212)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_15 :
Polynomial.coeff recurrence4Scalar0Main 15 = 227575145541816 * 10 ^ 70 + 7894873059716703761549674715331146416351989964119349653206240836505179
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_16 :
Polynomial.coeff recurrence4Scalar0Main 16 = -(57697309618153679 * 10 ^ 70 + 151985186543127599871889134039196056638974179935467621790122560058276)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_17 :
Polynomial.coeff recurrence4Scalar0Main 17 = 3099921679552154928 * 10 ^ 70 + 2744783413800600530330113218291496250531862121727941654032478402917698
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_18 :
Polynomial.coeff recurrence4Scalar0Main 18 = 2218089241413580000281 * 10 ^ 70 + 9601721879799424983222403108034569815710004388146507195771690435932323
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_19 :
Polynomial.coeff recurrence4Scalar0Main 19 = 76617062721843146618571 * 10 ^ 70 + 6748452926091755373578959812040000935013725420303465646753800706289874
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_20 :
Polynomial.coeff recurrence4Scalar0Main 20 = -(724488358164503132936966812 * 10 ^ 70 + 353093819247959300720862095172131713593220933129044634371679400662904)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_21 :
Polynomial.coeff recurrence4Scalar0Main 21 = 432192659813033311042455866958 * 10 ^ 70 + 7415653043363602467629770238372012775613058661209511556978389445737155
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_22 :
Polynomial.coeff recurrence4Scalar0Main 22 = -(152920852263140044771577423964457 * 10 ^ 70 + 1931936293496822857845454100836589908097093236523273501205846392031837)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_23 :
Polynomial.coeff recurrence4Scalar0Main 23 = 37980669723644817018067669315916764 * 10 ^ 70 + 2088948325684097043666037730239671540109853040885510848422909215955987
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_24 :
Polynomial.coeff recurrence4Scalar0Main 24 = -(6746565495241057894772746972692351835 * 10 ^ 70 + 8732095910376642899002848130688842782153376590925039663669682635082229)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_25 :
Polynomial.coeff recurrence4Scalar0Main 25 = 750799017527074496827323371376624157797 * 10 ^ 70 + 3097675686361266735675345509632793497536820962903482570714037114434714
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_26 :
Polynomial.coeff recurrence4Scalar0Main 26 = 4880150155609270301059519071713886808452 * 10 ^ 70 + 125691451262290754662840812254697115483352580878373590896819390968890
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_27 :
Polynomial.coeff recurrence4Scalar0Main 27 = -(29608732993395772998781027146953404813010802 * 10 ^ 70 + 9179206765877105437214615072118481356704146180107681937250851822124588)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_28 :
Polynomial.coeff recurrence4Scalar0Main 28 = 10644299135896416966483880698092291590808377564 * 10 ^ 70 + 2768460410438562829481227148389786883850435189692470678357797239963305
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_29 :
Polynomial.coeff recurrence4Scalar0Main 29 = -(2944417813645439710016101515318161057063282060236 * 10 ^ 70 + 9566506290898679110126409514063953017172131905304311426406021101036441)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_30 :
Polynomial.coeff recurrence4Scalar0Main 30 = 726433680677019007474786699021784903600137649610109 * 10 ^ 70 + 5476153452303053210058950533562399071563303371557367430449972702354941
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_31 :
Polynomial.coeff recurrence4Scalar0Main 31 = -(161094180153379009459285860325012739110765706152648508 * 10 ^ 70 + 673177975330332647116022315584679810008302580789184185570079279679430)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_32 :
Polynomial.coeff recurrence4Scalar0Main 32 = 31461505480468380588703616042770110794170779818650415165 * 10 ^ 70 + 8477222015092223838178066170009061446585299520361241352149747478322993
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_33 :
Polynomial.coeff recurrence4Scalar0Main 33 = -(5292315158893077766637780397373598426239016827359520746426 * 10 ^ 70 + 3194858306837266829052217903907277120860806807262531218608297234744145)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_34 :
Polynomial.coeff recurrence4Scalar0Main 34 = 744959497450480346460923175037379080853277200944905299463491 * 10 ^ 70 + 2007657678772025542242481222352349361374351626272291935042530703610836
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_35 :
Polynomial.coeff recurrence4Scalar0Main 35 = -(82323163121902221450431236329429211015752142934123899459876970 * 10 ^ 70 + 7150353176640810032463840734707177881681457968998957454375569081070985)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_36 :
Polynomial.coeff recurrence4Scalar0Main 36 = 5613871797102752308825429578020456534141809413823617164052842274 * 10 ^ 70 + 9774380939141532748928151284654052689585950472192572010851712218341603
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_37 :
Polynomial.coeff recurrence4Scalar0Main 37 = 238619803034692156886361629261424020198214162606661855175517847711 * 10 ^ 70 + 37450821956624555668262061200074526039051287998449909592288035008310
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_38 :
Polynomial.coeff recurrence4Scalar0Main 38 = -(166146954692616121166958399974456613145438759761993507768519836223704 * 10 ^ 70 + 3064425809112317244783107287245201781127303448196661307213686326078153)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_39 :
Polynomial.coeff recurrence4Scalar0Main 39 = (3 * 10 ^ 70 + 5804883542222935598680377358317936754311106201344480102084139628725904) * 10 ^ 70 + 8715774518147574599463641261484433044633812783519529058003648499918297
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_40 :
Polynomial.coeff recurrence4Scalar0Main 40 = -((563 * 10 ^ 70 + 5112893082092812657762473584894361360949556009477410171267700336626622) * 10 ^ 70 + 122022073544022475138699268294629285272854155740872664440545155345738)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_41 :
Polynomial.coeff recurrence4Scalar0Main 41 = (73202 * 10 ^ 70 + 2392411996189186105978327058354143378144033243299921679983852550948775) * 10 ^ 70 + 5880249804097136511113363381669276088780834094174439672798941392620572
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_42 :
Polynomial.coeff recurrence4Scalar0Main 42 = -((8162926 * 10 ^ 70 + 3763286729128462906503499846339383789905517112711229763437573076235813) * 10 ^ 70 + 1857431156920736464322054602280492201569454398543718017548359898914243)