Recurrence 2 lookup certificate: Scalar4Main coefficient convolution #
This is a checked coefficient-lookup shard for the second pseudo-division recurrence in the order-seven certificate.
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_18 :
Polynomial.coeff recurrence2Scalar4Main 18 = -20353418814107303099029103807745798884839481581506009273
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_19 :
Polynomial.coeff recurrence2Scalar4Main 19 = 1581348607168643735193590308757357878381380952998329628657
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_20 :
Polynomial.coeff recurrence2Scalar4Main 20 = -91613463484000408122859167471709724971594235209925399509704
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_21 :
Polynomial.coeff recurrence2Scalar4Main 21 = 3362895072337246421970539926197033299072690334540022718846116
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_22 :
Polynomial.coeff recurrence2Scalar4Main 22 = 3236177908509504561074664452017666418996221846508700695131225
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_23 :
Polynomial.coeff recurrence2Scalar4Main 23 = -12073189214839841896399852282392545181426566136101219112282944976
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_24 :
Polynomial.coeff recurrence2Scalar4Main 24 = 1133950865713386967368814247800034955197110951269964651327242189721
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_25 :
Polynomial.coeff recurrence2Scalar4Main 25 = -67046835957481374794204915342108721999972616382079831077304003191512
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_26 :
Polynomial.coeff recurrence2Scalar4Main 26 = 2631456392340516607937015199329241194956040528172990436207381288263100
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_27 :
Polynomial.coeff recurrence2Scalar4Main 27 = -(3 * 10 ^ 70 + 6081947441045949917891851730056392974796481933781132703585175242658638)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_28 :
Polynomial.coeff recurrence2Scalar4Main 28 = -(434 * 10 ^ 70 + 8228445539279716202190039865932775439611063680157929426149341345168506)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_29 :
Polynomial.coeff recurrence2Scalar4Main 29 = 47263 * 10 ^ 70 + 4159529257082267868672721380591614973748609201160717539567418188853958
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_30 :
Polynomial.coeff recurrence2Scalar4Main 30 = -(2897142 * 10 ^ 70 + 4069604605716771596449321477038994243256351672674033283278551834625921)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_31 :
Polynomial.coeff recurrence2Scalar4Main 31 = 128804979 * 10 ^ 70 + 3159381907641390317279288579144892950706200645209176939250952303350199
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_32 :
Polynomial.coeff recurrence2Scalar4Main 32 = -(4090080286 * 10 ^ 70 + 2452713159666853904214766548469147457897883873454883355230895876828134)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_33 :
Polynomial.coeff recurrence2Scalar4Main 33 = 60236757903 * 10 ^ 70 + 2277114294693727580410149091589464853653074017801610408636472201861460
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_34 :
Polynomial.coeff recurrence2Scalar4Main 34 = 3075251495715 * 10 ^ 70 + 8204603919086240991036050915070225930120782084941969539552392966674416
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_35 :
Polynomial.coeff recurrence2Scalar4Main 35 = -(322652558811675 * 10 ^ 70 + 3836026331147777066624765173618566120298215015846947301817771947434301)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_36 :
Polynomial.coeff recurrence2Scalar4Main 36 = 17196519308938885 * 10 ^ 70 + 5763480630064009021145425151018818547100870150286408297370015708360155
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_37 :
Polynomial.coeff recurrence2Scalar4Main 37 = -(663084583324531001 * 10 ^ 70 + 6928382168052673279817221168622425829031390167727105468226207772565903)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_38 :
Polynomial.coeff recurrence2Scalar4Main 38 = 19571265022454862880 * 10 ^ 70 + 9994159090442480873384296876967267201357869067338608689707836326763837
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_39 :
Polynomial.coeff recurrence2Scalar4Main 39 = -(434402180760613279469 * 10 ^ 70 + 447230961482820764939717652703064534399034696396545887521000128238789)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_40 :
Polynomial.coeff recurrence2Scalar4Main 40 = 6483126182535593169574 * 10 ^ 70 + 8029123225484672588699599760829269788616587525694574717047997533060481
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_41 :
Polynomial.coeff recurrence2Scalar4Main 41 = -(31650637528139668185442 * 10 ^ 70 + 7102387951478644976794048226507172964736953689429997668724177611091365)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_42 :
Polynomial.coeff recurrence2Scalar4Main 42 = -(1317241765267522884683902 * 10 ^ 70 + 8534898847333782491743209246126736218203953480748384209399925355802158)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_43 :
Polynomial.coeff recurrence2Scalar4Main 43 = 37196497490964372819954239 * 10 ^ 70 + 9621626226854229031693894436248793545263852606127338841102790767394403
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_44 :
Polynomial.coeff recurrence2Scalar4Main 44 = -(191631976988440352304910640 * 10 ^ 70 + 8059721362994064989930891576639587249834825960591770091535440990222095)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_45 :
Polynomial.coeff recurrence2Scalar4Main 45 = -(14017755055104280889294085241 * 10 ^ 70 + 3224353303888201995953837807537825295293693934777013891668139516777745)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_46 :
Polynomial.coeff recurrence2Scalar4Main 46 = 441559353242691785442136801407 * 10 ^ 70 + 4513908551761020564737504546556870823243662574357395242802996177862847
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_47 :
Polynomial.coeff recurrence2Scalar4Main 47 = -(3185999894931051309344435075307 * 10 ^ 70 + 8714614356131859603163059674033137837247556564838366942780497948315332)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_48 :
Polynomial.coeff recurrence2Scalar4Main 48 = -(215536373114938785338375196636209 * 10 ^ 70 + 8297364102940351897328227265258851293871100686239408152464828703470228)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_49 :
Polynomial.coeff recurrence2Scalar4Main 49 = 10952506632125987856817621130607884 * 10 ^ 70 + 4149718188343869932910140650428397959533145128252240994446536784300105
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_50 :
Polynomial.coeff recurrence2Scalar4Main 50 = -(317917730501661704176150114287425366 * 10 ^ 70 + 5326856347341669947693751841104978866540221730883982305359559374918632)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_51 :
Polynomial.coeff recurrence2Scalar4Main 51 = 7005456112974587241384012109193096120 * 10 ^ 70 + 7358578698788570048052194289528846739138196036054345063193393140421185
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_52 :
Polynomial.coeff recurrence2Scalar4Main 52 = -(126851765244169990384380893340945365174 * 10 ^ 70 + 6096689713337402501651328548024120043962138845420608044311483637821710)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_53 :
Polynomial.coeff recurrence2Scalar4Main 53 = 1937709118074667890715593937499706881479 * 10 ^ 70 + 9620599064184356377266084991088851337120522117455543845080582542709072
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_54 :
Polynomial.coeff recurrence2Scalar4Main 54 = -(24623929391431641338611045835260054188912 * 10 ^ 70 + 8164323636681492473548597685800033959646535997336208496010148127420283)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_55 :
Polynomial.coeff recurrence2Scalar4Main 55 = 234446314243960867728896408926262150033341 * 10 ^ 70 + 3989732927621179774087386254759192221363146369553891854125527588462539
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_56 :
Polynomial.coeff recurrence2Scalar4Main 56 = -(727108551778550120984680002452101350044293 * 10 ^ 70 + 8507375771051627221467495164843639889354142234574977195853295255587428)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_57 :
Polynomial.coeff recurrence2Scalar4Main 57 = -(36456429221933729350567761045044494322057394 * 10 ^ 70 + 5202198478266821386328803196310881194251420065583190618232177175452901)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_58 :
Polynomial.coeff recurrence2Scalar4Main 58 = 1223925292547623501750649970459019548170361188 * 10 ^ 70 + 8777728203047542219120982669986039055382867205016162054043828655920814
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_59 :
Polynomial.coeff recurrence2Scalar4Main 59 = -(26162815009729504066136575674876129015101947089 * 10 ^ 70 + 4843658303545582553159591004051320073724954114662762173541161757615091)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_60 :
Polynomial.coeff recurrence2Scalar4Main 60 = 452786705577841346236822838666822620884452185142 * 10 ^ 70 + 3544714683355292602201881240913480576269417186330568700541624152987359
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_61 :
Polynomial.coeff recurrence2Scalar4Main 61 = -(6733666220336704824639590936406250599459485235030 * 10 ^ 70 + 3226218194094742112590482936429464472561496609857086330943044464414836)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_62 :
Polynomial.coeff recurrence2Scalar4Main 62 = 87650955310926674250591896726281942534591525939647 * 10 ^ 70 + 7349708317745592096408558268794252764534720136929010300901443194981151
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_63 :
Polynomial.coeff recurrence2Scalar4Main 63 = -(996907028333650168796638736647200215531259192573477 * 10 ^ 70 + 9839548413154013551974678819397701211850175090000090260516654861788227)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_64 :
Polynomial.coeff recurrence2Scalar4Main 64 = 9654606362158582774465279309070927478386515804500069 * 10 ^ 70 + 7943961096181468113316149164461790404957582558571205559596677952532468
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_65 :
Polynomial.coeff recurrence2Scalar4Main 65 = -(72825580349139250446053180550500455440680759324662956 * 10 ^ 70 + 9310087330568291941127114051284597575330014418436504312250665102449490)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_66 :
Polynomial.coeff recurrence2Scalar4Main 66 = 263802642964431761674668970327998799313594710435981244 * 10 ^ 70 + 2081279003682151457708412127948336688205111968909928476121103986158357
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_67 :
Polynomial.coeff recurrence2Scalar4Main 67 = 4065052847498050757509705752733266047845901890764243241 * 10 ^ 70 + 5334776588735574854601167764800584065911961743320753308126592742219004
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_68 :
Polynomial.coeff recurrence2Scalar4Main 68 = -(121768510833189567120376917953968156625107382182232112695 * 10 ^ 70 + 6417276591343342043176254544810405154183838420875729489129948094709862)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_69 :
Polynomial.coeff recurrence2Scalar4Main 69 = 2071105166327971700256300716635169499070171589398739692074 * 10 ^ 70 + 2702763705904534643340542362363991594247293435991000190238804049024569
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_70 :
Polynomial.coeff recurrence2Scalar4Main 70 = -(28536363578583557116654752787894420189161011528685256207161 * 10 ^ 70 + 6944984519673493505648486649338357319655553877839790464682507330595439)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_71 :
Polynomial.coeff recurrence2Scalar4Main 71 = 346167489162428908870570693257398419718577939526276127229287 * 10 ^ 70 + 3189369097329253787619617731549149611693142554514221592536008919045109
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_72 :
Polynomial.coeff recurrence2Scalar4Main 72 = -(3823266614824763301269698923365357628920246321488647930594371 * 10 ^ 70 + 318053377206044947855834348157130041673314001234180840575205811656594)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_73 :
Polynomial.coeff recurrence2Scalar4Main 73 = 39115109276825238708146228251463183583386273000382381583588517 * 10 ^ 70 + 8694652233946433786547349253204357488025355307260375341107714894647928
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_74 :
Polynomial.coeff recurrence2Scalar4Main 74 = -(374552198524176249013465015478124844500208540778643147694788954 * 10 ^ 70 + 379608640647238845808678063856799595093507097861900623967140183098523)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_75 :
Polynomial.coeff recurrence2Scalar4Main 75 = 3380017570118113054698705114444925891064855305695418141412919067 * 10 ^ 70 + 1842366703768101632284679341306572984330801916497137629389419603270367
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_76 :
Polynomial.coeff recurrence2Scalar4Main 76 = -(28884495551723703889849846768855156030105913285051379720098725791 * 10 ^ 70 + 6045767787689506691405514391545618010475351366760532737634982735531105)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_77 :
Polynomial.coeff recurrence2Scalar4Main 77 = 234570519555910204472982081345532100762381662515172806558616194446 * 10 ^ 70 + 6553758305200577870289342763962758826923486358348597391416914686441359
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_78 :
Polynomial.coeff recurrence2Scalar4Main 78 = -(1814934973080970050504009075785489512709820119131772123670703264425 * 10 ^ 70 + 1395939284270716765267622493028102445935541889803435631559519048413305)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_79 :
Polynomial.coeff recurrence2Scalar4Main 79 = 13404555373588168527926642033946613254431870144164614257963460668154 * 10 ^ 70 + 3515823900173651438263693014172686207544454707950765135769312147430851
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_80 :
Polynomial.coeff recurrence2Scalar4Main 80 = -(94639624845464271214266950520258821693959212281925361030371106890289 * 10 ^ 70 + 6085746141846167396595791673448035272364402068303747636330222064319137)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_81 :
Polynomial.coeff recurrence2Scalar4Main 81 = 639473917762548384974541323727361877869588767514173082467900560784960 * 10 ^ 70 + 8557330450143419721853864334705797375612829232394786450591424072769084
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_82 :
Polynomial.coeff recurrence2Scalar4Main 82 = -(4139286124390950655737272846401902128052583611812816664488007173014253 * 10 ^ 70 + 995262462156889442807256761560461149716916022804286413707981962983447)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_83 :
Polynomial.coeff recurrence2Scalar4Main 83 = (2 * 10 ^ 70 + 5688958623154166703514619426854955764319010861582829470483606219367822) * 10 ^ 70 + 1945308598582825404579579739928430977112857855187935374687213078173234
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_84 :
Polynomial.coeff recurrence2Scalar4Main 84 = -((15 * 10 ^ 70 + 2961379717130581003620433140809714885798062003086966891253778488399675) * 10 ^ 70 + 7640352757159351034778587094335153542937213238411904904356805494714006)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_85 :
Polynomial.coeff recurrence2Scalar4Main 85 = (87 * 10 ^ 70 + 4228283458439234023731365722513584585126469893515110004003271827953378) * 10 ^ 70 + 3215259585473116127739922393831734862184828755521409839478497003232446
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_86 :
Polynomial.coeff recurrence2Scalar4Main 86 = -((479 * 10 ^ 70 + 6590440366610652147042962282103064143011155515043962457899160652842453) * 10 ^ 70 + 4455226841541514872807707840832555759705954970108349788536147944166210)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_87 :
Polynomial.coeff recurrence2Scalar4Main 87 = (2525 * 10 ^ 70 + 8658111264268051598399235535749638603713536592161243422197969531033317) * 10 ^ 70 + 2195886391504153322881171560006594725642089370943220560237272599305092
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_88 :
Polynomial.coeff recurrence2Scalar4Main 88 = -((12759 * 10 ^ 70 + 3282205886969645508097734383966185912030844640882306903838497069242171) * 10 ^ 70 + 1550850119707813458697299454642059565425951947749099350669446451654163)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_89 :
Polynomial.coeff recurrence2Scalar4Main 89 = (61782 * 10 ^ 70 + 2426650271630625565318008889360594826812732729203317700877237189642741) * 10 ^ 70 + 5346563152903707861222318501971684964961555094933673215039702747133180
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_90 :
Polynomial.coeff recurrence2Scalar4Main 90 = -((286513 * 10 ^ 70 + 7970291019839863854815495474156533433743721717484986334017533143350492) * 10 ^ 70 + 3463487591854299172453879144253473725370884070559868296978703616501400)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_91 :
Polynomial.coeff recurrence2Scalar4Main 91 = (1271268 * 10 ^ 70 + 3718929608219034112632952200725768803857337787167444222884577663182383) * 10 ^ 70 + 5508237398944266902971106770811567916678764274429857509373601206814292
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_92 :
Polynomial.coeff recurrence2Scalar4Main 92 = -((5389006 * 10 ^ 70 + 1206691789751893371121117702095722304404405330217470161350303461472073) * 10 ^ 70 + 8611451752313659556319946213334747953464122562834966530941411957264616)