Recurrence 4 lookup certificate: B3A4 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.recurrence4B3A4_coeff_183 : Polynomial.coeff recurrence4B3A4 183 = -((4180143858508476540858978507361311594826244345277641596311240 * 10 ^ 70 + 641818959349541219209518458530186536004694959663759479618022342150206) * 10 ^ 70 + 3664145813826265744944030608338534521296853947342423676481703253044203)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_184 : Polynomial.coeff recurrence4B3A4 184 = (3995816924820522537211226265839682699921957837883005710593366 * 10 ^ 70 + 3858911078805868863432878931144161434317263267693006258359699396440768) * 10 ^ 70 + 3943534384690300538572576325210653432021699901573773413380384144847087

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_185 : Polynomial.coeff recurrence4B3A4 185 = -((3637554994176223764487902915643030931817138031346047444367038 * 10 ^ 70 + 5046720310916804221523594856301078783615220374007231004201209203717982) * 10 ^ 70 + 6366065446198122094303172896538850001480332741674881915479347559553231)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_186 : Polynomial.coeff recurrence4B3A4 186 = (3177527061372675029112592537232894480896146250555795637816807 * 10 ^ 70 + 4798615812600696153475482859900834916036709455710829156594911339383395) * 10 ^ 70 + 2881658341991428123653352191424761615930022423850656443765135076973737

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_187 : Polynomial.coeff recurrence4B3A4 187 = -((2676302418930648452781809475195484162609561825123449097881865 * 10 ^ 70 + 6357669034280410612738959802667553099191980345307481550966647192736023) * 10 ^ 70 + 4996517264711280953494278100439327495057689324055015718769260618624337)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_188 : Polynomial.coeff recurrence4B3A4 188 = (2180451331058211141053987210843984178538410832164292291397024 * 10 ^ 70 + 4467581584911962764290187519499064048040314188338237942304421964150338) * 10 ^ 70 + 4352460408472028842956116364331291654691697792194005218963959859801864

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_189 : Polynomial.coeff recurrence4B3A4 189 = -((1722229225596053738638075709445920709380571703348238685933114 * 10 ^ 70 + 4599958109385506739917689943653705389180213395975309502164664068308667) * 10 ^ 70 + 2739042997806692101115594167223470012468553686783408275453161343832882)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_190 : Polynomial.coeff recurrence4B3A4 190 = (1320841728590254856233253737266523880283984573213591561840804 * 10 ^ 70 + 5578444898238591514035341586819213528937557717487623390260807532727974) * 10 ^ 70 + 7857792275732133725729145080030527917802653241966207015660017672516231

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_191 : Polynomial.coeff recurrence4B3A4 191 = -((984705251410877097810170665628424516837962282567609617971127 * 10 ^ 70 + 8022529597410387695630443218269727514257609544498621427393735543299868) * 10 ^ 70 + 6658959826420785596275037844302927959510053471478889753490478405358374)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_192 : Polynomial.coeff recurrence4B3A4 192 = (714145684126146521918844766032869231203187859436656429145310 * 10 ^ 70 + 23465742975566153461646714062887689131902689016353468014854729379367) * 10 ^ 70 + 3790474021876462459045979284228976146311549980162305805166022530062218

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_193 : Polynomial.coeff recurrence4B3A4 193 = -((504081512789996793217375976653160174143461002001018485259565 * 10 ^ 70 + 3957720017433161111099175303125443874519184497137846436926687826691090) * 10 ^ 70 + 4893224057688477823693448629441552363196932121888747106129974280572327)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_194 : Polynomial.coeff recurrence4B3A4 194 = (346378571220193938768486041292234201317363596106488008205391 * 10 ^ 70 + 9116724825822999540249629625091435066520519889326230126490795344511112) * 10 ^ 70 + 7945504311934304221637129835606473555669420178592183769315727561092199

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_195 : Polynomial.coeff recurrence4B3A4 195 = -((231707413191399880825985717789625451763145646191784547366928 * 10 ^ 70 + 2631668668566468025735693021135499694876684488211649196777033821912757) * 10 ^ 70 + 586572266020341771102363167834672347095077519841581022937779134583594)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_196 : Polynomial.coeff recurrence4B3A4 196 = (150856579718489913044813029858362015189311428900463560427222 * 10 ^ 70 + 126414543590588878115024417490523683241394912055663116539332829671007) * 10 ^ 70 + 413221257576309478377796571255117756089021820025088366788439502605124

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_197 : Polynomial.coeff recurrence4B3A4 197 = -((95543019094774836853934989025377237940276505687894985567619 * 10 ^ 70 + 5565611381939768751394219851828267899083101118462284159783826610587225) * 10 ^ 70 + 2125678330702915102196443914189860752893604811087882274985830142255946)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_198 : Polynomial.coeff recurrence4B3A4 198 = (58812074855794631734325199623534389286671219998707638108630 * 10 ^ 70 + 5646408583802541942888179605306548572044466971801757442666874208622066) * 10 ^ 70 + 9928129553965639809067727817228705228760348735688178866152254924967803

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_199 : Polynomial.coeff recurrence4B3A4 199 = -((35138600088274906858679850136091915678461940089669326848877 * 10 ^ 70 + 6324180382272201097342589689512645461687388872226799733445086767726408) * 10 ^ 70 + 423864248112521654883754075596200254263631297842759240599074652862356)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_200 : Polynomial.coeff recurrence4B3A4 200 = (20336563367429645980705767828324404094317349173185313056688 * 10 ^ 70 + 4973136070477178021307700458457005111914924403315209095559189698815951) * 10 ^ 70 + 1332600817723987860302969586019259570178400834320535715869597855506083

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_201 : Polynomial.coeff recurrence4B3A4 201 = -((11366495353273240915894251252602127609755405139871274618924 * 10 ^ 70 + 17378782493623633939340239665964183824090901440319715383801714625556) * 10 ^ 70 + 5342393005135214772007781416179988740086706905859750288426417788799854)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_202 : Polynomial.coeff recurrence4B3A4 202 = (6106540927608630249631005500769042713107190447748993220599 * 10 ^ 70 + 8590906778975300138068001784354319971185231231826245698717165507190653) * 10 ^ 70 + 7308980918325408693415339551878617825642748039427543399697946189007655

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_203 : Polynomial.coeff recurrence4B3A4 203 = -((3129677075487442526739522860593903798181312967633968185800 * 10 ^ 70 + 9767851529917139668478391223897545395352853478935381814118118535659206) * 10 ^ 70 + 447290170921129070301286897806585942936076909818553235961586964151156)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_204 : Polynomial.coeff recurrence4B3A4 204 = (1510291615863271652745588967228798771702352528374504091010 * 10 ^ 70 + 386297740277753843676234220513239916496687497476749666542765445906219) * 10 ^ 70 + 546797136437315312697818607998355619391043469496245220074417804903562

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_205 : Polynomial.coeff recurrence4B3A4 205 = -((669151369635943777137227279591927067428138744845602147236 * 10 ^ 70 + 6278988363171026439733999398561714600295047333756952507593096267034920) * 10 ^ 70 + 4754031671917475442055602563079619599715866311168312072135178698176035)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_206 : Polynomial.coeff recurrence4B3A4 206 = (256718499677192076717525134096301269348565081267257180630 * 10 ^ 70 + 842495130264200929985569041795188301138543175889286988467221910271302) * 10 ^ 70 + 2591630221781658401101264978192826397124205872771889431046434693668734

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_207 : Polynomial.coeff recurrence4B3A4 207 = -((69891038407795409698015121984336367195362249305798518939 * 10 ^ 70 + 2617507220029325565161355343346789296034895690354719930702655038729659) * 10 ^ 70 + 9608586900182371864949750810740324806258613736158477095148866271368851)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_208 : Polynomial.coeff recurrence4B3A4 208 = -((4644811418846471185475020929850689047343790350421460890 * 10 ^ 70 + 9072143416509198543215886534074850676747997866585115811395635436139522) * 10 ^ 70 + 8378961249441631079165677041594721651531930426076708835993211613325030)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_209 : Polynomial.coeff recurrence4B3A4 209 = (27289912642454765826312633873342292917547730625619733898 * 10 ^ 70 + 4033584147136267163038263415899593117142810857477950137015734780530124) * 10 ^ 70 + 4856758249590434346985456121849394196256858780766555077078683971816303

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_210 : Polynomial.coeff recurrence4B3A4 210 = -((28538662785557589200446352191530794082872199963341633507 * 10 ^ 70 + 2530416888757232713771928930964847411744201702671173197061216227079737) * 10 ^ 70 + 5418326981530225282155540262294953891603022902815591441848590929760152)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_211 : Polynomial.coeff recurrence4B3A4 211 = (22740468722941059636481740304122389338558018118670063792 * 10 ^ 70 + 6739297548187225322262873024342313256868189453795131262624095718159242) * 10 ^ 70 + 8889134811778444195013634990379247945958255552260567683883866667574813

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_212 : Polynomial.coeff recurrence4B3A4 212 = -((15982033767915420290951339770683992087420260362520967625 * 10 ^ 70 + 8688680289144741422122537119680085731306020658880030544537587761165213) * 10 ^ 70 + 7075326731465485423294173741174436209993435464230015113762246374955387)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_213 : Polynomial.coeff recurrence4B3A4 213 = (10396708977828404146225380200698366691855309159576298242 * 10 ^ 70 + 5106559213671476955529410806472048236705641154805546931169857950163551) * 10 ^ 70 + 8969102711711199135123631246219244210132897744313617954707985937554406

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_214 : Polynomial.coeff recurrence4B3A4 214 = -((6399004211506657593313676377347875038156418109631257623 * 10 ^ 70 + 7216730879231001308318406526921995151161990010568096393430565551914900) * 10 ^ 70 + 5770148811002709584707260745057022251037426621145702283260859575494289)