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_215 : Polynomial.coeff recurrence4B3A4 215 = (3770324010414482394605607206693775689482175796570686306 * 10 ^ 70 + 9304077907664459136996933734967950917967890754219958556015972096945733) * 10 ^ 70 + 4966223572402946692803511558652005847955143799076062743257320483835823

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_216 : Polynomial.coeff recurrence4B3A4 216 = -((2141434079224488700196839234250482627391651614728182333 * 10 ^ 70 + 4210442631945286677054238498267153511733785475703037508034467705823201) * 10 ^ 70 + 2249908410992908030445268013331794146802877902092623771332597824449157)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_217 : Polynomial.coeff recurrence4B3A4 217 = (1177550720678007035539802055396557833588369168602277117 * 10 ^ 70 + 9142634744387247853617783601016358597571151277101264430382113323833480) * 10 ^ 70 + 7112761609514111641378193044626670611388840016702081090083579827011249

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_218 : Polynomial.coeff recurrence4B3A4 218 = -((628683798726464555826301988997049047467538349216823989 * 10 ^ 70 + 6860665507572520392170453875360290423991534558673513893633746523553301) * 10 ^ 70 + 4766016338623736774313600827619641360803706660950186566651532072263408)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_219 : Polynomial.coeff recurrence4B3A4 219 = (326493515920423383329401119239351109865492872645792815 * 10 ^ 70 + 9049901257275270426983121417359998039112847241681357198340146419348873) * 10 ^ 70 + 1867159062048582136287818796896403858067381456509159407615206026473837

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_220 : Polynomial.coeff recurrence4B3A4 220 = -((165135489506849765689195349421830644590086504744769665 * 10 ^ 70 + 632981548201829867690153002157969043096833304138552310040363808131482) * 10 ^ 70 + 8524830134513143009296330119023229901028999005315906239676860080625749)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_221 : Polynomial.coeff recurrence4B3A4 221 = (81408551780288236608899451600179489078765343881058879 * 10 ^ 70 + 9056655992819184088733996926903870201488680969451011169399933529399010) * 10 ^ 70 + 5391975687847332549650699477382945102202774315769135888033655968872739

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_222 : Polynomial.coeff recurrence4B3A4 222 = -((39134812916039723448618068652280018965907495517521079 * 10 ^ 70 + 5462319893815952238049706960184397939683593874041725489001006960540319) * 10 ^ 70 + 5355801489493785644588522836378125254234879264458391952765169216411575)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_223 : Polynomial.coeff recurrence4B3A4 223 = (18349085625116822598632979276718405373939699595380766 * 10 ^ 70 + 9594769007552443566549150356528170676674697807487655407385525506228171) * 10 ^ 70 + 5747197915593462636304126770245148097838452835787579429900252269190811

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_224 : Polynomial.coeff recurrence4B3A4 224 = -((8391408502738952623237583230273992620193637200229313 * 10 ^ 70 + 6560244404235765719285934113504872591059770642433154465227223390988063) * 10 ^ 70 + 1251240229820587339115260176557311692231032719561067059863182116787146)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_225 : Polynomial.coeff recurrence4B3A4 225 = (3742542602164913099405571370207731549392688006202295 * 10 ^ 70 + 358535616319257944665084661421524985966100771601492055386748644052104) * 10 ^ 70 + 4324325268886477747801595409849318777297705129503277082216384026085689

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_226 : Polynomial.coeff recurrence4B3A4 226 = -((1627382496302569908164018386758005220644436628935888 * 10 ^ 70 + 3341632162225343231811335896311308822900314416415805992160887099485548) * 10 ^ 70 + 7330282786592052657075520380297724519589606716801215541603593019366017)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_227 : Polynomial.coeff recurrence4B3A4 227 = (689635521136473298420415796672665636019513283131254 * 10 ^ 70 + 3791955013790535874900956556432603670575193110447858479881288522374302) * 10 ^ 70 + 4515600958053277450012138205625000583849261282408699452993452178909417

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_228 : Polynomial.coeff recurrence4B3A4 228 = -((284642329490514214419881844783527372685653112457703 * 10 ^ 70 + 5590079411717689805949441472605024224324737786077674111927583112287746) * 10 ^ 70 + 9658536150316790605039610504827781788887184643125441400990871499406656)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_229 : Polynomial.coeff recurrence4B3A4 229 = (114334065615575088775822813463232306025695510196876 * 10 ^ 70 + 3905128801643297841434429541578381997831304541979434084832042617392166) * 10 ^ 70 + 9989066042934616148887404405940293358319815936935087761719643514107289

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_230 : Polynomial.coeff recurrence4B3A4 230 = -((44643016072769947198177701076031410100426462749868 * 10 ^ 70 + 1872382830490867840469839086776002840165594881740079698704859362651269) * 10 ^ 70 + 6496064899626966110677794814006509054065081551645607890600378303760629)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_231 : Polynomial.coeff recurrence4B3A4 231 = (16916669219394716427114725657616641084502469227433 * 10 ^ 70 + 1032730901111136213196194243804001699536070513779908344021848300304900) * 10 ^ 70 + 9012266038941331621300756762118196597340042406719909525238335898124759

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_232 : Polynomial.coeff recurrence4B3A4 232 = -((6205312619522838812155017779979557648473768579295 * 10 ^ 70 + 2560289991034355838782929064833998200617059796483827579563104796257907) * 10 ^ 70 + 3388781098266069550399175448695281652135895655992788350412200279063618)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_233 : Polynomial.coeff recurrence4B3A4 233 = (2194470732930217390793831885133634618593701774787 * 10 ^ 70 + 6150686978909108980945438881767134133213411491554192523756662053297155) * 10 ^ 70 + 7421336793822055137488523678995184421499190225318550606243015098606767

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_234 : Polynomial.coeff recurrence4B3A4 234 = -((742956351742455866914883720419847353155459633057 * 10 ^ 70 + 1574081118247632059381815788641846187804462950740498867574576725694843) * 10 ^ 70 + 8421972673162484689107969243254832915953057524134529581290796275918857)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_235 : Polynomial.coeff recurrence4B3A4 235 = (237670251548326237554824663278674152897308338539 * 10 ^ 70 + 7511877192062227131941522778750779292617477459236614020186294755576280) * 10 ^ 70 + 7362141446753196677661554614247736718808422458066808477856346972124299

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_236 : Polynomial.coeff recurrence4B3A4 236 = -((69900772882398023876259060639981817914314420275 * 10 ^ 70 + 9352731838494624210487203993276730946239814558509498579945849202314138) * 10 ^ 70 + 1136271457838317971291789887269647445735634134712722542047913601015113)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_237 : Polynomial.coeff recurrence4B3A4 237 = (17634411224586505481821186400947269089243224052 * 10 ^ 70 + 9399779076619254152560701953058020331971525072718930082358432192074730) * 10 ^ 70 + 9563078482275375138891120800878603687230754197759281296628379785636792

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_238 : Polynomial.coeff recurrence4B3A4 238 = -((2901719333853415664958238203303817843663639290 * 10 ^ 70 + 3621849534855684169559241490615138579626142732120240059507520881035351) * 10 ^ 70 + 2665186925536466450509991088924284585226205684908179835508929482644634)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_239 : Polynomial.coeff recurrence4B3A4 239 = -((488698472707462977139141176606152325472304899 * 10 ^ 70 + 8922878731555023203251573459304463769585139858128241319107541369926646) * 10 ^ 70 + 101428321452953562596409401393036473146495787298572933163779867168885)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_240 : Polynomial.coeff recurrence4B3A4 240 = (846159528111470900882588147007742439019417421 * 10 ^ 70 + 321604408056984640985346570274722504204481527096306036900774178156828) * 10 ^ 70 + 5355320004698262334941533648113231242773354423144389479925224012498015

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_241 : Polynomial.coeff recurrence4B3A4 241 = -((593677558988642642816548245138501603600544749 * 10 ^ 70 + 5094034130682679730449817381738533632661942360316433855875804064676502) * 10 ^ 70 + 4271907357038119017894442907753471810858643055786310875620582451984848)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_242 : Polynomial.coeff recurrence4B3A4 242 = (336606784232475865146522119934117283445205532 * 10 ^ 70 + 6493184924265900069025355559199975043691664085645874399220739024952480) * 10 ^ 70 + 8155487836006336552803241714180121998702071969532682207498067285944880

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_243 : Polynomial.coeff recurrence4B3A4 243 = -((172415488000386052670594905194775024547229253 * 10 ^ 70 + 916562843595861073819118362784232144965526569796081496104300723316531) * 10 ^ 70 + 4841071206339108733307271403407476498544194077967618624246248368258520)