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.

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_142 : Polynomial.coeff recurrence4Scalar0Main 142 = ((7659902613887767146396138655096209676962724117470083757019216 * 10 ^ 70 + 6636087029906198476887236191508081776962276471500387431529034266307471) * 10 ^ 70 + 3686811172095162233810866214380505576723889098215680999552732737294477) * 10 ^ 70 + 4529229744646153033216678383485236193620458224764881680853170566065630

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_143 : Polynomial.coeff recurrence4Scalar0Main 143 = -(((38694428100341364581132723221678609407164283378094852944151515 * 10 ^ 70 + 6750030356102137443035725246820371263720964956249176510057118961036403) * 10 ^ 70 + 1689629072565158371189024485570161981225593607157723090191587297186127) * 10 ^ 70 + 9965089678869358579745411358157764734093144315895264914118295287484560)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_144 : Polynomial.coeff recurrence4Scalar0Main 144 = ((192022606781095257019322593806804769019442498838756663596191283 * 10 ^ 70 + 4562731815902399414059707644637909643701041724922167163413147379851719) * 10 ^ 70 + 6357843137173682424607024307799148419783984229947917998652887140956231) * 10 ^ 70 + 398573580522051656238197692765575787580173498999291529683454615691859

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_145 : Polynomial.coeff recurrence4Scalar0Main 145 = -(((936250832392269050691260395457946025787496036677917544574305611 * 10 ^ 70 + 7756911509724449342464077779658713687551183099587123474928228918300557) * 10 ^ 70 + 4113755866245278480357065797999839269075310269891801898186528151771306) * 10 ^ 70 + 9300431385787490199650812323314505396636910656061006246306875755998582)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_146 : Polynomial.coeff recurrence4Scalar0Main 146 = ((4485631294158060185411533622556540701129264790638992225439976779 * 10 ^ 70 + 4511045654266343971230828422146257186500314675614056533504767530468486) * 10 ^ 70 + 3820888526889718582282798452127964230083412743957644767753238844204623) * 10 ^ 70 + 1990513756239053533762182273187834966236365524697886533640727541256289

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_147 : Polynomial.coeff recurrence4Scalar0Main 147 = -(((21120317633952658623267128191980875018011652328893745458156118900 * 10 ^ 70 + 1839155753262915805715248802770621534015511107918174371478981265722935) * 10 ^ 70 + 3361990199168310041451634743656812847871475832081584125496571152381431) * 10 ^ 70 + 8847347815752156793465929559726109572903862086672950321813108398287425)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_148 : Polynomial.coeff recurrence4Scalar0Main 148 = ((97740676319435621541429471993521993738367321088116116489021914220 * 10 ^ 70 + 9348693332089915655320260626097939678472357322085530205194449575591795) * 10 ^ 70 + 9076660825949483536665029507033809942941113933039487154330820867184696) * 10 ^ 70 + 8497768648054743862764527783345851822994223875540325878509161749988704

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_149 : Polynomial.coeff recurrence4Scalar0Main 149 = -(((444630547835142644474004331547550368553819641217632842141011539315 * 10 ^ 70 + 4402741340933484876208055699057847654082494519386085322690497117036343) * 10 ^ 70 + 4995898293981016001646666244344996474785867943164496978232943806818502) * 10 ^ 70 + 6117272247743623228678865580240347029983202814403676369345364509377548)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_150 : Polynomial.coeff recurrence4Scalar0Main 150 = ((1988483244281888577399321862409137508239795969650592037909688683920 * 10 ^ 70 + 376031619236640959133092179819972697210530158710746693838193328647923) * 10 ^ 70 + 5463083722406228397601825363375080819343018407557668956655361303965871) * 10 ^ 70 + 1589257887153187110631629315176407183631513113650959789596136234581108

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_151 : Polynomial.coeff recurrence4Scalar0Main 151 = -(((8743624390345727672018950956318906460240553135477921083688287801995 * 10 ^ 70 + 6816118381986574242031000761942952985984963634431387139180571641034955) * 10 ^ 70 + 5750909706818423256700617324050288467337375537669191481809156893256106) * 10 ^ 70 + 7245558708332140564275231749055225049553394323817708535513178032563270)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_152 : Polynomial.coeff recurrence4Scalar0Main 152 = ((37805489193205786835350759011554562668397953254944196753441392840704 * 10 ^ 70 + 1335097371288162240636025692530235384620639936468937529483403002888643) * 10 ^ 70 + 3840909026603547919995788851876067276117219846111088025890387375307990) * 10 ^ 70 + 4770133101813372291996429870607441288568326022987409114946753925223337

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_153 : Polynomial.coeff recurrence4Scalar0Main 153 = -(((160752461197347484172338800319453778403969152609936193462981090049456 * 10 ^ 70 + 8023038385572916814412794460869833957347186534177671030872842827886378) * 10 ^ 70 + 2214190843783715507384121876010733057342024638377742138499308169044351) * 10 ^ 70 + 1868609115038590173191082196012019222469325983129789127402884385301321)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_154 : Polynomial.coeff recurrence4Scalar0Main 154 = ((672270594487392492283077119572277213600766877257453186326500512032511 * 10 ^ 70 + 4309458530241645593651926314126856860466178438979993850010826683164464) * 10 ^ 70 + 1281245854895091407035306931786285790997192691379081551454532762107973) * 10 ^ 70 + 5333439875948836112550584715975304632494321853394222696798887211104455

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_155 : Polynomial.coeff recurrence4Scalar0Main 155 = -(((2765396403344830624479953682675119649014223824620168094320907010065136 * 10 ^ 70 + 5994687737813153715885970885928491580050374472395158582814081093795547) * 10 ^ 70 + 3307801526494365496136488461501222389991408892688961796254843410089924) * 10 ^ 70 + 4872389310468113675170821462394980423853403812196118095836208580873202)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_156 : Polynomial.coeff recurrence4Scalar0Main 156 = (((1 * 10 ^ 70 + 1190238376600526291935807579677344253051911924736063083373434072326601) * 10 ^ 70 + 6039032082540987445535720789239498121099061964078253963268105843914028) * 10 ^ 70 + 5543224636162168930016720644116100044479435042631954020664513311002308) * 10 ^ 70 + 3857981649186573754563406256104924306598630122948634800248700319599283

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_157 : Polynomial.coeff recurrence4Scalar0Main 157 = -((((4 * 10 ^ 70 + 4548249722536241003954479941719888354106318985447548239750547457270059) * 10 ^ 70 + 8790413711147610071928319033768980376133679545738515328145856793597376) * 10 ^ 70 + 7505821024902332453461066965487338095629532068015975951197992554306302) * 10 ^ 70 + 8577484506773176393530731713953418391189853274820699677577298999597708)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_158 : Polynomial.coeff recurrence4Scalar0Main 158 = (((17 * 10 ^ 70 + 4490130349898643384757434960958165226057363465747662079649691443819218) * 10 ^ 70 + 3808503190080835086752804384981299184605619740326647138078969501753676) * 10 ^ 70 + 5112328456894221824416459922027982622391959437766728567710404636828838) * 10 ^ 70 + 7376963741627409212651732658166264000508900625205209692117135395894425

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_159 : Polynomial.coeff recurrence4Scalar0Main 159 = -((((67 * 10 ^ 70 + 2509519172873118782995897020867201800954425593299754166603174400656438) * 10 ^ 70 + 5972833434841808214831984742435106109823766505432092224485978727263252) * 10 ^ 70 + 5167441959772241569541724386830280326597655591988630084131246780798735) * 10 ^ 70 + 5007488775414707490314774769439160076425578115675801007384764144783129)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_160 : Polynomial.coeff recurrence4Scalar0Main 160 = (((255 * 10 ^ 70 + 648977883067557412234764190854417909815812637408064625922992653930848) * 10 ^ 70 + 8805571273096841659146301911080552774204311084731312569336590366105393) * 10 ^ 70 + 5172971624316189559862018260151222872418598016670119446230916218600978) * 10 ^ 70 + 6995164678405419856759783205392231732052018749032534281253562960052430

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_161 : Polynomial.coeff recurrence4Scalar0Main 161 = -((((952 * 10 ^ 70 + 591274296994711327336746158926198738139770226359635231070443402448438) * 10 ^ 70 + 9314232713876071309432250663793197727465835007970379000064093929792424) * 10 ^ 70 + 8508999086695682263079512629391861816023118162414926732647221894460439) * 10 ^ 70 + 4370303467028671409868850086855697555170586647881377930812464433996310)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_162 : Polynomial.coeff recurrence4Scalar0Main 162 = (((3497 * 10 ^ 70 + 6258668124513937570641168788868608237209332418825887296798196133668163) * 10 ^ 70 + 6492634005989380558261412115957818801994164231029914303644463205710214) * 10 ^ 70 + 4294307347989660810238367063620810509376191982014829809943656402209393) * 10 ^ 70 + 1034712779181249622526170465512430720256065430280506940535212564958245

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_163 : Polynomial.coeff recurrence4Scalar0Main 163 = -((((12647 * 10 ^ 70 + 7481662841833526262558255832137828728521615967061992685417311989205971) * 10 ^ 70 + 7396644738623992966792013116982260055749052850706237288650639173709409) * 10 ^ 70 + 199462393519374542418758192663385176409168203291397252675036452692232) * 10 ^ 70 + 3006748389555462612993472257717268391174669539433443527674732199619934)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_164 : Polynomial.coeff recurrence4Scalar0Main 164 = (((45021 * 10 ^ 70 + 1642494632517913178134885316805546543892925726835572130546278480176703) * 10 ^ 70 + 4632894298725626074169680437724715225728893476677275293738733092212856) * 10 ^ 70 + 2217527271888192511240117492083855857362907019773647853483018140068042) * 10 ^ 70 + 277727385993517113653297110963359644921713134266167239402191922675820

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_165 : Polynomial.coeff recurrence4Scalar0Main 165 = -((((157766 * 10 ^ 70 + 9919879162658493380709601373570057997537751799819792025493308333714423) * 10 ^ 70 + 8293234553835675134842999473928323468037726807897232366460708410203211) * 10 ^ 70 + 676811802690408673813119801038759330129870861341699401917680323498144) * 10 ^ 70 + 3025360813420406010759357288754057463917882570417006666926556647826959)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_166 : Polynomial.coeff recurrence4Scalar0Main 166 = (((544305 * 10 ^ 70 + 5808472011808337915818480959892662472841258010867493628010021959918761) * 10 ^ 70 + 3817756649193890126281708650377491952581443828599565413624095321560467) * 10 ^ 70 + 1023955475027804132482570100962292643919219843708391216238520559710236) * 10 ^ 70 + 4933887253643818271819789706004345359535170577786036636702461509494217

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_167 : Polynomial.coeff recurrence4Scalar0Main 167 = -((((1848957 * 10 ^ 70 + 9078181284952301054407459113024337374403760014849092599022168617520061) * 10 ^ 70 + 4423013250119686582927394751951767132168225616570158993632114154674977) * 10 ^ 70 + 1499870853405767120172786240704044445429085565446542685544251306433606) * 10 ^ 70 + 8294960600569852947051211196149207844391492631182116128801161634938182)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_168 : Polynomial.coeff recurrence4Scalar0Main 168 = (((6184410 * 10 ^ 70 + 7026679744029776106610798978009118355784515070661299356380623651808861) * 10 ^ 70 + 3313205665078717386174939531143390237376020775632080205339386608210586) * 10 ^ 70 + 2796571845961263237605615420259025263877554015561844808800226206801932) * 10 ^ 70 + 6536638186184974219295460963753362918814032768917621294857793826715471

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_169 : Polynomial.coeff recurrence4Scalar0Main 169 = -((((20369729 * 10 ^ 70 + 2922098714622181893852965518650700969412824159859825080315325585377047) * 10 ^ 70 + 675130842525170722529125473805426945712557062393593797270521354965262) * 10 ^ 70 + 1245393721057202982130343731056197347134051079200024229527502883031682) * 10 ^ 70 + 4972604993672740956046639178881452502058084769864569383936678935111874)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_170 : Polynomial.coeff recurrence4Scalar0Main 170 = (((66071706 * 10 ^ 70 + 9647620620351341759831067420911257845276877952256808350238597973534377) * 10 ^ 70 + 8408324809250504318557732930001766837919646063316965608522371883517290) * 10 ^ 70 + 8445942033386519383331498759974315065392022729274812786929726666711050) * 10 ^ 70 + 3523427624671983815597768723504618766270406161092644635229127495521677