Recurrence 2 lookup certificate: Scalar2Main 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.recurrence2Scalar2Main_coeff_234 : Polynomial.coeff recurrence2Scalar2Main 234 = ((848 * 10 ^ 70 + 4773022010588484361559476895642063200877512033482454834624789450660243) * 10 ^ 70 + 3980610027480138363451804852857734898309822869658120302479649914689957) * 10 ^ 70 + 6137770620972292062223135122771781416215814778309433411076376817788609

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_235 : Polynomial.coeff recurrence2Scalar2Main 235 = -(((894 * 10 ^ 70 + 2932955438479461812464416941644358325955887551194791927392205296605121) * 10 ^ 70 + 5891901176252168735344978921865112348331109266796143469638070397389891) * 10 ^ 70 + 8909162685734654876766258538957881372188839571217572477269133638296718)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_236 : Polynomial.coeff recurrence2Scalar2Main 236 = ((890 * 10 ^ 70 + 8116685136837117251996888341398661737392320267414691550946834444810835) * 10 ^ 70 + 8519298357711285373346802622894035795414091830908973262193715471434005) * 10 ^ 70 + 9131472691343777705050546924765223060315783302905269847733257045137863

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_237 : Polynomial.coeff recurrence2Scalar2Main 237 = -(((834 * 10 ^ 70 + 7194662067245812222183029049792595035711781949488364125203113763714950) * 10 ^ 70 + 795588648328009477155071646348216022247247218859863377722258873549890) * 10 ^ 70 + 7525161790988804380106319176294977902089550532581351317964596485493089)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_238 : Polynomial.coeff recurrence2Scalar2Main 238 = ((729 * 10 ^ 70 + 3475843244422149673789268150053972175009372419241239136374576663887111) * 10 ^ 70 + 5844888944886418665208591101163904085342861265374867098319956842786231) * 10 ^ 70 + 856844074012681994156903109581811135780259022324470609115782020622517

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_239 : Polynomial.coeff recurrence2Scalar2Main 239 = -(((584 * 10 ^ 70 + 3914273660069439537426689419887680819866862335891101403063325916091813) * 10 ^ 70 + 6773811847236645624867626189187935241442531486212293562748669809631063) * 10 ^ 70 + 3350756797902992801518438215549406380725205935658640718766283901098559)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_240 : Polynomial.coeff recurrence2Scalar2Main 240 = ((414 * 10 ^ 70 + 4466359732632024816433149848921705441430949007230152176225432239456291) * 10 ^ 70 + 1491000863762169820104196352792419273365765420366843141213931468215169) * 10 ^ 70 + 52267393963592573221164605117450650780702648118502398746315457621190

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_241 : Polynomial.coeff recurrence2Scalar2Main 241 = -(((236 * 10 ^ 70 + 6647527704116497269545244914497817093910680147900631031849901826534382) * 10 ^ 70 + 224475802388351267858388255825612907215249508586833329202986965346452) * 10 ^ 70 + 5362073643722140448828723572795411509647045770553863057143649117907273)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_242 : Polynomial.coeff recurrence2Scalar2Main 242 = ((68 * 10 ^ 70 + 356961850168833889317117942407003855116672244251021866066524961333903) * 10 ^ 70 + 5764884070327361586034390654081852493121577271220067182346961415654884) * 10 ^ 70 + 9848928825617028177462179390500136902958205364231190986560300270306380

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_243 : Polynomial.coeff recurrence2Scalar2Main 243 = ((77 * 10 ^ 70 + 1300256438069547055988155747018988191530164668649454564082067644474642) * 10 ^ 70 + 5996394179637184653215803747320440016775255851756340774495508212708632) * 10 ^ 70 + 3656130478926561303310007669517068876573656437162454608560006343359756

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_244 : Polynomial.coeff recurrence2Scalar2Main 244 = -(((189 * 10 ^ 70 + 288684067300502468095233406349625666704990916449820900694090291354857) * 10 ^ 70 + 9467720573478691315232211276580798454695739887098855699424321159576802) * 10 ^ 70 + 6335863050830441549085216115313735958246858279825245198344006951608574)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_245 : Polynomial.coeff recurrence2Scalar2Main 245 = ((263 * 10 ^ 70 + 2094085682021266442490213830312427364849037740734172524688534622581768) * 10 ^ 70 + 8910981164756711996821314076435873999241591315291938161284126668193247) * 10 ^ 70 + 2312657359691958848132588166883287877195520696296249580144930437556515

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_246 : Polynomial.coeff recurrence2Scalar2Main 246 = -(((300 * 10 ^ 70 + 3929382145567216321715023357791996940091491964151079626851916368439638) * 10 ^ 70 + 7368815885301956177167712095134783100388320898059550023763861884537079) * 10 ^ 70 + 4621414459091651476817667414010911137341719951433943816194822993990822)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_247 : Polynomial.coeff recurrence2Scalar2Main 247 = ((305 * 10 ^ 70 + 4563483203422858080376142991085755926170603836025319717850830306317971) * 10 ^ 70 + 2410070757553127966947001605037918248762404463034645460386546386829852) * 10 ^ 70 + 1478130197603326101506764219916030403962585062099199896997233843032979

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_248 : Polynomial.coeff recurrence2Scalar2Main 248 = -(((285 * 10 ^ 70 + 9146706222285465357169021296870294815833130050896016945532925864244436) * 10 ^ 70 + 4998800810235124678102504285009115451923872773069828776547375686938654) * 10 ^ 70 + 5436065484026581731765102975451396608383606969443254442929625979521851)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_249 : Polynomial.coeff recurrence2Scalar2Main 249 = ((250 * 10 ^ 70 + 2858967922786557901508222906718293878769413793475702736337207239196918) * 10 ^ 70 + 9617549653840754163224671855972175034678294761758220381733941958938874) * 10 ^ 70 + 4960361592310852951747198963359776256473043723985991728762777274179206

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_250 : Polynomial.coeff recurrence2Scalar2Main 250 = -(((206 * 10 ^ 70 + 6679114521589218728541989833635381295787684887047766650855184523942814) * 10 ^ 70 + 2967232482121728893792825753803329916769803218960135031320614547076973) * 10 ^ 70 + 6324769543020167046239866264500983127283975208252706140479428532227822)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_251 : Polynomial.coeff recurrence2Scalar2Main 251 = ((161 * 10 ^ 70 + 7395836996666963040279712827333696745016066001047208635388180357077331) * 10 ^ 70 + 6001737385750607520002633325470584237860068877228386264554186550761286) * 10 ^ 70 + 3087677975575601145227256735930743819151432872582302993019776553642492

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_252 : Polynomial.coeff recurrence2Scalar2Main 252 = -(((120 * 10 ^ 70 + 2591652292001421673738072577643782811848705216780326481731857229876621) * 10 ^ 70 + 2405385727024528884357839302174865905342915961665769437345738635025552) * 10 ^ 70 + 2491562731376198099159444450977287559309643465126098478454254913436501)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_253 : Polynomial.coeff recurrence2Scalar2Main 253 = ((85 * 10 ^ 70 + 127023231615946489245279924690636287897233007413913961667304755972412) * 10 ^ 70 + 9962130694019225641126605175024242474405452350644422374946924140269906) * 10 ^ 70 + 4176669469458155470530538846170892465703735992372860569033077985470691

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_254 : Polynomial.coeff recurrence2Scalar2Main 254 = -(((57 * 10 ^ 70 + 879794791221167274606581453306909897605774402799889758887801726938193) * 10 ^ 70 + 3823146955875583318854077907158479816911615996268960681541629749094179) * 10 ^ 70 + 483801769374272475503905594523172838326578568317065064384985316201519)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_255 : Polynomial.coeff recurrence2Scalar2Main 255 = ((36 * 10 ^ 70 + 3222901045619399152942558960779553518710294591602988345887064673901025) * 10 ^ 70 + 4393558224828399448725655938825051012390405963857232024153930121588244) * 10 ^ 70 + 5927457096775028700065909001003078718619298661700412005678731602115455

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_256 : Polynomial.coeff recurrence2Scalar2Main 256 = -(((21 * 10 ^ 70 + 7867773783207851916404120753413699682475284844958014946146336425585402) * 10 ^ 70 + 8531314619872103957008780490748765292250515052737650825404506840902368) * 10 ^ 70 + 8369430597449957584771575803990620327735877686812992907572986461774171)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_257 : Polynomial.coeff recurrence2Scalar2Main 257 = ((12 * 10 ^ 70 + 2096205803568329953697892443848493373835885339929706714105715702953607) * 10 ^ 70 + 2624642156054541932532830553545044324916257341505296533874589961023513) * 10 ^ 70 + 8893373123157238943240613618741079229665314267646792673412448721585380

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_258 : Polynomial.coeff recurrence2Scalar2Main 258 = -(((6 * 10 ^ 70 + 2872647485238986320891745094718418953397646675571830127836095278133123) * 10 ^ 70 + 2240471610313851477718559988256696620053537236698405085771672263780682) * 10 ^ 70 + 5030195613165256864359247051648458968869772312362802789857843475756799)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_259 : Polynomial.coeff recurrence2Scalar2Main 259 = ((2 * 10 ^ 70 + 8736302384307627288257414308132597781962637818298911013553896791968848) * 10 ^ 70 + 6823502181203169473885041636490438132946160229315585343840522921246811) * 10 ^ 70 + 5871411405118630366229882890489226820042383277699173519956911290502837

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_260 : Polynomial.coeff recurrence2Scalar2Main 260 = -(((1 * 10 ^ 70 + 646149688787783331975300807417545314082030208935338744643879929994253) * 10 ^ 70 + 4832193618793649741880250342872093626234301500384585570696529569332602) * 10 ^ 70 + 1826577650916793352059252511172940838187405225168034030113052158343884)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_261 : Polynomial.coeff recurrence2Scalar2Main 261 = (2080563506824725241279737762665012152538943823498590024926830996281602 * 10 ^ 70 + 8701908041395747777373901145771469368191696170374536750607708828108550) * 10 ^ 70 + 1317077833761304533357965733385843829309714195523523850425329769477025

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_262 : Polynomial.coeff recurrence2Scalar2Main 262 = (1294545298286251269389786403081612955646276306144438471035355771070962 * 10 ^ 70 + 1255041262909768289599333262438138932910960500345576762485557666641034) * 10 ^ 70 + 9679413211387105644215447560932961063733461302309649038614228701763855

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_263 : Polynomial.coeff recurrence2Scalar2Main 263 = -((2133366282293718258325792650176873461204886366211041561153585922538699 * 10 ^ 70 + 7159774227604857779867905087686548594866847546120484546515274099152739) * 10 ^ 70 + 9488326844961246503161880955019488043676607066395647868071422532466852)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_264 : Polynomial.coeff recurrence2Scalar2Main 264 = (1922917882948710830475626444645933199810607125939671741879464617341951 * 10 ^ 70 + 4099506234891871073730418836685904748882042364401154783497966253201648) * 10 ^ 70 + 7866636222009772999292039498747569648636070758396003740936264713235586

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_265 : Polynomial.coeff recurrence2Scalar2Main 265 = -((1410893631477453530744671499804053434269907252046802732932457513946303 * 10 ^ 70 + 4589939956891086536202738999971999341401769635758971655945527282861520) * 10 ^ 70 + 8079233373521984523233395799398182464365226451878558495796733889072327)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_266 : Polynomial.coeff recurrence2Scalar2Main 266 = (919099552570439442252615216400915663921385651284079722486771761213615 * 10 ^ 70 + 2800597582331910170531754966426790189009078357422131020726643009210528) * 10 ^ 70 + 3284258665844795851959160237135743418504439825169359596454442002807002