Recurrence 2 lookup certificate: Scalar1Main 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.recurrence2Scalar1Main_coeff_195 : Polynomial.coeff recurrence2Scalar1Main 195 = (412645496293888699171064079314228157050111379446970066096457072 * 10 ^ 70 + 8480008591313949157066663556641401144718985506954254157007018022601394) * 10 ^ 70 + 4267406067494721858270824485297196333386653251092596264847651574428946

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_196 : Polynomial.coeff recurrence2Scalar1Main 196 = -((352291647584392994161201735479366129156545422034131959886946959 * 10 ^ 70 + 8877088682623850811712063955740580666530682707625101494329309913555265) * 10 ^ 70 + 9367311442159688177674113225673360465177935695442157767216746496910135)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_197 : Polynomial.coeff recurrence2Scalar1Main 197 = -((1235495839541026873859491390491464559317489154791864661779571736 * 10 ^ 70 + 5914308030505865774311795898212906138228262062803076029688505004081851) * 10 ^ 70 + 326220445728312709579165149382538443864782558891883558690547432163789)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_198 : Polynomial.coeff recurrence2Scalar1Main 198 = (6980233606135199643528056068897943017052630599586923836743743937 * 10 ^ 70 + 2156335904611049987858720904508236032654850084267000704350387840720245) * 10 ^ 70 + 8236736921342051823693357594304329526914638273992147757513415734883694

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_199 : Polynomial.coeff recurrence2Scalar1Main 199 = -((19597068102068607155645316494256254721417454807874455082163650105 * 10 ^ 70 + 303704847485928157814262682476969674037049962788821680906108468669917) * 10 ^ 70 + 808054298725058701077206950942610965351470130650341781526716308383203)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_200 : Polynomial.coeff recurrence2Scalar1Main 200 = (34457678637971689932419582195658117334108361084489203530740886180 * 10 ^ 70 + 6156436935618790458059979527954996184784096103617090809356415369630205) * 10 ^ 70 + 909014125520685637613082328493157738991552359325638372613600331742129

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_201 : Polynomial.coeff recurrence2Scalar1Main 201 = -((19092072046893101928308097897961861944408226060890920361659338482 * 10 ^ 70 + 3451045366114291817265309299006206603616145412723844260546071066512114) * 10 ^ 70 + 4076634264567409066119807288861938270802294681325987269077277906590087)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_202 : Polynomial.coeff recurrence2Scalar1Main 202 = -((123634760017121994258548069885800418082026883665582503325171388206 * 10 ^ 70 + 7284129718744735490776635312403285895556404542920150774962365517235784) * 10 ^ 70 + 3505513616945979180381659307111355516843820886781482020370438567067957)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_203 : Polynomial.coeff recurrence2Scalar1Main 203 = (586799587985841740430295681785035052643683948818067976227308214851 * 10 ^ 70 + 5582276632302031170588000288979602542116022862964362478782784265044231) * 10 ^ 70 + 1596892341854615994039655522916987204146865497764941445219423852456736

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_204 : Polynomial.coeff recurrence2Scalar1Main 204 = -((1592032179392165290587256440133199242567332647529518064738689971579 * 10 ^ 70 + 539890895666167660318478575592444881211244712973809529619259454301400) * 10 ^ 70 + 8951325125148779618073369389996528675743335943753920729266153075692746)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_205 : Polynomial.coeff recurrence2Scalar1Main 205 = (2993379611455368361859822788624519116626410743612267893572816403691 * 10 ^ 70 + 2869488049333552815475308366782187615924349778486944607059605580987520) * 10 ^ 70 + 7904053570265466044357416892298242688471155162069294383680601195186393

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_206 : Polynomial.coeff recurrence2Scalar1Main 206 = -((3153430352361727679235849747456110583433439022455882172528055573694 * 10 ^ 70 + 7624397987224783463609325970765170550052164563551373325298449085682782) * 10 ^ 70 + 7987457321344848109714399781111046966421179285602100198295929884541274)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_207 : Polynomial.coeff recurrence2Scalar1Main 207 = -((3321422515512505423663068704403367001883630869037060760241548579641 * 10 ^ 70 + 2770626323817987429989381257970318042920093665881895054232022719530069) * 10 ^ 70 + 7477629944215181121050140755947112357893452284865560230130893708590465)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_208 : Polynomial.coeff recurrence2Scalar1Main 208 = (28776031131713211046211456759592857857683832763855903638835065636387 * 10 ^ 70 + 5409517958336141860696473625800724722017928778067824106859819485030005) * 10 ^ 70 + 4063268282939476140121776224743098358706716752900689693520363629475815

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_209 : Polynomial.coeff recurrence2Scalar1Main 209 = -((94267270901318899610835942642301734142864198292519309569087312560987 * 10 ^ 70 + 3447188549030444424069741264560419434339659315523893590644174937092419) * 10 ^ 70 + 3672837870949367282284934764028311104925922166894191134128433581632189)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_210 : Polynomial.coeff recurrence2Scalar1Main 210 = (222637180527994681587190668029343983763226926998952500976757942618943 * 10 ^ 70 + 1476937314127117537832940488285302595683324473488105739364148700129095) * 10 ^ 70 + 4050304650813031850455058096666698330625753450862178629714816869154181

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_211 : Polynomial.coeff recurrence2Scalar1Main 211 = -((407100185168065928236563046452389852866490092787886287345670213467780 * 10 ^ 70 + 9478512329762640761992442859329659488007062927264065763164700269571073) * 10 ^ 70 + 7643700709008724232564361400843439941201580904746865037768098485860329)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_212 : Polynomial.coeff recurrence2Scalar1Main 212 = (528078252195714816471344691003330253356288978330429667435538175644407 * 10 ^ 70 + 4953887390845987209717218462036305838520133399249556334518288124720497) * 10 ^ 70 + 6586532711640458118180045842135802017147644681929260626907669822426445

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_213 : Polynomial.coeff recurrence2Scalar1Main 213 = -((181166222123597029740641560782580511190094779143520223666701500624643 * 10 ^ 70 + 2524220255764504539020101553780200598511885339059845607546721308616427) * 10 ^ 70 + 8587907572730981742672644137085569583372254983822266402016146980344475)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_214 : Polynomial.coeff recurrence2Scalar1Main 214 = -((1618516322792476896773901049503801310168195587660676019709435842949419 * 10 ^ 70 + 831608651720236719677776703397106420731118226402268889150876545531948) * 10 ^ 70 + 8203332561399510793356975135123396803175395417274546985303297244101486)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_215 : Polynomial.coeff recurrence2Scalar1Main 215 = (6858330933875202306519299223694481102390861961402932520076146401432044 * 10 ^ 70 + 6588522776688872481940181329553973145969424339924714650003669182084987) * 10 ^ 70 + 9096549070345969904058367321217948493854863993207197502663015066246083

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_216 : Polynomial.coeff recurrence2Scalar1Main 216 = -(((1 * 10 ^ 70 + 8996759389885912229599450269956226308308631811532694065001761550562588) * 10 ^ 70 + 8650769520523524740611147444315929248605605499220173903624759618661780) * 10 ^ 70 + 877339874847300201220533353023016735507699862863839040095817396849453)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_217 : Polynomial.coeff recurrence2Scalar1Main 217 = ((4 * 10 ^ 70 + 3251539883790307213667779079343593147471670792442157425722374092550303) * 10 ^ 70 + 5626415322855040298479011591583759882267608636471980603107675821736234) * 10 ^ 70 + 8003488779608812002230033699757309960031538987161567217367064813887249

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_218 : Polynomial.coeff recurrence2Scalar1Main 218 = -(((8 * 10 ^ 70 + 6276325414366965722571654072813453365422766967386149902056427809298374) * 10 ^ 70 + 7783700368282825922185337232857029127584691443709310640494394854818563) * 10 ^ 70 + 3170403119424809943935190871009152711336219554016942962995901055605795)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_219 : Polynomial.coeff recurrence2Scalar1Main 219 = ((15 * 10 ^ 70 + 4585428244743827628583106701798993644836562368696596979779247669325571) * 10 ^ 70 + 7392861378990737569219774013934270291487418508953398701598569913646425) * 10 ^ 70 + 2604619237214130859179620772619134480248368512207584856327095378269670

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_220 : Polynomial.coeff recurrence2Scalar1Main 220 = -(((25 * 10 ^ 70 + 976259729552279913458568303528210405323802221589666655878309395015412) * 10 ^ 70 + 5469492902544638257825551170373456204959727593210566555678315910906985) * 10 ^ 70 + 1257532986419433231624774398958818676930718885436708250445121327169647)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_221 : Polynomial.coeff recurrence2Scalar1Main 221 = ((36 * 10 ^ 70 + 8338657384600994829466724155016610262145756685488116976153854218489894) * 10 ^ 70 + 4320692645631063706188778350595646506816103120743759987606983107805485) * 10 ^ 70 + 3874560841677717715248328636655684691376583764800452673152486627480099

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_222 : Polynomial.coeff recurrence2Scalar1Main 222 = -(((48 * 10 ^ 70 + 780917347272623406891882903554143135339559547000888019396677529983627) * 10 ^ 70 + 1396267200764560809637557136122947928108453510778810200684690634237135) * 10 ^ 70 + 2316317265826697373708841157016325051579804406024003555685572647191536)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_223 : Polynomial.coeff recurrence2Scalar1Main 223 = ((53 * 10 ^ 70 + 3018172311160924104274317624935278860733878980774527798141260773281655) * 10 ^ 70 + 1764084759110118943978727774835032845041336095714053808724257127000954) * 10 ^ 70 + 6554581505948743328433910630489657097759806239220846639829010146449208

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_224 : Polynomial.coeff recurrence2Scalar1Main 224 = -(((43 * 10 ^ 70 + 361270464652415241149404501694104320563154529378215911557222249166336) * 10 ^ 70 + 461562906957102812532386060943515303299427778262750947410969532743193) * 10 ^ 70 + 6942213265982444091195879290571347323942337430905888043660692227285160)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_225 : Polynomial.coeff recurrence2Scalar1Main 225 = ((3 * 10 ^ 70 + 3072353631615462930331368487471974555147048653830315047223273705551794) * 10 ^ 70 + 7206818089723514352863041615898078394483271029707503373017212838012239) * 10 ^ 70 + 9193040353627386541240178383358201349312618584933990134450327323142192

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_226 : Polynomial.coeff recurrence2Scalar1Main 226 = ((84 * 10 ^ 70 + 257390087905342719844770293941242679579581122847733486012217273151039) * 10 ^ 70 + 6736795346513580275958821684750561420767915964259735476349445459783830) * 10 ^ 70 + 7696856991885511768151192315279736055848298719681660356254148909067228

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_227 : Polynomial.coeff recurrence2Scalar1Main 227 = -(((239 * 10 ^ 70 + 5977744778695279865405524581373651818382916525237047721833009120855095) * 10 ^ 70 + 2170219986545314249481517047885244016390827769868226716985454796496766) * 10 ^ 70 + 6354942455124484178850434919450695620659939413651713365589033535878199)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_228 : Polynomial.coeff recurrence2Scalar1Main 228 = ((483 * 10 ^ 70 + 3031979405898075157791891223244305359721713829583295701001729511972507) * 10 ^ 70 + 6069865157147855497883956142922486564456574595710961427514826088585612) * 10 ^ 70 + 4431322656276395300164700127286047799925343811412740543314471595786246

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_229 : Polynomial.coeff recurrence2Scalar1Main 229 = -(((829 * 10 ^ 70 + 6595337086387056851058053599683650021749008463732077293475977253171831) * 10 ^ 70 + 3824600843762811612724134795372940543747942374695603190910607650705493) * 10 ^ 70 + 6360054794186721308298492990998221031961480836754817904296549170532590)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_230 : Polynomial.coeff recurrence2Scalar1Main 230 = ((1282 * 10 ^ 70 + 4341672815820912171872857424842302578619068161449149253864110385142464) * 10 ^ 70 + 3736210345187895443234007679822742115134708793769274240756987794429836) * 10 ^ 70 + 1472863046149323175551681990029578979034871539135913898053036230934065

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_231 : Polynomial.coeff recurrence2Scalar1Main 231 = -(((1829 * 10 ^ 70 + 6833086370342075237084479000343920656017088797920936700748844660287278) * 10 ^ 70 + 6097211672280311118618984177544643173945154364888192031180597966354163) * 10 ^ 70 + 4752142676953896282593322828581396999916524263861180424734883093696803)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_232 : Polynomial.coeff recurrence2Scalar1Main 232 = ((2440 * 10 ^ 70 + 6404195417811885287523562130965247187153091512682589972111119885448072) * 10 ^ 70 + 8073436129085885405907242249155482435262034675780470733833106291892331) * 10 ^ 70 + 9492491205750292644735464852484271343847286386675726818799272311078901

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_233 : Polynomial.coeff recurrence2Scalar1Main 233 = -(((3065 * 10 ^ 70 + 8167101879986834998305243149704569943811437122199497521662321553391711) * 10 ^ 70 + 4374977798092868317984829257224832631530477612874177845959407630023586) * 10 ^ 70 + 7719157549565329454516225942597257467699803488604657923096787448026777)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_234 : Polynomial.coeff recurrence2Scalar1Main 234 = ((3641 * 10 ^ 70 + 1590124141371229042657258950066280853577840209498475565439355878163277) * 10 ^ 70 + 4973105433094246749726423011822273529468643290291364906524724688044419) * 10 ^ 70 + 8640922430853500488385399789856413435714008778745571682418072634818589