Recurrence 2 lookup certificate: Scalar4Exceptional 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.recurrence2Scalar4Exceptional_coeff_154 : Polynomial.coeff recurrence2Scalar4Exceptional 154 = -((85986381066617794067661218138949679754317 * 10 ^ 70 + 9396203310727968954084161990407158365244202799840508356158385584641216) * 10 ^ 70 + 6816674593699282530213848613499197865337863140542434337279288224001287)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_155 : Polynomial.coeff recurrence2Scalar4Exceptional 155 = -((255170302312965852153529641436416406205475 * 10 ^ 70 + 6436132626925310697500860865614752126435905262629630510703557419465679) * 10 ^ 70 + 6527359546981715870464053242017418846862550060266680676849714470753135)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_156 : Polynomial.coeff recurrence2Scalar4Exceptional 156 = (1972804204445397871121228897438768172989020 * 10 ^ 70 + 6831993740131988336664448980226517375954673089077850845121931424732430) * 10 ^ 70 + 7074047857148306098801360876490798145702499783697697466492796210248716

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_157 : Polynomial.coeff recurrence2Scalar4Exceptional 157 = -((6443739819325249009479929197581890321529650 * 10 ^ 70 + 5400307004228073634252615079848718170318420901730626752619197455656843) * 10 ^ 70 + 395039559511176043539540090493240542239274035723659092663907648372466)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_158 : Polynomial.coeff recurrence2Scalar4Exceptional 158 = (10665442072207740372667504944959334773907360 * 10 ^ 70 + 1675593395855392079068314314931465058983322179265347676094216307516637) * 10 ^ 70 + 8744026954806307458079168034468379548004904375687471166329250682231911

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_159 : Polynomial.coeff recurrence2Scalar4Exceptional 159 = (10423775844246201080245023851695556126575576 * 10 ^ 70 + 5506587483623592710936784441870916849248324905884869698359148800700103) * 10 ^ 70 + 4353331818521407373210476751443490250828233486436662434469234763000328

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_160 : Polynomial.coeff recurrence2Scalar4Exceptional 160 = -((140329802014146645260738585006039517455313168 * 10 ^ 70 + 854550290455641400207980337054673998401087260470817278491888058171681) * 10 ^ 70 + 9019933563595781601865728557799570766621603800017714836307218615924190)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_161 : Polynomial.coeff recurrence2Scalar4Exceptional 161 = (533329294029196531776458223839333827542368334 * 10 ^ 70 + 448196135740387396705586103935622224104319844152627128192425802813788) * 10 ^ 70 + 8178604523387638411805846949115024061070434025415896593486164663114100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_162 : Polynomial.coeff recurrence2Scalar4Exceptional 162 = -((1180228346775362550890514396768289673162386738 * 10 ^ 70 + 8805429705466259642060475564451405815154407552131469057869333401331755) * 10 ^ 70 + 2930234856389331307839012985705460551523406810637939880818417819805113)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_163 : Polynomial.coeff recurrence2Scalar4Exceptional 163 = (822623550651455030426625723126731094127264503 * 10 ^ 70 + 4767156142230889718529014704920367777248975371047614364209651042014993) * 10 ^ 70 + 9511256229374136888694442732439026019391537797960404746908033944559932

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_164 : Polynomial.coeff recurrence2Scalar4Exceptional 164 = (5869225364075503534190792545302316950968409324 * 10 ^ 70 + 8287469342365019378106574534147561615625729150082739550408760936569600) * 10 ^ 70 + 5613265499946837267681541478279424257197127379928886532882960101101864

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_165 : Polynomial.coeff recurrence2Scalar4Exceptional 165 = -((32223287246742199060244721574825744179098913795 * 10 ^ 70 + 6072302415185453928840939944730703670827721245333167298552584574792361) * 10 ^ 70 + 6326408450807755442424609281444948288128741619758418305930291422118959)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_166 : Polynomial.coeff recurrence2Scalar4Exceptional 166 = (95944977302624596095936366228304454508025448098 * 10 ^ 70 + 8485308041827850372185506154401688931311841010448194126122404184016786) * 10 ^ 70 + 4289379110470542141452432125981712362230673356638473611373996476053130

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_167 : Polynomial.coeff recurrence2Scalar4Exceptional 167 = -((176986633324742252919086529221615354849271458253 * 10 ^ 70 + 1229709952009717621472171292577904682680551253733010842479093126257968) * 10 ^ 70 + 8684014798373672701145305870832027308790271220723842297405006701687201)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_168 : Polynomial.coeff recurrence2Scalar4Exceptional 168 = (67781824404446650073061473343701415997263287779 * 10 ^ 70 + 5348984940040557320851138036028353849227879050036217179311309154504603) * 10 ^ 70 + 2969403553430445706071184544148631632180286395650589516409586194155357

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_169 : Polynomial.coeff recurrence2Scalar4Exceptional 169 = (967415903576188392568541329173906168837414264491 * 10 ^ 70 + 8206998975288990759308551455826135525527120069292952119339229354377607) * 10 ^ 70 + 289608250552468626285379826952186437123587534726974527787315075337798

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_170 : Polynomial.coeff recurrence2Scalar4Exceptional 170 = -((4636091135172811243700566340769049732291518570307 * 10 ^ 70 + 8671808890837422864077272137280341967685481395822118769008355733334380) * 10 ^ 70 + 5147990051994495552044946469204449672057926212361351307625244902937681)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_171 : Polynomial.coeff recurrence2Scalar4Exceptional 171 = (13327621581331507208860456045426666844442948752543 * 10 ^ 70 + 8117565474119455363835454222496559349418038494854882162443168143243576) * 10 ^ 70 + 6031390726410097877597448485663239914030620351595567287495721120308968

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_172 : Polynomial.coeff recurrence2Scalar4Exceptional 172 = -((26315463550847581510887747715675272782696523114100 * 10 ^ 70 + 2932067619743263763002747422724331199638171979929440834786863751862213) * 10 ^ 70 + 5771512098812693232658286887410483405689779196590028113393564689085773)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_173 : Polynomial.coeff recurrence2Scalar4Exceptional 173 = (26271053378675139741813765712104048436645159621372 * 10 ^ 70 + 1086914656514005326243863156760297547879747876638512328829668995861386) * 10 ^ 70 + 2431516694204645990889822962447644915012228289473626170074213881927090

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_174 : Polynomial.coeff recurrence2Scalar4Exceptional 174 = (52993042643384443339815287547750640540872659703821 * 10 ^ 70 + 6831662694241846657240937496051163040596379288891885978187680944653024) * 10 ^ 70 + 7589704049250867110266223855530483974010007883418614532538786513032616

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_175 : Polynomial.coeff recurrence2Scalar4Exceptional 175 = -((380658236317133240374308920648506876293053403384145 * 10 ^ 70 + 7066370172194082565886218672517039762975255180252794185188297575023792) * 10 ^ 70 + 9773878376616653241865632567066560219380949448142760957049367103493686)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_176 : Polynomial.coeff recurrence2Scalar4Exceptional 176 = (1272337247608290514512330380158236427538481022870104 * 10 ^ 70 + 4405039878698030863551657935108516641513833422780571253595704000175890) * 10 ^ 70 + 7389758390401034351005946995543647808806855471644453152219799333662641

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_177 : Polynomial.coeff recurrence2Scalar4Exceptional 177 = -((3087976792287017910715735680113839068819816116105915 * 10 ^ 70 + 2864084696275781918953416251168586013441314727598511239578753258577998) * 10 ^ 70 + 829121421483397806870351393516137257816063185434837307371800127341023)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_178 : Polynomial.coeff recurrence2Scalar4Exceptional 178 = (5638755302757109590208407294768122296959667611412547 * 10 ^ 70 + 8127939440208401443772658576129838900306528929322490936584304871960643) * 10 ^ 70 + 2608814010458154259455148025004836692889491090742935659243800150906039

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_179 : Polynomial.coeff recurrence2Scalar4Exceptional 179 = -((6439200600109193859684549751103219273221511465722382 * 10 ^ 70 + 7221249848600896116859564542132925509145301044068887415571100299565585) * 10 ^ 70 + 8401474673340042093362956913748540549038377997756952814411945867103779)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_180 : Polynomial.coeff recurrence2Scalar4Exceptional 180 = -((3134983780158132904132246308808802018608351516907808 * 10 ^ 70 + 1215620628344878728165227452026842148101487216368179190574052710240814) * 10 ^ 70 + 9906762716315243541573170557993010796730181864759249656725840080710262)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_181 : Polynomial.coeff recurrence2Scalar4Exceptional 181 = (44490893873643910136757643058460236040315349724252227 * 10 ^ 70 + 199392853761278062740045463587602078422437682456383501406300842172621) * 10 ^ 70 + 5797916953225812990902371822612881315441372646040620668853653889209535

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_182 : Polynomial.coeff recurrence2Scalar4Exceptional 182 = -((160302290547457073716271263587203885003612668231735181 * 10 ^ 70 + 2285881737820373478664532318990476143517566842316453399664869084794725) * 10 ^ 70 + 7562135478904570194278673129761318035536535802704405968935601972167232)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_183 : Polynomial.coeff recurrence2Scalar4Exceptional 183 = (419436908545940108994169647230963903889017515422257503 * 10 ^ 70 + 9452836989017059385600632804735763053325039289436955998912671079126095) * 10 ^ 70 + 459490581526355514323995451806686452225088984479507537598350906811803

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_184 : Polynomial.coeff recurrence2Scalar4Exceptional 184 = -((904619718442641015502486010220207856117081941059855899 * 10 ^ 70 + 3862231671270221480572249772370185086417967986373483729053475873730628) * 10 ^ 70 + 1697964999831342569339244990646628005486832386188752638089475373045451)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_185 : Polynomial.coeff recurrence2Scalar4Exceptional 185 = (1657538426772314546552058344947654565351053248538805491 * 10 ^ 70 + 5118624407651502122355279846053455699504321613674473115043549627490078) * 10 ^ 70 + 8628959666992551254054136627651209838067403885228672361977089482360511

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_186 : Polynomial.coeff recurrence2Scalar4Exceptional 186 = -((2545928850916364645576667655374810362422610269506444205 * 10 ^ 70 + 5572813218584460558404914257482124843606058957463684959743017616693807) * 10 ^ 70 + 8148115687748047266986879866420788222129343653697549864420410217105485)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_187 : Polynomial.coeff recurrence2Scalar4Exceptional 187 = (3019630020200597934902864576618449205500346927841178874 * 10 ^ 70 + 2623012392966442973589963194836230151030186544512307185012731177843317) * 10 ^ 70 + 336773762880902395008482676257600193991278443986993775330807443877733

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_188 : Polynomial.coeff recurrence2Scalar4Exceptional 188 = -((1755748997357214844825953459633493300807270622686699325 * 10 ^ 70 + 8127907022251238034923647213952457382823762132587464070438165092835962) * 10 ^ 70 + 8804457215448021172188100104620872816149375729148787781291023706975551)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_189 : Polynomial.coeff recurrence2Scalar4Exceptional 189 = -((3722957148216367642212113343166922117518645649672735849 * 10 ^ 70 + 8609151448386649380337895539224438771838265296825114170855623364286681) * 10 ^ 70 + 624116939345460084092011538020421749513689028452107022531342674681788)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_190 : Polynomial.coeff recurrence2Scalar4Exceptional 190 = (17228202257237863418348721356302342473375606954972622797 * 10 ^ 70 + 5947928711234764850355796984150883211726296864457056895843236379116745) * 10 ^ 70 + 8239981348112863209673324324489163003192527197480263262019561723201202

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_191 : Polynomial.coeff recurrence2Scalar4Exceptional 191 = -((43473731947050633954467877240868395746846283676331124885 * 10 ^ 70 + 6916304898241001871401222364342099334651076643943851962418271441822365) * 10 ^ 70 + 32319526193739442218615998505809242945119600252138483165569765309255)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_192 : Polynomial.coeff recurrence2Scalar4Exceptional 192 = (86471203383458519100515639100071236157164017440527233466 * 10 ^ 70 + 7843442469277415279320366428034216346972726551967578334406348421882128) * 10 ^ 70 + 2639919132831903853229269351976148704726975598253813668253452795826153

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_193 : Polynomial.coeff recurrence2Scalar4Exceptional 193 = -((146213377104431346208059574052496210859641601697825256209 * 10 ^ 70 + 952675553150699286179458919613352924447727244896966593704126725817109) * 10 ^ 70 + 7109249752800191996911708234582519759108756011904597752220480724817827)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_194 : Polynomial.coeff recurrence2Scalar4Exceptional 194 = (213450193407976211440764788271997522235199445703300759981 * 10 ^ 70 + 8807243316165643965594438735479174635298186157902938267101369425908329) * 10 ^ 70 + 1403049153873379601733457102562860361213089324034832215053069860584300

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_195 : Polynomial.coeff recurrence2Scalar4Exceptional 195 = -((263157442475245668424842185599223226086539254206104732561 * 10 ^ 70 + 1869053643901032661332080864930308399893513627053463712313704023831147) * 10 ^ 70 + 6131358405996028195307106847329313839358152970511510023823094906834676)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_196 : Polynomial.coeff recurrence2Scalar4Exceptional 196 = (248502760688686686559644708841705411616267296557704639064 * 10 ^ 70 + 9338373745107776563311758918417843599506756651376570873320798387967668) * 10 ^ 70 + 5528102323623117849233082567177259023500520219134101819861639081940407

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_197 : Polynomial.coeff recurrence2Scalar4Exceptional 197 = -((98428073365564011824826114433678571532858849328848510198 * 10 ^ 70 + 7517294409736294849729047511526874796010604075947989126845031218880589) * 10 ^ 70 + 7794427776552535405169418787146344303495878316619654488267396289435348)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_198 : Polynomial.coeff recurrence2Scalar4Exceptional 198 = -((277207448911769398955874057330574243623669352599282221616 * 10 ^ 70 + 573652598271285055896675084896474067601980826718143888697965971272890) * 10 ^ 70 + 974155108259652576309782615080153764118894457958506081020197970677461)