Recurrence 4 lookup certificate: B2A4 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.recurrence4B2A4_coeff_139 : Polynomial.coeff recurrence4B2A4 139 = (25143326365376079373133083652924286566644547333640069213531 * 10 ^ 70 + 5997789601324738869118282014380627311911911931452675005586935229609007) * 10 ^ 70 + 5247585992260720748081659815886978770398366805965568649532931341556150

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_140 : Polynomial.coeff recurrence4B2A4 140 = -((47560466995939877669627706875651350395941879171212515012521 * 10 ^ 70 + 9562730225131497568338422600165489972593452508389697099785116760157999) * 10 ^ 70 + 7054625170795351126159715137750010009140536018441702933651416184711114)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_141 : Polynomial.coeff recurrence4B2A4 141 = (88164941019430185844945323950269775091737885238863153358648 * 10 ^ 70 + 3902925381739374818210348153000025936389359126172436130474984903782726) * 10 ^ 70 + 399514691572935273509675677592318317109543333590242166063704362408468

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_142 : Polynomial.coeff recurrence4B2A4 142 = -((160170735789727240422378467502911117843047321657103809224233 * 10 ^ 70 + 8699929831500696969853063355481485609715800258468886301333911383042990) * 10 ^ 70 + 2321230435034409499507056908795524999718403585227537526797766312746713)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_143 : Polynomial.coeff recurrence4B2A4 143 = (285178586702033509980197562949148841200435360123118517246668 * 10 ^ 70 + 6025564667315682937865906881230490950368006891190831097500141135354066) * 10 ^ 70 + 205308030943432161978906936990991437333949614529561686540619742527055

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_144 : Polynomial.coeff recurrence4B2A4 144 = -((497627278010161700922659460322267614193840093635205077969138 * 10 ^ 70 + 1501786869150737832526782077612037503681320473255920666593670931574035) * 10 ^ 70 + 9598776070769253599506793549212640859324531845490770665006047073066010)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_145 : Polynomial.coeff recurrence4B2A4 145 = (851039848533294426330675292399530811144880529556322250042016 * 10 ^ 70 + 1027977553426737783262041827745557033654799005956585132569887351360211) * 10 ^ 70 + 2308505189704012921551902001638191045377835662727824269276353418144187

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_146 : Polynomial.coeff recurrence4B2A4 146 = -((1426450761250305675407924058605105841847248835705755984822100 * 10 ^ 70 + 1563565969250746138171406872047789289311479108256254670011812970125777) * 10 ^ 70 + 8798767958202295374056571406791439097964246670757789153431250611484133)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_147 : Polynomial.coeff recurrence4B2A4 147 = (2343285737022045514166672683945430000702097105618734182202273 * 10 ^ 70 + 7322933102623084638266277690318410377480965673728346624073109346188444) * 10 ^ 70 + 2696594357847158096910492874292841634859578724428083098990579688431901

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_148 : Polynomial.coeff recurrence4B2A4 148 = -((3772708369956303675317507232269020336278330474185301859960923 * 10 ^ 70 + 2838592230007803997697273042811918425105551415581868625629462005990320) * 10 ^ 70 + 8960100502784126973482778154377521248871649545120090238287247998437894)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_149 : Polynomial.coeff recurrence4B2A4 149 = (5953002725156784054194142780133308905527238983446138543405913 * 10 ^ 70 + 491506324085862318251835129897854442297354190763758003126603320457233) * 10 ^ 70 + 1658564294198052854290298296685034384613951317952786290953469251681144

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_150 : Polynomial.coeff recurrence4B2A4 150 = -((9205901608195178835581567749136244280566848933439600303642774 * 10 ^ 70 + 9046967215191629402059059990130986967517172995750177208464543012648796) * 10 ^ 70 + 3961629790126811705760581586490325531229112575002638090161610341597782)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_151 : Polynomial.coeff recurrence4B2A4 151 = (13951905048524574240479570903906414735879903095300520089999072 * 10 ^ 70 + 8996164497223857734268586587416359789771461077846010092278990069108075) * 10 ^ 70 + 540623261765501158727337601215636347587445072044759696938381014754203

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_152 : Polynomial.coeff recurrence4B2A4 152 = -((20721629529940121025298832012816615347926792826056688173938705 * 10 ^ 70 + 5898354736302834800903254256307344453179900344065327668950851358824925) * 10 ^ 70 + 8587832852990059065801756637930538341181304868296696892335316496324530)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_153 : Polynomial.coeff recurrence4B2A4 153 = (30159228537432348139858670871019634871320970383381839947960677 * 10 ^ 70 + 6540459079571930176559088258433858320209659157687282340282833307383721) * 10 ^ 70 + 4288295466328381395677988584849635963080946859840423122510385869809377

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_154 : Polynomial.coeff recurrence4B2A4 154 = -((43013155225622266392021337867178541951306258308381604848732714 * 10 ^ 70 + 3705429798998618719341578928436103623388724464924915044928411666112165) * 10 ^ 70 + 3465119931478399431330389026264054997111052683594111763751032373733172)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_155 : Polynomial.coeff recurrence4B2A4 155 = (60109294760996304980989818254405032387628381837193479259705195 * 10 ^ 70 + 736573340574946432062593964150860448805199178494105625605571584372855) * 10 ^ 70 + 1746207234186098757184441960988896049485801548017319865910010282592186

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_156 : Polynomial.coeff recurrence4B2A4 156 = -((82302102861430699006081078648452958633182422690293791803186356 * 10 ^ 70 + 6676597264221156335747193601544652077736197693490334230376878645517071) * 10 ^ 70 + 1013426748671526185607013700365561331564185306753955560534988065672458)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_157 : Polynomial.coeff recurrence4B2A4 157 = (110401132554371337153730185680700375947114842405683820635377121 * 10 ^ 70 + 5651622911184726308513356841584488054353586603702464629267650116023838) * 10 ^ 70 + 8617662982362189277376271514864014099948336142054750493230309753383093

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_158 : Polynomial.coeff recurrence4B2A4 158 = -((145073361501515670892361714204087618224184851799045697465733878 * 10 ^ 70 + 6329124877852822464424398454352337815108704291104932932956060196739515) * 10 ^ 70 + 3002035092914804835124570265287524719722286116233696143015316564855071)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_159 : Polynomial.coeff recurrence4B2A4 159 = (186725958534951244343967214734610509381150448563787123476767083 * 10 ^ 70 + 6896201313013864074479630754344369484425448387396588682319490062869253) * 10 ^ 70 + 1354249110005469263113572414565827884927427152124867382094005624196494

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_160 : Polynomial.coeff recurrence4B2A4 160 = -((235379144060368009688360029379838234420351633908820113998627991 * 10 ^ 70 + 3417379885386668200853658104508398782355204205913094488872256169193464) * 10 ^ 70 + 5283855908321870067206039983780258644571413075865120328631527985145243)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_161 : Polynomial.coeff recurrence4B2A4 161 = (290543854794216278047215969986385048854138075826594542827867948 * 10 ^ 70 + 8775535827494131042083368783672221246315779014347326883210761693463385) * 10 ^ 70 + 9918545837663643460775001169336990406229428326429355043969543803063257

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_162 : Polynomial.coeff recurrence4B2A4 162 = -((351122982871747124586778520294796489612423265098884664379243970 * 10 ^ 70 + 9955451758501871807074143941039843428882218154529478146679082816792357) * 10 ^ 70 + 6910451823471141354012817489304217481526207547125000356119251719840944)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_163 : Polynomial.coeff recurrence4B2A4 163 = (415356857001269507943319008516943295121443342536189294858030042 * 10 ^ 70 + 4416391861482697275401507071164372623640571478309482943145363714261467) * 10 ^ 70 + 1794213943747355315680038773524508488569831386035262497691426011693922

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_164 : Polynomial.coeff recurrence4B2A4 164 = -((480832319020258227632242316525812416987897688724429940201105021 * 10 ^ 70 + 8420546782301986367340174583007741369671324574720678501110024307871915) * 10 ^ 70 + 5068875719386612557745161012628895035252729344676941932255734603263170)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_165 : Polynomial.coeff recurrence4B2A4 165 = (544569581616506495806860385506355723589624158967926164684532164 * 10 ^ 70 + 7494175810508101038193025624827644021991480364169069912722821043129057) * 10 ^ 70 + 1701954441430940408184361232501299858017669114459498327533161658694647

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_166 : Polynomial.coeff recurrence4B2A4 166 = -((603192071379230993010384192626139100196711244756550060904845507 * 10 ^ 70 + 4729488247368702670277814228261186525247741077667842192804115420847360) * 10 ^ 70 + 313316887038195008297674386168652903468481691412702555145510392149588)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_167 : Polynomial.coeff recurrence4B2A4 167 = (653172553348387704733190475475227725841977255102329798743244907 * 10 ^ 70 + 28085554691898025408798434136251432826384205803208604297616246259043) * 10 ^ 70 + 9019443595383706768284267621842933157791543132855071520999213536657742

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_168 : Polynomial.coeff recurrence4B2A4 168 = -((691135724178506330741877323901965094072848857728052015930773882 * 10 ^ 70 + 6809120931601924761243616134638482248926314192397254565637658203093493) * 10 ^ 70 + 1155378644116172189162987606347259351292013101059970350492284166883168)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_169 : Polynomial.coeff recurrence4B2A4 169 = (714185485428596330579561350144391694183892163730427850106895594 * 10 ^ 70 + 8157009256219184576750504613101017683018271209543698568074147724051995) * 10 ^ 70 + 9767897311788683762875279462137837699362923646399446686355373541476937

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_170 : Polynomial.coeff recurrence4B2A4 170 = -((720216779307142453974013667871319435420786027098446765039556533 * 10 ^ 70 + 4124108011370380475916993492504852796999846071452817423499180927884351) * 10 ^ 70 + 8586818148965289106453879539832983338533547352531291960618166372416121)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_171 : Polynomial.coeff recurrence4B2A4 171 = (708169323490569380092471736143799798408935569628802785410512049 * 10 ^ 70 + 6222817138888740054994624837539572511718379842171093823515788181913499) * 10 ^ 70 + 1641909499110729393065402260584379844529228733475229471102539615994580

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_172 : Polynomial.coeff recurrence4B2A4 172 = -((678185031195948862328508142565550454081497170480401730773673643 * 10 ^ 70 + 3095139892440717601483719676714005233005994837834578178611698931630565) * 10 ^ 70 + 4503173021371764149330693184335863697218784613669505122432512939326698)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_173 : Polynomial.coeff recurrence4B2A4 173 = (631642238076300589384230356095553487932896271591922538891116881 * 10 ^ 70 + 8431757013975045751911971424905040828075315755330615311682395594289137) * 10 ^ 70 + 347379705309033390325686812770830829878228017671163027379809419963511

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_174 : Polynomial.coeff recurrence4B2A4 174 = -((571056530742305150495611114774837472678218370467861636235997267 * 10 ^ 70 + 6972249276436443028509162999993536718848110411775644287377404348958277) * 10 ^ 70 + 2287317844374041514334766510856465843873961328129140664571833644286249)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_175 : Polynomial.coeff recurrence4B2A4 175 = (499857219283767942381786187008882116693841876493668371914245942 * 10 ^ 70 + 1108784267385709580039135163073171375512507515992849458314724657794459) * 10 ^ 70 + 7964256814988050242987086263301067769635357539487569153663810559726789

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_176 : Polynomial.coeff recurrence4B2A4 176 = -((422066874387980961932284356684014569125399358640555090883263904 * 10 ^ 70 + 2931789418530576405176010079255669699616469284301664919969934533045227) * 10 ^ 70 + 5420236794323529275528902989218679105651098302006161852957142960997017)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_177 : Polynomial.coeff recurrence4B2A4 177 = (341925465212552607628249689881935350831059051589594714514141184 * 10 ^ 70 + 8483328045124382731863230571993046119455741466923419101932891215146303) * 10 ^ 70 + 4775811008361785483000961142668924537782472609883546978040957976632010

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_178 : Polynomial.coeff recurrence4B2A4 178 = -((263507891459384560505336643494481597275850179095785993057898373 * 10 ^ 70 + 3518210275114658104820440343103546210918078313656466195860166251720914) * 10 ^ 70 + 1359594484811354258077570923991890066947002911991461082121307754728139)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_179 : Polynomial.coeff recurrence4B2A4 179 = (190382877962047630219587560755610674696847478849103471985389916 * 10 ^ 70 + 298649322331734620269704155733266924680249637550573201466100400162244) * 10 ^ 70 + 9075268528570396587979561554199605598869857759699024333809052540900867

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_180 : Polynomial.coeff recurrence4B2A4 180 = -((125352692406901912519467893030347059233224460205533125268119891 * 10 ^ 70 + 9439833033117540684555264873879726809511130817531201517365887315685404) * 10 ^ 70 + 7584140674884761855456981334484897368811370977225296755333081492175629)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_181 : Polynomial.coeff recurrence4B2A4 181 = (70298850249939519894158561569510983215621688946073547362296485 * 10 ^ 70 + 8726298463758404092055246882175184899900168763347189970437466684559837) * 10 ^ 70 + 5146611720249541805917279562332194362841172063396792530443902009208439

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_182 : Polynomial.coeff recurrence4B2A4 182 = -((26141801770431118103373782779271511448877150390996266013949300 * 10 ^ 70 + 9022713230472973344572029923244723782414788899609724479058292299370243) * 10 ^ 70 + 5380916250235910898263292032977962819568355233870355634780385852081420)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_183 : Polynomial.coeff recurrence4B2A4 183 = -((7094187814103072961371433473982792608714439058687004175341214 * 10 ^ 70 + 4860849103275702396280328370712098787016045785784679035345542589584939) * 10 ^ 70 + 5367650380130815208961473111489764320712691105670030322282149497055329)