Recurrence 4 lookup certificate: Scalar2Left 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.recurrence4Scalar2Left_coeff_115 : Polynomial.coeff recurrence4Scalar2Left 115 = -(((6525666137052408126127308018995720884906 * 10 ^ 70 + 6187024663540072376156372598443618760723723822888130972768169983346784) * 10 ^ 70 + 7409048821422252964963290724671562459317485230470899389334791440098584) * 10 ^ 70 + 8618954322899926220423875957336662889349433350054950431932294784458014)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_116 : Polynomial.coeff recurrence4Scalar2Left 116 = ((55058837878026253142260661871692314719148 * 10 ^ 70 + 8334847107744163188401381812042036088238628586977692924063703186374428) * 10 ^ 70 + 2938249130228115408617989287565799529575131818870401994822777911524911) * 10 ^ 70 + 7150417450921501324100441673409235411602363805627349520596579524138149

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_117 : Polynomial.coeff recurrence4Scalar2Left 117 = -(((453876010942975563580873097492948469918266 * 10 ^ 70 + 4701372184796775606869179676183653843387234091938218333551410076617545) * 10 ^ 70 + 2819158424291402325262104181512318021629961184844004396123863380974838) * 10 ^ 70 + 4201261817746502517794795954732953337918856247839805389154271811321154)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_118 : Polynomial.coeff recurrence4Scalar2Left 118 = ((3656766724298442209581969079366870000016496 * 10 ^ 70 + 4397807905690812443647720860218302497104749875307707121745280726133138) * 10 ^ 70 + 158137516888351920882188895453548029878812756993663962191484146059971) * 10 ^ 70 + 5518764690709890373644844804581374857326472182091072017948320997944129

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_119 : Polynomial.coeff recurrence4Scalar2Left 119 = -(((28803278995240404602910037055054632854525975 * 10 ^ 70 + 4545945021492460912324903249320445456549366382036340228892645311476098) * 10 ^ 70 + 7782547248174279029635453740047758231502967689735304401513166349925037) * 10 ^ 70 + 8661085773661663975271318505020375414526040201507779935111226171876948)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_120 : Polynomial.coeff recurrence4Scalar2Left 120 = ((221870572614778586513638539338155278848153790 * 10 ^ 70 + 8424457860553692145420631451049551283767127662786788229207644084413851) * 10 ^ 70 + 5942584233890615918625634313890644380809761256115058410496352136773475) * 10 ^ 70 + 9763305728168675270143633678482233161614911576714300820329863442310705

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_121 : Polynomial.coeff recurrence4Scalar2Left 121 = -(((1671834343679970261256493954289627866036023324 * 10 ^ 70 + 1065490454940813989446492772792064728856515244222898962840868025230900) * 10 ^ 70 + 6539188337869466846719679437377693994260143320672930741882820853450678) * 10 ^ 70 + 9440797354145601729160277662513839631565524317705134531954474353284702)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_122 : Polynomial.coeff recurrence4Scalar2Left 122 = ((12326504098329417682850593809218949630657578148 * 10 ^ 70 + 268247508488492355218657731216110189260519721666199395278418661302628) * 10 ^ 70 + 4967652960287127692837107209947961064878042552840986849354896803899174) * 10 ^ 70 + 7312172725318837412895240772081894644851825715465131970469916438560944

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_123 : Polynomial.coeff recurrence4Scalar2Left 123 = -(((88951293909064327163032148370731656522909688377 * 10 ^ 70 + 8404237500187103381485714631377423904706538029667265372458279234345379) * 10 ^ 70 + 1547156985976740969690688405623725982783106463221397337811169087561423) * 10 ^ 70 + 2494537582381241123712072821317716069432294220477582452129348900785268)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_124 : Polynomial.coeff recurrence4Scalar2Left 124 = ((628403092983484682254371547551953660923277013780 * 10 ^ 70 + 2706357813063086286196624419110645929839463383268941010715517324693312) * 10 ^ 70 + 3725990250673567413728990425046712746246702168498365827962673833082253) * 10 ^ 70 + 4821227949436306899435234596872358261667359568946097403205883104318567

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_125 : Polynomial.coeff recurrence4Scalar2Left 125 = -(((4347123071337845784876156454507887046447329432981 * 10 ^ 70 + 3415178246291737131013333708415480225791067621874561635601892916031192) * 10 ^ 70 + 7668836033930505121769678621146386497133741831524211639063928069672597) * 10 ^ 70 + 3291503937883300310336931390060961959054661241615186600489269478071517)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_126 : Polynomial.coeff recurrence4Scalar2Left 126 = ((29453922929225772487429272185663753291800475665206 * 10 ^ 70 + 2422936207720011561141402447557914584402648652700128926492282017712471) * 10 ^ 70 + 8954312924198021545865865303215734138500927426598095961530364238162498) * 10 ^ 70 + 6214723135062234668497714285586333403131669915508133533879522266968400

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_127 : Polynomial.coeff recurrence4Scalar2Left 127 = -(((195505213916148224841812805806134320542431769755253 * 10 ^ 70 + 1420103629242591062499963721090631701059716263603512994668954878250143) * 10 ^ 70 + 7407138952770407990012668724921661996847509703853530803901956254874938) * 10 ^ 70 + 2597093894545797551783020746793420885051602390402659661937960977868965)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_128 : Polynomial.coeff recurrence4Scalar2Left 128 = ((1271570790616742627591388851591898987023587556917238 * 10 ^ 70 + 2391655962115774704619074960945296261103392774722839408667795651322992) * 10 ^ 70 + 6328009662662639681300157970056510419780965634550175369928269630648510) * 10 ^ 70 + 5827023014769923559340821837537074110612206872560939578714233633486685

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_129 : Polynomial.coeff recurrence4Scalar2Left 129 = -(((8105495595149272215030722571533973852170745751159998 * 10 ^ 70 + 6214265492337170526663008658291453084855730317805001297177146688691484) * 10 ^ 70 + 3480485008519321559476954631009203463053472898171752954799054220151726) * 10 ^ 70 + 1802586817754539742009283832101517747823763301213720753730410693452308)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_130 : Polynomial.coeff recurrence4Scalar2Left 130 = ((50647996036585034028720771610512680399990360741385785 * 10 ^ 70 + 4327780533053345389773319970042925494421377977001306389380734452291148) * 10 ^ 70 + 3469987281665436237260177281588355421039276898165864966166451176395127) * 10 ^ 70 + 7811231883955499531407197315353374368203225528322618401661019749248744

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_131 : Polynomial.coeff recurrence4Scalar2Left 131 = -(((310293452747257386911753290985690108950340838343046060 * 10 ^ 70 + 2591611217051534986127727517107655978713707430785508308374737167862838) * 10 ^ 70 + 1721304754878967633670505973070025656353733219362124097401686675858343) * 10 ^ 70 + 5480878710655915228206308230044891120922442628658579006441851407997096)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_132 : Polynomial.coeff recurrence4Scalar2Left 132 = ((1864197458553413718077863295982934798829493504199008093 * 10 ^ 70 + 9394216485825542527457296672081996579726249357381857215574113002193961) * 10 ^ 70 + 9098341133510782104789885360181898859817339838600465420466310686614418) * 10 ^ 70 + 1338323955472319339843473447156223065615765418887249835379894598117683

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_133 : Polynomial.coeff recurrence4Scalar2Left 133 = -(((10984970869248636197132467490816651298997522538675762169 * 10 ^ 70 + 2462428129336112938020374874071105108229725587007057119966144721760028) * 10 ^ 70 + 2344379996829785072648597086207272454116375032035104550376697260746558) * 10 ^ 70 + 4462826493242827082170326895268332262794704855715341692885390774225146)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_134 : Polynomial.coeff recurrence4Scalar2Left 134 = ((63499442886525793161255382581175561174724684634545118370 * 10 ^ 70 + 7550552099447466375269168941415452248783141946921465342619537540918262) * 10 ^ 70 + 3448535129963064043366767307361558835214164615791261944519362861149988) * 10 ^ 70 + 942428988769774357101423329788610226657494438516086262280908281072118

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_135 : Polynomial.coeff recurrence4Scalar2Left 135 = -(((360146262999992154919228008743210327334800628400892566705 * 10 ^ 70 + 4349512382423762377486088804713867000247973564881241969305741589511242) * 10 ^ 70 + 8964921072441833562729458970348690976650076470639412913245892252286894) * 10 ^ 70 + 576363075028705250611007618460318689650625849977467235136570908204519)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_136 : Polynomial.coeff recurrence4Scalar2Left 136 = ((2004461250266106584165694408939022962318985530009680293382 * 10 ^ 70 + 5020099245270384404183481535886649546909734183229538655472067932195275) * 10 ^ 70 + 9735886215258277550465393265579461077955963201160561977804649908477801) * 10 ^ 70 + 2800727049383866795125941474463474381346759303476618084902894292115649

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_137 : Polynomial.coeff recurrence4Scalar2Left 137 = -(((10949538244710898340572172157339724417846474551364661145773 * 10 ^ 70 + 4150111786394570550238066547388002406361668189435870544454330024934842) * 10 ^ 70 + 2734328195345086215010335847561051718152180813160224633478704242487548) * 10 ^ 70 + 5751841076692334652896587664599400826201059811274217447266866202595954)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_138 : Polynomial.coeff recurrence4Scalar2Left 138 = ((58713899114764092086743030057272683040541959025148822208719 * 10 ^ 70 + 1144011214894347599071314688174917333825156171552906987173306270385118) * 10 ^ 70 + 8182962520821835275258123051992173888883671600186876703975411627955327) * 10 ^ 70 + 621825760655490995855213598064899742335685690971252983775202393081456

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_139 : Polynomial.coeff recurrence4Scalar2Left 139 = -(((309099742912173212677485921258090605568710695772301723498049 * 10 ^ 70 + 8439125231571453259012190027390080824036633260446621880399664848086026) * 10 ^ 70 + 2009914511054808379583379011626174363731761209725412369500525156448893) * 10 ^ 70 + 7471123351057784924387525600182985962604828537366582185441898217893650)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_140 : Polynomial.coeff recurrence4Scalar2Left 140 = ((1597837856690706888616170903675982113948948657961564544613762 * 10 ^ 70 + 1463539545488251061800526943516164266041055428810302607849348526070660) * 10 ^ 70 + 8596298725482403911532648221534699485964774547843758875017614086077124) * 10 ^ 70 + 9315392330554443830274267541409238665393448035589502513085206776637646

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_141 : Polynomial.coeff recurrence4Scalar2Left 141 = -(((8111571972494959119131233371355446950617528548001648349065006 * 10 ^ 70 + 5338397561079001436798898392679871418458896700394180470617197679986994) * 10 ^ 70 + 9917405817054801497429880237453548962794440888093247382254738720996897) * 10 ^ 70 + 8114350587439404126325915980706130215860535939702382948406090174239863)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_142 : Polynomial.coeff recurrence4Scalar2Left 142 = ((40446017113073864351187401014817212094899922434260295115023225 * 10 ^ 70 + 1712660362162048632294651336026376526513455835030301065091273269514725) * 10 ^ 70 + 4064224618337685964882584251315526513045898739034485994034259518161214) * 10 ^ 70 + 504511766335241628383232111625930604243982881498497864098992006833659

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_143 : Polynomial.coeff recurrence4Scalar2Left 143 = -(((198108620659335190423018824756242586095616807415003528563196179 * 10 ^ 70 + 6053710674843364884635466455869884996286698594026510087362843262277263) * 10 ^ 70 + 5730470682276527240183452833954306388060813911124368959130464901325627) * 10 ^ 70 + 377046131890776661408927507704678282199272661007813269583659648477219)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_144 : Polynomial.coeff recurrence4Scalar2Left 144 = ((953333129318724619413974475157980486616509576033553717991910104 * 10 ^ 70 + 2991861689673425573720056343508820183088381936216167152768252571209709) * 10 ^ 70 + 6623406640574607350260270170170508492104195163143195344060067299560892) * 10 ^ 70 + 5012959795892093564686039699402869025003004537970674584123136903261148

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_145 : Polynomial.coeff recurrence4Scalar2Left 145 = -(((4507699198509346305723413747235172166035739710804636625341519013 * 10 ^ 70 + 5685312405247756970338777477845546065081451397962719718930928725429822) * 10 ^ 70 + 2708789976358149753505178514504828613338006472384486931304592967936160) * 10 ^ 70 + 770655858555193503328167482780172173890797465366584753065900898143611)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_146 : Polynomial.coeff recurrence4Scalar2Left 146 = ((20945358325831401847373328755924782415276543051394150945637114977 * 10 ^ 70 + 1232632127386749265203421570487334117843426911682042520778806419604590) * 10 ^ 70 + 2663816282896631573613331668655036191264168238266802142294909659156598) * 10 ^ 70 + 8886317947040047078129422034546152732517295044853407497472665873923885

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_147 : Polynomial.coeff recurrence4Scalar2Left 147 = -(((95652315670819859062028445501308228987291336500714063366486301465 * 10 ^ 70 + 8927723207692081783240526526812329415756316245107320308130836626864763) * 10 ^ 70 + 4319246520338611230998050788603432868574366906714406202186647328333930) * 10 ^ 70 + 3240293306161838792336813600327205295123794969371077197469742864541879)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_148 : Polynomial.coeff recurrence4Scalar2Left 148 = ((429367100475386819238044105979047261688475092956973713188689158528 * 10 ^ 70 + 1671898643952734466855613241286822640315600777792925227773643736573966) * 10 ^ 70 + 8214124354247543206874304329764901447229628836608788239689374734524457) * 10 ^ 70 + 1206321647626054751431584678819056536124763020334454800669232752505470

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_149 : Polynomial.coeff recurrence4Scalar2Left 149 = -(((1894684803572332316974706888964989443476476818892057686617775754292 * 10 ^ 70 + 7350382883575191827641404314296779753305022215405657222775870960144968) * 10 ^ 70 + 1791971675805717763951284607763058442079230860120918568116716448393221) * 10 ^ 70 + 6074163041915007360231882263954855113140517908685643325363326918132526)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_150 : Polynomial.coeff recurrence4Scalar2Left 150 = ((8219929554173120314712397272850209964091368693545323802283211498070 * 10 ^ 70 + 7069107290089655776726342005550320121160854226820101498708281192160938) * 10 ^ 70 + 947508284406015987759938186299484406883923975400449349856152541919428) * 10 ^ 70 + 8199100826564675213523588131051369943297126157876293150686524451575534

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_151 : Polynomial.coeff recurrence4Scalar2Left 151 = -(((35064592237020586287350110581777386590707276427667556402291192722250 * 10 ^ 70 + 7769811714083431626147156186238818321740696041967449816403182136862853) * 10 ^ 70 + 6591620055433077808504537655109087317902446531846511222914795377618002) * 10 ^ 70 + 606651730227447900673887712825995462683943597370834073153213214191079)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_152 : Polynomial.coeff recurrence4Scalar2Left 152 = ((147090434270508235081067927936921093850697645542565282462013192995844 * 10 ^ 70 + 5903796872027316721649165104042353280866272333123269470934454219799298) * 10 ^ 70 + 2765778160065540649030406731555285216261973146580971213906873795354508) * 10 ^ 70 + 6953700691020435196055124250795548501588834796288549198741114346022618

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_153 : Polynomial.coeff recurrence4Scalar2Left 153 = -(((606818926232453240210778347197328327444697762662305977539354237600693 * 10 ^ 70 + 1498980240130495706953716971337166267562946645040450645814951782464710) * 10 ^ 70 + 7898921688900611477147216524413067282247490872198861045850521730790145) * 10 ^ 70 + 5219461655166725084452244752851934449686903306619757706784624261111095)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_154 : Polynomial.coeff recurrence4Scalar2Left 154 = ((2462270388979677580578640938064080644728453492571407283490667053883013 * 10 ^ 70 + 658521974375277649711133569508376242566872635808161335279951869378436) * 10 ^ 70 + 293440762230908452218145515818273163761100840264570632349684986544494) * 10 ^ 70 + 116613546670841964730611606038236794230128015869382822508782725793907

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_155 : Polynomial.coeff recurrence4Scalar2Left 155 = -(((9827792985562580650807737913570641238598501082245629778512331016279585 * 10 ^ 70 + 5982068158416714569185951968060097074517919307000369643329183785252808) * 10 ^ 70 + 3084323851181614324499436778592381088564239091452662734676331136395373) * 10 ^ 70 + 2534897070842470068504738751803028003417499918209552599075411642958324)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_156 : Polynomial.coeff recurrence4Scalar2Left 156 = (((3 * 10 ^ 70 + 8588724583707045895833244817927684611616113855593981624278647881048532) * 10 ^ 70 + 5334696112954456797629968785939464413644900620544268351706808888858856) * 10 ^ 70 + 5378598068448120928732791656697462311171517700321078802864263576873784) * 10 ^ 70 + 9712425796538891244422714213960546022974424494542436836908328955150923

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_157 : Polynomial.coeff recurrence4Scalar2Left 157 = -((((14 * 10 ^ 70 + 9069371210808551903330581384943434085351989415190973717500013843296797) * 10 ^ 70 + 2288997565728158393166139390638052600242302434961892334750344048167127) * 10 ^ 70 + 2445112799581751462738044875179101214224612149239158838308085468444192) * 10 ^ 70 + 6900270348925182357106975984853031578052384169715059545823741240111957)