Recurrence 5 lookup certificate: B2A2 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.recurrence5B2A2_coeff_146 : Polynomial.coeff recurrence5B2A2 146 = ((3591596324312756766014 * 10 ^ 70 + 4040376560735570720867773571368750322333262527716744379067261694653482) * 10 ^ 70 + 3258040744267560152720467915320841478729311631948401928549929998648730) * 10 ^ 70 + 8352861406807196028159852346759307484479628827354033968954645461815421

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A2_coeff_147 : Polynomial.coeff recurrence5B2A2 147 = -(((2976897632809606240132 * 10 ^ 70 + 5347532689148525443152600992484780605861781908802198523533177498895330) * 10 ^ 70 + 1854806747242625596353092525376519385016898242320355434935817299793055) * 10 ^ 70 + 2542939823145142758112408540689145851845244181974669817167478305076900)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A2_coeff_148 : Polynomial.coeff recurrence5B2A2 148 = ((2333363575436472881344 * 10 ^ 70 + 7248886750756025674974447482257823287187886519592626998161473476458333) * 10 ^ 70 + 8763687822650354514655299691958916373198050420862542375465970343789243) * 10 ^ 70 + 8929806468044289604112965516601955029037652314534485245464544817083190

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A2_coeff_149 : Polynomial.coeff recurrence5B2A2 149 = -(((1702369735843100328819 * 10 ^ 70 + 8938399208837083044237416419449143486116281222198462622070606108627544) * 10 ^ 70 + 1442458972028945680735561943900420087874276231999214524437817802731617) * 10 ^ 70 + 7623452825201469436867030027871288458526781838050905736854589952261586)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A2_coeff_150 : Polynomial.coeff recurrence5B2A2 150 = ((1120205978617354865055 * 10 ^ 70 + 7205551863525398313669657954453881105198622338771895535223713110145424) * 10 ^ 70 + 587859612215546572645893451998179657689328183241176079012748556798330) * 10 ^ 70 + 5554351705810825839628577248197415802613480129947189184388130024201587

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A2_coeff_151 : Polynomial.coeff recurrence5B2A2 151 = -(((614724961590036773893 * 10 ^ 70 + 4858907215171443462678117622922919022309404884990172923082465225254890) * 10 ^ 70 + 4286434456042557528062168015841477425832548937740154294848620016342922) * 10 ^ 70 + 3319671051182130678419953747062930765108212401691598853953263257307855)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A2_coeff_152 : Polynomial.coeff recurrence5B2A2 152 = ((203423427948641339611 * 10 ^ 70 + 4846699892790703296072636103106646747034786800654955959490186947405595) * 10 ^ 70 + 7772548622651077626256065019943158445403710560016769344587617101958355) * 10 ^ 70 + 4793445654900009976969895352316762271019319472437625206238401530792477

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A2_coeff_153 : Polynomial.coeff recurrence5B2A2 153 = ((106916740874087138284 * 10 ^ 70 + 8728449468987132230796677316150168044348594645098691347887280252765810) * 10 ^ 70 + 2695212899421183243835266802766367996830942485552814991697818755744569) * 10 ^ 70 + 2389280874682832557526639142355400706118508727620632627648330949579272

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A2_coeff_154 : Polynomial.coeff recurrence5B2A2 154 = -(((319180814988951032940 * 10 ^ 70 + 7139483950883486093946697273201226582385715550918375721562125701562833) * 10 ^ 70 + 9432058912205207155929798378997018509600007527872567655980731218763927) * 10 ^ 70 + 5915493606111716376112423116462073543094678443311671346551531025279636)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A2_coeff_155 : Polynomial.coeff recurrence5B2A2 155 = ((443835607760286379353 * 10 ^ 70 + 3255577612137270691723482445577916124784484461555541802416719309299779) * 10 ^ 70 + 5475199822615975702849007922029897008422651819494935504183470087324636) * 10 ^ 70 + 5355870920887538753968076582009803705470333757148607272218192964829888

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A2_coeff_156 : Polynomial.coeff recurrence5B2A2 156 = -(((496289325986925371153 * 10 ^ 70 + 2406887386945921969699454218077121942575912541178688476807691511206535) * 10 ^ 70 + 7368781512162656944459258347636554485887900243110472360928946981156170) * 10 ^ 70 + 841391814757611945258342772540487825563705749013703471843652980907548)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A2_coeff_157 : Polynomial.coeff recurrence5B2A2 157 = ((494185506442994629755 * 10 ^ 70 + 8659566131484884911302803552111907765361502167995776367199147985905253) * 10 ^ 70 + 7800422086251875477695330030300822776260447121384097484238545462522409) * 10 ^ 70 + 5012279877021849623297375508992867034890796247984855815479569113338257

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A2_coeff_158 : Polynomial.coeff recurrence5B2A2 158 = -(((455033515804669783579 * 10 ^ 70 + 7183556757501894620164372686845690787668597051315902796917167813264350) * 10 ^ 70 + 6194236197160930653406936581439914222073846553670683158862041731261618) * 10 ^ 70 + 4371085466358887112868652212336171878188163639683461422689533997288283)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A2_coeff_159 : Polynomial.coeff recurrence5B2A2 159 = ((394435761426198247513 * 10 ^ 70 + 7870557805241407580478963796466495257182401862768984275041302695594399) * 10 ^ 70 + 6592724683453551330275685353907779681011818300290849114000050095944586) * 10 ^ 70 + 2930806125968883810158563437817524328806360067554706245661700817326041

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A2_coeff_160 : Polynomial.coeff recurrence5B2A2 160 = -(((325013976676649978936 * 10 ^ 70 + 9328552902035089899267093390491098446681601410609607434300391261098746) * 10 ^ 70 + 2307550064557033089812008066220120817099037026644937542407500855639140) * 10 ^ 70 + 6976174168685999479369516052964533868559637725336293437822781240027425)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A2_coeff_161 : Polynomial.coeff recurrence5B2A2 161 = ((255998934252720810493 * 10 ^ 70 + 7340291524357882808987860764045198226683568439434499741520271817178962) * 10 ^ 70 + 7057112952731256780148089129738635099713747339216235235883221734765937) * 10 ^ 70 + 5147635101209892545473229698237061476629097765734259344716211314685252

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A2_coeff_162 : Polynomial.coeff recurrence5B2A2 162 = -(((193352235388629309161 * 10 ^ 70 + 9863878040867134030166712873195903058757695525314818888786946457645627) * 10 ^ 70 + 7453621496806989815991039965796304332312226076692307810224428976563479) * 10 ^ 70 + 7942231519686947395305952159630521359278411080757240618565349464856376)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A2_coeff_163 : Polynomial.coeff recurrence5B2A2 163 = ((140243002570872955636 * 10 ^ 70 + 8304602565835728855462799638213522475849905871061343473861386258185817) * 10 ^ 70 + 3008224687487079422258462099151097249861850431242835088597230298568131) * 10 ^ 70 + 3713347654800730904602011045515816465352918131891231856371957529735445

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A2_coeff_164 : Polynomial.coeff recurrence5B2A2 164 = -(((97701128723464085648 * 10 ^ 70 + 378976790890794062598247967965980020306854851197334689409645972136450) * 10 ^ 70 + 1351073579216086177631442296782996148065020550928162750085696715978491) * 10 ^ 70 + 9634599125043962197488657466693469567340876456076664247274194819891512)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A2_coeff_165 : Polynomial.coeff recurrence5B2A2 165 = ((65298957117513882171 * 10 ^ 70 + 1583549850105939130717010595819981366060840039049660101848628364796179) * 10 ^ 70 + 8033221725155455134153462112957927867308344139920773512821492195896611) * 10 ^ 70 + 3262273983908145310562860097389935565464050542928530448788851198717818

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A2_coeff_166 : Polynomial.coeff recurrence5B2A2 166 = -(((41759073492091197153 * 10 ^ 70 + 4930691772877531746072851538083892500208912217628862364524674269330674) * 10 ^ 70 + 7309977471261715650641885447005235782800905888929883025706166854480750) * 10 ^ 70 + 212594069095616216415646459421932622317460252758515417347715170259181)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A2_coeff_167 : Polynomial.coeff recurrence5B2A2 167 = ((25433351661792369707 * 10 ^ 70 + 5777028589528130812801613232066713084550309866338639937593164424541986) * 10 ^ 70 + 8917737711551513081427901140695271635397230342010209438268017673134682) * 10 ^ 70 + 2515872520200553145605767997936556983184542603587514496348591513994883

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A2_coeff_168 : Polynomial.coeff recurrence5B2A2 168 = -(((14638000150510368401 * 10 ^ 70 + 7192277988057286262615001520229604859951807502115176746385206043570200) * 10 ^ 70 + 6486045493198759788211934303906502288326322736678718827808741644917170) * 10 ^ 70 + 2621281500536424054105288656497891948730311858367665883566348292808208)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A2_coeff_169 : Polynomial.coeff recurrence5B2A2 169 = ((7856633288990164886 * 10 ^ 70 + 4590561873265525211476185649576363143248679386149831775666809819930629) * 10 ^ 70 + 763559454220303507896326754626391567948636674835117167217838791498744) * 10 ^ 70 + 7608743358247912537104522957355971156371853960303593199886001060750692

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A2_coeff_170 : Polynomial.coeff recurrence5B2A2 170 = -(((3838050374219387879 * 10 ^ 70 + 2401656408374867132737323933073069950872614207606617463496985745433836) * 10 ^ 70 + 4287356229324788115175092944458094867467840103640338929280982246324863) * 10 ^ 70 + 3784778621921446366986195134199495701884694776098708522615808499901349)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A2_coeff_171 : Polynomial.coeff recurrence5B2A2 171 = ((1619816665640600361 * 10 ^ 70 + 1827229941673496458934083502184303169494550601086295508993852275587362) * 10 ^ 70 + 8395307324962961740240842357891305615755055710596295806661819225263242) * 10 ^ 70 + 4810480928164136237101522532859404224289509449513249080237824950928964

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A2_coeff_172 : Polynomial.coeff recurrence5B2A2 172 = -(((506339502030775564 * 10 ^ 70 + 7363558205397575483086702183545179491052459384270340942059918908993505) * 10 ^ 70 + 6754479502387743453518231418222582016595727771204174985936581623396956) * 10 ^ 70 + 5685836653754310117384874503541629434693983164880503485248622025590664)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A2_coeff_173 : Polynomial.coeff recurrence5B2A2 173 = ((24242150011063393 * 10 ^ 70 + 7860565079570908682825845762313882657896513363472279805410454934466452) * 10 ^ 70 + 9645800449236367323750932819581454976129676719933001081988789736778128) * 10 ^ 70 + 6171228773687133093578854490018269804604432544900802861551550497463825

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A2_coeff_174 : Polynomial.coeff recurrence5B2A2 174 = ((129000696157789916 * 10 ^ 70 + 7251999923833599063791176977424745853727689325415795501088196516727641) * 10 ^ 70 + 4143534164023998778027883556529039410112798695774302207738400177253703) * 10 ^ 70 + 6921835405394052488248278589456592413035766064507300758092944948121

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A2_coeff_175 : Polynomial.coeff recurrence5B2A2 175 = -(((133411832606396734 * 10 ^ 70 + 5818974834347964322921720454466062756569274436462876539741508296216569) * 10 ^ 70 + 4062942704520857218145037501223041057859715524979363580349201712133697) * 10 ^ 70 + 1443858504220927873035847974715394466492981496083833771972601788416263)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A2_coeff_176 : Polynomial.coeff recurrence5B2A2 176 = ((86939724070130767 * 10 ^ 70 + 9537874001956178670580579011041262343911851607991560454335161010609220) * 10 ^ 70 + 4356731416996879568624959260168763732173251299939927319446251446168394) * 10 ^ 70 + 1356513814921215830537530767295183565614782821126590931476778811677996

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A2_coeff_177 : Polynomial.coeff recurrence5B2A2 177 = -(((36404753850754231 * 10 ^ 70 + 6296176473907956995902632119608420379081691932587561730124747466063706) * 10 ^ 70 + 2155083661198782808973167650839545630161988788714471148953832578737473) * 10 ^ 70 + 478487217186732772737766264642691349465064293599603489418715284410236)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A2_coeff_178 : Polynomial.coeff recurrence5B2A2 178 = -(((573739488851276 * 10 ^ 70 + 1955369492499241870375539217516130906317264485705062093808365576506654) * 10 ^ 70 + 3537294869581412385041387938311484210268918401558858278046047580375318) * 10 ^ 70 + 47402044938319913597300446774184341559405716821562636669808279255253)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A2_coeff_179 : Polynomial.coeff recurrence5B2A2 179 = ((21189074156527968 * 10 ^ 70 + 3027785459758880702416015308714428436310732458959970182637023268087668) * 10 ^ 70 + 7733294849704675367879354084862914211731010294133249487511709142383139) * 10 ^ 70 + 6657138866102087300905512632112123617260693830064383689720985673115116

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A2_coeff_180 : Polynomial.coeff recurrence5B2A2 180 = -(((28783548678042409 * 10 ^ 70 + 8645126903986901549324715976100422732825811074889976388430520429500832) * 10 ^ 70 + 1239177078391137852321040423792885892365454947625215713685132023522424) * 10 ^ 70 + 8710704398736568214187356964154483320738033737790459779533335087980200)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A2_coeff_181 : Polynomial.coeff recurrence5B2A2 181 = ((28175468336039417 * 10 ^ 70 + 408821779424850221945510476760599950775069196504681172392536752226617) * 10 ^ 70 + 2231133232727621259486568996483081311897908701647848048346731268191499) * 10 ^ 70 + 8019992642458285251271193286188107763846452368548341257471909802638776

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A2_coeff_182 : Polynomial.coeff recurrence5B2A2 182 = -(((23532590006915416 * 10 ^ 70 + 8282622254370351190543361001254327820514600665018060174303627043451058) * 10 ^ 70 + 6047276516296380146577580932037938235815422981889535339910598080748964) * 10 ^ 70 + 2385447735412950674031005017202770291631707285517572494423386187879712)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A2_coeff_183 : Polynomial.coeff recurrence5B2A2 183 = ((17708112997518063 * 10 ^ 70 + 2521992783973019469747697419699115583717258394828711110367235403522402) * 10 ^ 70 + 8139779473110882491554123235147770139244791773797619154794278978238139) * 10 ^ 70 + 3162710159654397279133251286290084332721843438598991900399485901444982