Recurrence 5 lookup certificate: B1A3 coefficient convolution

This is a checked coefficient-lookup shard for the fifth pseudo-division recurrence in the order-seven certificate.

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_147 : Polynomial.coeff recurrence5B1A3 147 = -(((1696334771169582388970 * 10 ^ 70 + 1966026530578096573451621291948217449677941882332284933278381720933130) * 10 ^ 70 + 9243919591624522445580297336580824866442768952776025888404564519382810) * 10 ^ 70 + 9462935794965288793910172592023300830673960421196233754928336225981228)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_148 : Polynomial.coeff recurrence5B1A3 148 = ((1168738582272903478090 * 10 ^ 70 + 4652498502575117371892790951102417018151937681722567847710231298491101) * 10 ^ 70 + 9006151521380294967408270614872638372373519581328691047634978911051955) * 10 ^ 70 + 8591221023173859750127283027460963237822607476740971460408882332226757

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_149 : Polynomial.coeff recurrence5B1A3 149 = -(((667745789158280733079 * 10 ^ 70 + 3214060340802266070701496802160247571364853455464027256043551797141089) * 10 ^ 70 + 6870054493125727036454062553539548247515300326034213902479843825932138) * 10 ^ 70 + 8573393631876245165870861095721574398632896078157222728545886830199530)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_150 : Polynomial.coeff recurrence5B1A3 150 = ((222491767065150853213 * 10 ^ 70 + 7433526164715881836425481711855752321169238824993227978851826925340228) * 10 ^ 70 + 2347948838405077003763798443733052704654820113221596141113061392619105) * 10 ^ 70 + 2952213231712987160497582705408228128811855809544970054022812561043945

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_151 : Polynomial.coeff recurrence5B1A3 151 = ((145908669090124038113 * 10 ^ 70 + 5970908065571126360572764504094977811149645032015104822179628147971453) * 10 ^ 70 + 2480192702142150412749746872785485102190834908996534419830091531414907) * 10 ^ 70 + 333719159030366615699859868176812053175282329293768689653285538341811

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_152 : Polynomial.coeff recurrence5B1A3 152 = -(((425775527349951458324 * 10 ^ 70 + 6358425841630066315278722020211999438419970278666582857040469899499354) * 10 ^ 70 + 5072592202740952110764364146408480174089781778945791130812223269524299) * 10 ^ 70 + 9673966935149128498335961638391970632043486279093571444665296879784842)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_153 : Polynomial.coeff recurrence5B1A3 153 = ((614883452156075799937 * 10 ^ 70 + 9398135728751386699866175149109371537924321999907717596576265664578659) * 10 ^ 70 + 1637906134231124866479415928118226874003020777776239487027054277135409) * 10 ^ 70 + 6254504433847372819872356563925617161225889353401283076060376980483011

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_154 : Polynomial.coeff recurrence5B1A3 154 = -(((719255060513491107871 * 10 ^ 70 + 2389719419005281065856239249134001475643454084254298106159077603325420) * 10 ^ 70 + 9218884039327324530563919817867172038464076117911831102339476485932659) * 10 ^ 70 + 2665584547015237070743463030860490621844719576368013869651260482952730)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_155 : Polynomial.coeff recurrence5B1A3 155 = ((751084228375487791305 * 10 ^ 70 + 9011498167860773310004964736274429325868434380614985260593559121800905) * 10 ^ 70 + 2380519232283868851914245678465605652246085217526612709544424801628184) * 10 ^ 70 + 5469875499205797880248043314673424806338879656222403446999581258019867

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_156 : Polynomial.coeff recurrence5B1A3 156 = -(((726240085150188712872 * 10 ^ 70 + 3991691443568615061502021127059869137001675634208635855506600276932344) * 10 ^ 70 + 6557656147404013369324630030653781649321319557903618255556149539610778) * 10 ^ 70 + 1556284314681060731246840049573484381314270461804295200261805048345989)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_157 : Polynomial.coeff recurrence5B1A3 157 = ((661796488893218280043 * 10 ^ 70 + 1396324522462921219672092708802797185775409697608741607611196129735669) * 10 ^ 70 + 8230529849609594992647473275964751527395495550593060106479295799197227) * 10 ^ 70 + 5737630650028324087983977052411017188976799914925712628154566773680396

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_158 : Polynomial.coeff recurrence5B1A3 158 = -(((573943276210988164074 * 10 ^ 70 + 6182988196831383784374148395060424751188244984246485590614258377119519) * 10 ^ 70 + 7769457905895964135595380146453528199063180510358881068586575947260364) * 10 ^ 70 + 4276478694713123552812136533339183782416512264686163194997183826510509)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_159 : Polynomial.coeff recurrence5B1A3 159 = ((476498139052099747503 * 10 ^ 70 + 3494268883820268266805654773414180117239509610715107911814812909623334) * 10 ^ 70 + 868268572571494099121381200096677561537728864304149620803908646939134) * 10 ^ 70 + 1186834055792559106479006163571029331888718533794683854948754034905868

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_160 : Polynomial.coeff recurrence5B1A3 160 = -(((380089717897558270606 * 10 ^ 70 + 7632347964880164255713327865192823216747563703851520986583628338053947) * 10 ^ 70 + 9016918485689347319597849567370702979536108397151088853368977261349476) * 10 ^ 70 + 7371035274421870772219125856428446134039085483830602367214131974068994)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_161 : Polynomial.coeff recurrence5B1A3 161 = ((291955944290318127098 * 10 ^ 70 + 5394157582988855622576655271557070315286006780967944791681705673182163) * 10 ^ 70 + 2155776874800761886822490988114916381566872294069518533872914791708190) * 10 ^ 70 + 7210717800464807780054467317772783320179780284782782554613945236305634

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_162 : Polynomial.coeff recurrence5B1A3 162 = -(((216217083886216883956 * 10 ^ 70 + 5034357348527587712625015063895370320824540104877221235491540237977581) * 10 ^ 70 + 7937744945856398661413699810496564890192663608033861983540946264676217) * 10 ^ 70 + 3542625931512077386080401223916046287766088711136231573377420163436068)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_163 : Polynomial.coeff recurrence5B1A3 163 = ((154446369778793258927 * 10 ^ 70 + 7351373931789465024056698572353461199789165641295607711140300340663371) * 10 ^ 70 + 9661364819084474714079451408463582246125871637281584815493638487702544) * 10 ^ 70 + 4128200332183129480673074327376661343706200952583880133263502160094750

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_164 : Polynomial.coeff recurrence5B1A3 164 = -(((106366570454688563347 * 10 ^ 70 + 5698293929213996300484367426723104942838548204851772364971360518155550) * 10 ^ 70 + 8611268992181425359351051877689806279990144504931986894823843447029871) * 10 ^ 70 + 2657275583000049560639707240840007657154320103459100339923480282903700)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_165 : Polynomial.coeff recurrence5B1A3 165 = ((70534935404509769926 * 10 ^ 70 + 1749895733086566628265290315516218443315853930973680941365008424942930) * 10 ^ 70 + 6591945885417979450971907174119883696267035527681145180509881439739126) * 10 ^ 70 + 7858522256241062776196946741807583654141401222756148217125482908354514

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_166 : Polynomial.coeff recurrence5B1A3 166 = -(((44926210233912653911 * 10 ^ 70 + 9840661468183852006150807815696686400450959436286740302934304189149670) * 10 ^ 70 + 1761356867441426632938082420263056568648742595609678500997248977314923) * 10 ^ 70 + 2978077536204277768556638380230954868539603492017820171307715783823358)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_167 : Polynomial.coeff recurrence5B1A3 167 = ((27370428250093689509 * 10 ^ 70 + 1608651914686331557036879568458539328994735311846150107942992372518036) * 10 ^ 70 + 5517716327525965657831326146956438287036820955523847886240795651638580) * 10 ^ 70 + 1708666270000865775280294685576589071720191948405787102976616848461338

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_168 : Polynomial.coeff recurrence5B1A3 168 = -(((15840082331275603799 * 10 ^ 70 + 9872307400694260491256304426707859541706391688038259092766230497936479) * 10 ^ 70 + 5791372681228879572074905851629197423899096113612695289867901167511259) * 10 ^ 70 + 4324677928446408580524356779250480507413461374945374100575761443558926)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_169 : Polynomial.coeff recurrence5B1A3 169 = ((8606170082079437933 * 10 ^ 70 + 3456246498257957630862838972674033801129346905514590285625252801721087) * 10 ^ 70 + 3424233254357222853931394507379714640206859597058242116129871821507498) * 10 ^ 70 + 8278770303821290148331950985078398138426612705936625778236328639090094

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_170 : Polynomial.coeff recurrence5B1A3 170 = -(((4294696525852669412 * 10 ^ 70 + 3895683051944630971329282520832571340751774248176622833576294714129955) * 10 ^ 70 + 2653497232849493457378734232815736547587375924444993648268696293033913) * 10 ^ 70 + 5545311679296657711080613386354551622771113346173596901236924181578010)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_171 : Polynomial.coeff recurrence5B1A3 171 = ((1877253568224390693 * 10 ^ 70 + 7097489974733632601368165383952883373347652617317285196734059922877655) * 10 ^ 70 + 6872348725957690625088558456983313975924057031144519437389703915845077) * 10 ^ 70 + 3220309396611500067276999633931969818601457174919472165142423472239822

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_172 : Polynomial.coeff recurrence5B1A3 172 = -(((624962138034567365 * 10 ^ 70 + 6523496045510611751089839921680772869577669896601639291968178209937424) * 10 ^ 70 + 1617382231159466913269842933720140283829326233787704829345643731958339) * 10 ^ 70 + 3071194281482349709968690435120853787999462997791511720808929477595937)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_173 : Polynomial.coeff recurrence5B1A3 173 = ((47806583694716461 * 10 ^ 70 + 4101286304064084668604474230954252447940909047329276137574682303306118) * 10 ^ 70 + 9315906507721099002595145055740300672106861695265211850755028653904327) * 10 ^ 70 + 2545487616381492592279272223795313612136682069397858960694769597355316

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_174 : Polynomial.coeff recurrence5B1A3 174 = ((166231855393716302 * 10 ^ 70 + 4847061613652383040251795294299872242187071493992639217243177129583952) * 10 ^ 70 + 3792308684789185265201505496250395578258440316472453918879757538797872) * 10 ^ 70 + 32929638595729566087026585223128966917274080736213004137658785502095

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_175 : Polynomial.coeff recurrence5B1A3 175 = -(((204320984450881800 * 10 ^ 70 + 7512537374960658187825489096316496989314346642467256506512553697880710) * 10 ^ 70 + 4036886693725967690613692755660899955575118813424913126166268587833810) * 10 ^ 70 + 8864353592758423667910713477532379400877785382246912314225359597952425)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_176 : Polynomial.coeff recurrence5B1A3 176 = ((171025722892021524 * 10 ^ 70 + 4418287877948373971152407410066648837140512080349524326168787379866815) * 10 ^ 70 + 6999756914202845919743247017022644902005203839746671733566736299227582) * 10 ^ 70 + 389498369819292272338479136246812400741268079885464536826176516545971

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_177 : Polynomial.coeff recurrence5B1A3 177 = -(((119491122106760021 * 10 ^ 70 + 6640513418778050195603354980581318254690198505448474605337578363901212) * 10 ^ 70 + 3177375871659159030087392460376395903307638154094828498210695906143177) * 10 ^ 70 + 2739598967587491399846186603447433510405029246230593573474975820513458)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_178 : Polynomial.coeff recurrence5B1A3 178 = ((72994432450766246 * 10 ^ 70 + 8904225233977728789133613688292263713080568538560266850174750648321187) * 10 ^ 70 + 5373258735275803595441948130937862022713725271008014183668840894719760) * 10 ^ 70 + 6432493069213463487257484545887129531816407622891299580938006036084376

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_179 : Polynomial.coeff recurrence5B1A3 179 = -(((38915046181994298 * 10 ^ 70 + 1402521324058696133797529588269382942447737648972394433601727488937925) * 10 ^ 70 + 8922854938573624905768807965824657272043836119013347151476990088213290) * 10 ^ 70 + 7159561123992166917075321795065841284260228275541837103564814613097471)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_180 : Polynomial.coeff recurrence5B1A3 180 = ((17186329052556079 * 10 ^ 70 + 8182021616738886491312416010810247420382433759052379907703427578942976) * 10 ^ 70 + 1401741935189178577431366110690351700975185362388852135057204001960827) * 10 ^ 70 + 9195942560022634829991675123276423404097903297244974040805990456224379

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_181 : Polynomial.coeff recurrence5B1A3 181 = -(((5004230123704493 * 10 ^ 70 + 709285160979995156419520967892630457404284118640480321006067692240713) * 10 ^ 70 + 5169017695777774407697638103964894474880141041402397003499809131642179) * 10 ^ 70 + 2351210960488379455186457147570775557769851236925913272887524755494965)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_182 : Polynomial.coeff recurrence5B1A3 182 = -(((829851837774744 * 10 ^ 70 + 9741666212108834321057213380816392540075525918898340238650269807429474) * 10 ^ 70 + 5961694463209292250426915267926457719844974809419111689341784213302360) * 10 ^ 70 + 4593146947769372167375428600382945536833927555348874183818215131436595)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_183 : Polynomial.coeff recurrence5B1A3 183 = ((2946538079547601 * 10 ^ 70 + 8571534215730870232310464961064504973214675850090951616991956185971015) * 10 ^ 70 + 2985100818364682212738159700122739745880382183531244112036685069510034) * 10 ^ 70 + 5527011092804275071142197311768689933015754779663205909949488528567114