Recurrence 2 lookup certificate: Scalar2Left 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.recurrence2Scalar2Left_coeff_144 : Polynomial.coeff recurrence2Scalar2Left 144 = -((11794399837792569195182103219239828050 * 10 ^ 70 + 2022741476255043946006869110175889433928867249001765580412292320881469) * 10 ^ 70 + 8130553314381741414869994998296567025530426455799276934099503469667851)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_145 : Polynomial.coeff recurrence2Scalar2Left 145 = (65927675241520560791099113513771365585 * 10 ^ 70 + 4830320928968748700634397493504159649689330242703171766657704022143289) * 10 ^ 70 + 3718034937433184322539404594414728750315543523349494840493048832321298

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_146 : Polynomial.coeff recurrence2Scalar2Left 146 = -((70190760132429631002595692590693494943 * 10 ^ 70 + 6929333638671330170847411382633867821771517935082946232335901066216543) * 10 ^ 70 + 610537560688827354477902863372711025315839008659893971683845566867512)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_147 : Polynomial.coeff recurrence2Scalar2Left 147 = -((594222424915232254748840503720591659392 * 10 ^ 70 + 1570942055319156601483447572701577226379420429939008227796579455705159) * 10 ^ 70 + 2174350801367495714856624221540563705188251005924176961400950791957119)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_148 : Polynomial.coeff recurrence2Scalar2Left 148 = (2731514562523465416778279832758861230596 * 10 ^ 70 + 9681876736225416110718444286423547384168086807853077693252911201781993) * 10 ^ 70 + 8852545362131323154852520966923129155346550299239666424749534227627085

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_149 : Polynomial.coeff recurrence2Scalar2Left 149 = -((953156868689262796082104090081851528606 * 10 ^ 70 + 4667997754225929834435764410259071043970505180307536143510385271935823) * 10 ^ 70 + 1980966674003856132366603619793728751121083005209638262882745332883329)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_150 : Polynomial.coeff recurrence2Scalar2Left 150 = -((31981106473544408150550006266019016953404 * 10 ^ 70 + 1690801012141992921660778097270749559853991423552977269060237330554375) * 10 ^ 70 + 4193381779932200414790917902343771514504174820764609893383936946096)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_151 : Polynomial.coeff recurrence2Scalar2Left 151 = (110905396567926465917869989138484369678436 * 10 ^ 70 + 4887110675216515866636847575815317264259685645419782833845917346214002) * 10 ^ 70 + 3785062574258363653566923261086378044498483761740477962762550207539326

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_152 : Polynomial.coeff recurrence2Scalar2Left 152 = (87202347688568147536747366338709281529946 * 10 ^ 70 + 9059861946091043230675149463507352594828383660600089483124298536636330) * 10 ^ 70 + 8134152720467227119871676811627236261521438122460068625445527903902785

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_153 : Polynomial.coeff recurrence2Scalar2Left 153 = -((1885647683223483516504714523116973756703126 * 10 ^ 70 + 182194285125593925092962261471374229719695627601173741506428660946288) * 10 ^ 70 + 2668568164521463465414206412756621680199251607000298703338276971108407)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_154 : Polynomial.coeff recurrence2Scalar2Left 154 = (5607355020018830949086246488503991494840511 * 10 ^ 70 + 7610019046382955785573453124239967762082521385496353186884034590504356) * 10 ^ 70 + 4073005346714398301112514500618488966552469798029205134971137005278973

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_155 : Polynomial.coeff recurrence2Scalar2Left 155 = (5418938120094153028642542586981246022731497 * 10 ^ 70 + 2188358481321766987751404826964821329896917546821308106349885769786288) * 10 ^ 70 + 9198759553055836677011852398608374264394008200436030247368358112120943

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_156 : Polynomial.coeff recurrence2Scalar2Left 156 = -((98030985934313753901188341541746575066809597 * 10 ^ 70 + 1253889738490251115035697987303516242314440752368004593430242298145796) * 10 ^ 70 + 7704241580327418851056441148054229837902295875260802009802899452768182)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_157 : Polynomial.coeff recurrence2Scalar2Left 157 = (311371738636520531362666469624846219195754944 * 10 ^ 70 + 2006432369402699771458348479445267850589954052525655473315108688589276) * 10 ^ 70 + 8491160425298406866889485307768029157085419804049000823024369756325916

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_158 : Polynomial.coeff recurrence2Scalar2Left 158 = (41526280824016409669534356658193706744148015 * 10 ^ 70 + 4584299147207909486086142365154754897518768880779501787891268719398101) * 10 ^ 70 + 634575259291389450453178374674345724870486362776717468061940818846346

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_159 : Polynomial.coeff recurrence2Scalar2Left 159 = -((4063685872183626914798392201056537914348394193 * 10 ^ 70 + 3126742767900938546552350143317842744792448354825373592947686701649589) * 10 ^ 70 + 4728144261832349857784169955532403478384942426216891547282133484564518)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_160 : Polynomial.coeff recurrence2Scalar2Left 160 = (15490057036555114166356904783244404205283149692 * 10 ^ 70 + 6300539794452947637686360189285444336017903431248765134579017475674330) * 10 ^ 70 + 9828845637272489110672450338527246545945806784456451097400784701347583

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_161 : Polynomial.coeff recurrence2Scalar2Left 161 = -((12869366777976457448687792495610624843831074988 * 10 ^ 70 + 173556532658843422826198126072342224546331921665140851838639214886294) * 10 ^ 70 + 5231451959156461398048512440966938508514840689646844038975115984319723)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_162 : Polynomial.coeff recurrence2Scalar2Left 162 = -((127047124722664001108194900480663830014161673335 * 10 ^ 70 + 5693556278035965054119154512509005878029970156158569220586198360847675) * 10 ^ 70 + 1333258549218327955872795152569352943602437667927568958249834498303554)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_163 : Polynomial.coeff recurrence2Scalar2Left 163 = (635725806173754211393327587299047198969417520794 * 10 ^ 70 + 9499969975875136354624525917416265114137956176513357747876912699630739) * 10 ^ 70 + 46924312877611404562820708323968618521199987500904271169365323363862

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_164 : Polynomial.coeff recurrence2Scalar2Left 164 = -((1069338406764983241201863288870632146978845534435 * 10 ^ 70 + 1619693264882698997588882678194499769539030502931655499339296855378014) * 10 ^ 70 + 7806110463276867283387630623605356841804021994043157866019500705021688)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_165 : Polynomial.coeff recurrence2Scalar2Left 165 = -((2648142837513308471859014318744850996239670746025 * 10 ^ 70 + 5317811366222418182313137963021195034344873710768300039049058624375277) * 10 ^ 70 + 2709307262658908296516566054057899799905834691721179239886368304291840)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_166 : Polynomial.coeff recurrence2Scalar2Left 166 = (21178659047174245962126335195184745846157810705217 * 10 ^ 70 + 3400105412225348681900811615804179041831956673751332335982033983511470) * 10 ^ 70 + 8866222980513482009516800030067126744192435403051359869450838659512823

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_167 : Polynomial.coeff recurrence2Scalar2Left 167 = -((53262636427985257820777234542267040621819883593834 * 10 ^ 70 + 4179685984253647943511296300617582773310363024504674112340558134215412) * 10 ^ 70 + 3570329662258148249789532853130662821235238848142963609284007349317488)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_168 : Polynomial.coeff recurrence2Scalar2Left 168 = -((10908911221474547840679428129967974831789267937515 * 10 ^ 70 + 4419980603463922600044028698233586682749302102087289894200229901954918) * 10 ^ 70 + 2329470928816754624471416622625794280389753930687870205096532194080394)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_169 : Polynomial.coeff recurrence2Scalar2Left 169 = (566065971867870058159558861420521828632026756108209 * 10 ^ 70 + 4970774734869227218156587753501024651079963803951552941259963250716189) * 10 ^ 70 + 7844689737928743857670024090593535213982080373026074422940337163878200

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_170 : Polynomial.coeff recurrence2Scalar2Left 170 = -((2025766800204495354544381384765802086214733700965148 * 10 ^ 70 + 5345779810110160880909417560195564966900761089420296982817273951186108) * 10 ^ 70 + 7799443199499860536340346320236367097488823487629288205256496062031921)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_171 : Polynomial.coeff recurrence2Scalar2Left 171 = (2206781942362885174590826719477851851253046450425441 * 10 ^ 70 + 9424131749759565584243542539128576093089238785667984324575920940911509) * 10 ^ 70 + 9663149897831534906282042283278425806335221964932922155093846519303454

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_172 : Polynomial.coeff recurrence2Scalar2Left 172 = (10847248708218683342484777207780305272007077477502230 * 10 ^ 70 + 1753296221968756802281438752004925241897696713875792323060720064199230) * 10 ^ 70 + 1787700728196211535978792093098805901695698560839997582541099255159401

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_173 : Polynomial.coeff recurrence2Scalar2Left 173 = -((61730162546794158370561143938710363461386684700934370 * 10 ^ 70 + 4921855213082151333187117334387535568002445778691909499264915686170524) * 10 ^ 70 + 6944196445402067331235066070140593829339003235809694976273041351619228)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_174 : Polynomial.coeff recurrence2Scalar2Left 174 = (134648756847694839433399723690010917198304038548336808 * 10 ^ 70 + 6654561572765296737251108283940612149331641536987958425960017362510993) * 10 ^ 70 + 2459621370680426615980018216508823639078534304549256954981497210031826

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_175 : Polynomial.coeff recurrence2Scalar2Left 175 = (47593446914886227851881505498771724902057357449459047 * 10 ^ 70 + 9008274496429978103490964053107334659952365771664624171948395175491777) * 10 ^ 70 + 1779266938591457907107840237368670044466039216979947342761956806078768

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_176 : Polynomial.coeff recurrence2Scalar2Left 176 = -((1388216938664807203917524014559693685582444739861163133 * 10 ^ 70 + 63966473791131138725682865582818990070284889395354354133696647416899) * 10 ^ 70 + 8117431346423845164298735683240858529772468070657531749832678993904603)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_177 : Polynomial.coeff recurrence2Scalar2Left 177 = (4910066166086968267612027543666267911115721324164787196 * 10 ^ 70 + 1308028607681397754710781127530257962900258982208431594783301116032039) * 10 ^ 70 + 8471971431904373028882881965590119709945129718581049296024414879563487

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_178 : Polynomial.coeff recurrence2Scalar2Left 178 = -((6863516558401828582284673644742371801909665726726595858 * 10 ^ 70 + 2905541143222839522740739408635278949046437488807463986424106407036603) * 10 ^ 70 + 6112919327407147044934736342440067824109199405035856024108653401496381)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_179 : Polynomial.coeff recurrence2Scalar2Left 179 = -((15353389551891325768296696814951029614265430583693616522 * 10 ^ 70 + 3138454749523930217230703386626333628037126953510727269663174502855031) * 10 ^ 70 + 8304176510337568025645906944069989850699681241191320424386908324878193)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_180 : Polynomial.coeff recurrence2Scalar2Left 180 = (116645720734528903986506375626545131311181122789546362174 * 10 ^ 70 + 8868987757390914286701852515669590501556385033622686897170071820074272) * 10 ^ 70 + 4258862364371701456720295200619148579624978610004903823358600531806849

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_181 : Polynomial.coeff recurrence2Scalar2Left 181 = -((324362221101189110067618324605615346533181686311445433000 * 10 ^ 70 + 3030349440780183018720569011725711601138428903057441562680795700456748) * 10 ^ 70 + 3998036648439774889125729727455060375260787790169034066195185709407066)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_182 : Polynomial.coeff recurrence2Scalar2Left 182 = (312494953755837722743190013236774762818237031977309036776 * 10 ^ 70 + 6358099405083535829773128590864195478445672903886924116121253030691249) * 10 ^ 70 + 8081197731362498517951778435442550123231102234247778313275270158669343

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_183 : Polynomial.coeff recurrence2Scalar2Left 183 = (1361198100290975601336192465039167769008297888602019266108 * 10 ^ 70 + 4317184565461902227816703172478452588982098028255236843129760704253657) * 10 ^ 70 + 9619179386306469967841583729216480083187704993337349874582024188530437

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_184 : Polynomial.coeff recurrence2Scalar2Left 184 = -((7692874454502926268648460984526669634066062139571950745211 * 10 ^ 70 + 4652421503625029872382622631261665927938257570510903253225897197778974) * 10 ^ 70 + 7543231560588891588393011476459169427913209095243969199560941730731248)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_185 : Polynomial.coeff recurrence2Scalar2Left 185 = (19343089727956890748044390026017571662215806762156391362711 * 10 ^ 70 + 998168353787674801028395985159879915052604578779111113416587171856697) * 10 ^ 70 + 8743258813037350025110319158828333640681964420340843799180163245918851

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_186 : Polynomial.coeff recurrence2Scalar2Left 186 = -((17048126872111611135639187575193203953210040595856871167921 * 10 ^ 70 + 8864125556659534419628899887136124391695793540730063368308798324330253) * 10 ^ 70 + 1213102101189271186713496274316414481769823689850936409560578828756608)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_187 : Polynomial.coeff recurrence2Scalar2Left 187 = -((76791793144827385082482325427987731305726418936331115860892 * 10 ^ 70 + 1782703393062683509823077934100953331923987056341703053915843163974518) * 10 ^ 70 + 4593210509126481037882613134983139049333570089224690203292009570430708)