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_244 : Polynomial.coeff recurrence4B3A4 244 = (82859251955136728534456300876436220527113651 * 10 ^ 70 + 4295256671755794848285049803963402104410146267740004223965982064786190) * 10 ^ 70 + 3572057718729915177137060095163215499535037596159723663075199597947595

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_245 : Polynomial.coeff recurrence4B3A4 245 = -((37953130188619760892070608068176147664607889 * 10 ^ 70 + 9237706415130664274812731180750890957009411791427596125386802381492405) * 10 ^ 70 + 7163895844846739682761295069946279900992997558609334680856294103953893)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_246 : Polynomial.coeff recurrence4B3A4 246 = (16678500643657198443949427357161917478966530 * 10 ^ 70 + 1123040529097114875722062667848068783787049801251166602693525727355385) * 10 ^ 70 + 9233620841607286679946419039218775464721141252168634172721765891409406

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_247 : Polynomial.coeff recurrence4B3A4 247 = -((7046114101947233054185195723590046303730814 * 10 ^ 70 + 9104933129349908133330354203999122475874542522227970968485206976754358) * 10 ^ 70 + 4735228865006975405676867620573093219808005269054535808952969176859586)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_248 : Polynomial.coeff recurrence4B3A4 248 = (2859876230185277107635665387895054347555766 * 10 ^ 70 + 5601666309683313715481244640997599116108099744598183326488624404479045) * 10 ^ 70 + 3055860818143613898623423704487079945882597750771708714367336735680571

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_249 : Polynomial.coeff recurrence4B3A4 249 = -((1112339485244252217870210898937255895815218 * 10 ^ 70 + 6860675429961399816187529545576698523620012139044337529770275832702321) * 10 ^ 70 + 852988519196705561193579058394487904450835219878410986834007944363941)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_250 : Polynomial.coeff recurrence4B3A4 250 = (412769561635244863083470177879907136386389 * 10 ^ 70 + 1385470884820471708458155024321999921563590141572183598653278029799077) * 10 ^ 70 + 8538413679080417336561640928192668659329081572714995924918897379154648

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_251 : Polynomial.coeff recurrence4B3A4 251 = -((145147638914417912396386477958197861774146 * 10 ^ 70 + 9714443546232852409880937509091958975757990245289767478503695100885906) * 10 ^ 70 + 3424628757005447334541296356533500808408887992106525220067377791588200)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_252 : Polynomial.coeff recurrence4B3A4 252 = (47852557575069867672715422126623753458131 * 10 ^ 70 + 3565075856462395733756075275454646901366123675192834139111490264510967) * 10 ^ 70 + 2846878691374671032221325482997197310332876301572963101524345465038164

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_253 : Polynomial.coeff recurrence4B3A4 253 = -((14523039562892106753840802431440909887576 * 10 ^ 70 + 4931734875080869336613536396459281361769297398046085539357330933259024) * 10 ^ 70 + 6008043212665000499992256479259083422756241396998791420521491090646637)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_254 : Polynomial.coeff recurrence4B3A4 254 = (3913600683243822999621046547869642313590 * 10 ^ 70 + 441266457746992613052103919145585890216382479851056554126366622862000) * 10 ^ 70 + 2055429294424460797249135581637071404271056633663734299402454821371100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_255 : Polynomial.coeff recurrence4B3A4 255 = -((854074929819220648436357170412000253644 * 10 ^ 70 + 132130281082424238955597423431716799435412516557392745092249845947355) * 10 ^ 70 + 5059253802774043284961958886406372861627963656241860301704670061019709)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_256 : Polynomial.coeff recurrence4B3A4 256 = (98323794769780094649407919126535556209 * 10 ^ 70 + 8332773210371804175671109384813709269757461544545365351103660088946949) * 10 ^ 70 + 4220279747444879178447679138061187223767604267975688811123337336279938

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_257 : Polynomial.coeff recurrence4B3A4 257 = (35387900189656742631531095895309703548 * 10 ^ 70 + 6145975739200543878708550897098747440692352260523722530648518833981103) * 10 ^ 70 + 2415988002469810010815878939246797055509977274221303359918856717933258

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_258 : Polynomial.coeff recurrence4B3A4 258 = -((33984553059933006813851853946006419723 * 10 ^ 70 + 8598764251792963245065311901107146799190373331628988841060069340609447) * 10 ^ 70 + 6956781345691076472303729552669785557030985735254239004878318155330408)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_259 : Polynomial.coeff recurrence4B3A4 259 = (17661128696825722373022603221584663505 * 10 ^ 70 + 9619091298715722999618056415866827636630470256571259981610800917174880) * 10 ^ 70 + 5360263576705260111736521879500210183749807861143572038073188521635495

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_260 : Polynomial.coeff recurrence4B3A4 260 = -((7389912004866915635843495409019366006 * 10 ^ 70 + 9248185954176430784551660180257775749412734975089546322226049154798834) * 10 ^ 70 + 8803350802096386064400195783654284875418347876755731976395412747582332)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_261 : Polynomial.coeff recurrence4B3A4 261 = (2706429516472781261514012931465764621 * 10 ^ 70 + 3120691282153534062198724972431774818231217842393798138639890837706507) * 10 ^ 70 + 8398910898165139302755454766891663605905679683982292886325159347872540

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_262 : Polynomial.coeff recurrence4B3A4 262 = -((891547097249974456580452858326760272 * 10 ^ 70 + 3182011402201796782987138085967075973649595913443656538556096875230349) * 10 ^ 70 + 189855106431831841137802653190035743168031373964866248714288025880322)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_263 : Polynomial.coeff recurrence4B3A4 263 = (265325287834601844471981242958785470 * 10 ^ 70 + 7068715653469948226148395917369153463348870412724803098871995594681184) * 10 ^ 70 + 3593621969315663272248678779432515640737432931707905673752944215322255

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_264 : Polynomial.coeff recurrence4B3A4 264 = -((70122606754248824932310425367104530 * 10 ^ 70 + 2199887411873968221205773533959916927800783939788588049278678678205515) * 10 ^ 70 + 9699508063357805085699785392889110054666502325139658511348284421395356)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_265 : Polynomial.coeff recurrence4B3A4 265 = (15424940187931269570493148935719224 * 10 ^ 70 + 7379770984457804172057204691300814793807023580130468751065349464167947) * 10 ^ 70 + 3429323281786150415048029888688911247946511089064967866001404998428264

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_266 : Polynomial.coeff recurrence4B3A4 266 = -((2103840496021547360452116371668644 * 10 ^ 70 + 1057327211486152236085025969375759643359543816902376770563246235649731) * 10 ^ 70 + 8021273654417470344337066103227693575643322759711199552589590546571240)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_267 : Polynomial.coeff recurrence4B3A4 267 = -((383806252021653240785649741784834 * 10 ^ 70 + 1528287219062692705721588826502035325897795661459084867556340396052271) * 10 ^ 70 + 9056578332981300539116347732984832629769914176044407666587905872714530)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_268 : Polynomial.coeff recurrence4B3A4 268 = (501793254296427666428158972305162 * 10 ^ 70 + 1071998540818671232215800122674950614890961711889433091630380096900368) * 10 ^ 70 + 9889165604223577240316212886558658804464425918537178565640597631012421

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_269 : Polynomial.coeff recurrence4B3A4 269 = -((293380975201200755931500049435971 * 10 ^ 70 + 8340813341170181176739172272801170821924522740103384066727515269661633) * 10 ^ 70 + 1492609126148510109584087790394799549028956473742112475244137461055125)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_270 : Polynomial.coeff recurrence4B3A4 270 = (139476580418114380304825639317171 * 10 ^ 70 + 4839724450135537051747889901486153243294262132101800926067238523176566) * 10 ^ 70 + 5120862048595348215002232248897975389382980915228777527293622877458357

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_271 : Polynomial.coeff recurrence4B3A4 271 = -((59836251681198190225644740211663 * 10 ^ 70 + 7681805167409891175905018333448214594343850739185216696832893201199467) * 10 ^ 70 + 7796965506151888632123474020915754732682740874640658748950487693084500)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_272 : Polynomial.coeff recurrence4B3A4 272 = (23993838635711418307492964263542 * 10 ^ 70 + 5541224860847948133917047981176426607728335617253775815413455227763433) * 10 ^ 70 + 7079738545347724718965384234610382087686367094636839056741622871814029

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_273 : Polynomial.coeff recurrence4B3A4 273 = -((9120690554770471950143129573268 * 10 ^ 70 + 9396158766066987264469991347077094195132244452941571139092056090035978) * 10 ^ 70 + 6459205885439143178359185743940134206765040440241313514048142831329551)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_274 : Polynomial.coeff recurrence4B3A4 274 = (3304252153105216594761395240844 * 10 ^ 70 + 5294511565361741471486484286035853107156330450328890559599089036328611) * 10 ^ 70 + 5929889112622867807714850875522489876272582880161732552625931265438964