Recurrence 4 lookup certificate: Scalar2Left 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.recurrence4Scalar2Left_coeff_0 : Polynomial.coeff recurrence4Scalar2Left 0 = -127471115825187632452307041285142471049216

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_1 : Polynomial.coeff recurrence4Scalar2Left 1 = -4011287777375747889525563116007642725524910080

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_2 : Polynomial.coeff recurrence4Scalar2Left 2 = 28334011706938345927449892455348506877518871478272

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_3 : Polynomial.coeff recurrence4Scalar2Left 3 = -75630802208780268109721094093080497550916989135089920

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_4 : Polynomial.coeff recurrence4Scalar2Left 4 = 94787890866504242515279295282874591979474130167469907456

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_5 : Polynomial.coeff recurrence4Scalar2Left 5 = -31051920582379933833806066663955829847410340960780278197360

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_6 : Polynomial.coeff recurrence4Scalar2Left 6 = -67776221530991344021875761982119277564688026621567849821913720

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_7 : Polynomial.coeff recurrence4Scalar2Left 7 = 102304347298346249538311221130900816986823440125823092518720718960

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_8 : Polynomial.coeff recurrence4Scalar2Left 8 = -67194063918792685662737783584772845681391094933258357189361624294636

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_9 : Polynomial.coeff recurrence4Scalar2Left 9 = 2 * 10 ^ 70 + 9648442864474559438266783872790027333546290228212153356813488638542756

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_10 : Polynomial.coeff recurrence4Scalar2Left 10 = -(1423 * 10 ^ 70 + 9259984208895214042128940295111627849375819377242617750960343399814024)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_11 : Polynomial.coeff recurrence4Scalar2Left 11 = 674031 * 10 ^ 70 + 581304485347317387099952708724950069768683086450319455437158094490376

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_12 : Polynomial.coeff recurrence4Scalar2Left 12 = -(161559662 * 10 ^ 70 + 9552042877844065750738872019814393188081950396019973333460338309552400)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_13 : Polynomial.coeff recurrence4Scalar2Left 13 = -(39672410627 * 10 ^ 70 + 7615599190959447665933412673514209220750138246818455562178426581911596)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_14 : Polynomial.coeff recurrence4Scalar2Left 14 = 51257845862576 * 10 ^ 70 + 8377826215875843487505891526062998373564581956171102260020946054354768

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_15 : Polynomial.coeff recurrence4Scalar2Left 15 = -(26099663116032402 * 10 ^ 70 + 1502858717619982664727236924939331117025947661556589279414922984906568)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_16 : Polynomial.coeff recurrence4Scalar2Left 16 = 11144958915896891718 * 10 ^ 70 + 958892645422579138077265920450098006637737797702115676667477813492994

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_17 : Polynomial.coeff recurrence4Scalar2Left 17 = -(4370890525831241268216 * 10 ^ 70 + 8222065355369929179157830621831687092046099195241918405650086623733620)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_18 : Polynomial.coeff recurrence4Scalar2Left 18 = 1241820230962625091076560 * 10 ^ 70 + 8141638997689085444700369815948083168709228901164633106774764427573349

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_19 : Polynomial.coeff recurrence4Scalar2Left 19 = -(91034008276239700626494960 * 10 ^ 70 + 49974723408091175836496735671338190589591911745122474233313778291775)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_20 : Polynomial.coeff recurrence4Scalar2Left 20 = -(124340426828166323942689980865 * 10 ^ 70 + 4977243212922904439553506822894768734325076540465260952328134300693406)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_21 : Polynomial.coeff recurrence4Scalar2Left 21 = 79898907445031000840642898095322 * 10 ^ 70 + 1701685893348849204529165255009325486372851914109468510908519936690984

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_22 : Polynomial.coeff recurrence4Scalar2Left 22 = -(28905252793433204471271967560440964 * 10 ^ 70 + 1969238175942713719178633339829572539489101630060927636548779318932529)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_23 : Polynomial.coeff recurrence4Scalar2Left 23 = 7356234922660298507199385596096397593 * 10 ^ 70 + 2382081344417936805732602865410025352014499941247677958618175532085121

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_24 : Polynomial.coeff recurrence4Scalar2Left 24 = -(1303886409209882505005350278249406552131 * 10 ^ 70 + 4396326234895596387652222309791593204445535661041643748408895731571250)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_25 : Polynomial.coeff recurrence4Scalar2Left 25 = 97071983233125920632982164985796267326739 * 10 ^ 70 + 3931092016764537652425191725234001892976603629700565221935287878678269

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_26 : Polynomial.coeff recurrence4Scalar2Left 26 = 41148810992278701370684014544631831108704160 * 10 ^ 70 + 6727363433926234196944374078754695935815019806461452765617011812704319

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_27 : Polynomial.coeff recurrence4Scalar2Left 27 = -(25262272205198095247897385149651140959765386565 * 10 ^ 70 + 3040349337406841674299671366905712662060971010413602828573850626151161)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_28 : Polynomial.coeff recurrence4Scalar2Left 28 = 9005914526816815783203355969342176787092637587205 * 10 ^ 70 + 9075572529378644068291023612136747416891177748792989766631791132248909

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_29 : Polynomial.coeff recurrence4Scalar2Left 29 = -(2537308641182017784744572152799995047421667433251387 * 10 ^ 70 + 8981028089486620733481792562235888671944786167383351748226016105398300)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_30 : Polynomial.coeff recurrence4Scalar2Left 30 = 603562515222327963840277594685169553407484217143274353 * 10 ^ 70 + 7736353045568933365599083257702169207185186308769847467521851093303069

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_31 : Polynomial.coeff recurrence4Scalar2Left 31 = -(123817419619583759609597519860585689415472868050874138606 * 10 ^ 70 + 4878562555992567337773135403079899355176133191515881459324631971581189)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_32 : Polynomial.coeff recurrence4Scalar2Left 32 = 22050147475317731493710158495786860716375682820519883343657 * 10 ^ 70 + 8272970705158648691700191850024098513252843324545852039603118213345837

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_33 : Polynomial.coeff recurrence4Scalar2Left 33 = -(3402923859643917907377609157491216900417538774268581957380433 * 10 ^ 70 + 9280404131233200834147716758172786443141460104045318410738274072035894)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_34 : Polynomial.coeff recurrence4Scalar2Left 34 = 449857433875838971282778545928556834828882574625793021222686838 * 10 ^ 70 + 6950485049242012330813459377191232934596763922716635044926132418011021

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_35 : Polynomial.coeff recurrence4Scalar2Left 35 = -(49374253151591346324996879222659457903257972638594217297174798995 * 10 ^ 70 + 125834641441611741431819576349236622171764337116875667268733997623437)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_36 : Polynomial.coeff recurrence4Scalar2Left 36 = 4110727399433705882439304943428494017931531629871866626751170574691 * 10 ^ 70 + 8282262828515247883526078143513606672801538767530069637115475029193073

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_37 : Polynomial.coeff recurrence4Scalar2Left 37 = -(165428576986449962901700039759957175231443500402056219960219344454540 * 10 ^ 70 + 9136788235846231138574117833270052417911603811458340482431771720149016)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_38 : Polynomial.coeff recurrence4Scalar2Left 38 = -((2 * 10 ^ 70 + 2568663113482297816379502696960321307664238215183382941320853347331683) * 10 ^ 70 + 3019566076465230093843961798658260267666735421018529328210975716048015)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_39 : Polynomial.coeff recurrence4Scalar2Left 39 = (680 * 10 ^ 70 + 6193779925468254385975643507355514142911410888908966841534634175254992) * 10 ^ 70 + 1504172669142818949865774577003173864674739960183319156818708869511341

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_40 : Polynomial.coeff recurrence4Scalar2Left 40 = -((107432 * 10 ^ 70 + 466239045769447370109150022759829160612490970353627659620895411805476) * 10 ^ 70 + 6519989954596023800713929641002258585052260867552248810262428892157760)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_41 : Polynomial.coeff recurrence4Scalar2Left 41 = (12846234 * 10 ^ 70 + 4482036918481258330046683458690828538955404101840821667204279459640206) * 10 ^ 70 + 8369842088445867914860291516694133960566685079157512516080000763205990

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_42 : Polynomial.coeff recurrence4Scalar2Left 42 = -((1242214030 * 10 ^ 70 + 268734753471160810256266080156464116494797311231177080886840639570292) * 10 ^ 70 + 5724976758756262845956359597776552586612381855506065092381207374176838)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_43 : Polynomial.coeff recurrence4Scalar2Left 43 = (95867665703 * 10 ^ 70 + 8678962945931966795884869424738275190184678028441937734723175044607403) * 10 ^ 70 + 2152992922448835879162220044518542354700146146109112107960064712321781

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_44 : Polynomial.coeff recurrence4Scalar2Left 44 = -((5189693910657 * 10 ^ 70 + 8289050677532400687440077088356197161286623312899687482396375606508674) * 10 ^ 70 + 2535425849821785766638908889616178617177808655932111151008360493752159)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_45 : Polynomial.coeff recurrence4Scalar2Left 45 = (44306103007312 * 10 ^ 70 + 7799290459414930800808397495492325616454354876723067430863921283228034) * 10 ^ 70 + 3234515502168156450022576804499774146317806620269744960720391034096430

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_46 : Polynomial.coeff recurrence4Scalar2Left 46 = (35414304331445591 * 10 ^ 70 + 5476640261766934731214690428068334792787361208834201900031988698665214) * 10 ^ 70 + 2982924034170457717428205077203906731252271562471453325262498076084475

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_47 : Polynomial.coeff recurrence4Scalar2Left 47 = -((6090839925826557741 * 10 ^ 70 + 8030499160827078895069086707383779706105803398501352825242552619336862) * 10 ^ 70 + 7082438326572370476184371775004511678065194858470853561842220926379666)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_48 : Polynomial.coeff recurrence4Scalar2Left 48 = (707139799729792401072 * 10 ^ 70 + 9116225173921139373704013551871319032429290513495751669761522689966302) * 10 ^ 70 + 6200124127099086387799558698639840346940445810405910654771949285186562

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_49 : Polynomial.coeff recurrence4Scalar2Left 49 = -((67734958252993813527985 * 10 ^ 70 + 5348991229673209059267024411338398170436896031904421932800420552464270) * 10 ^ 70 + 9508809034752443628377368128431862907635108127603290839483944816815843)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_50 : Polynomial.coeff recurrence4Scalar2Left 50 = (5690793434313301367598691 * 10 ^ 70 + 4504136778965477628939469857491586948465704664877103225965239860723750) * 10 ^ 70 + 5184241133307778396751715489844800700486030005527786623108474826964860

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_51 : Polynomial.coeff recurrence4Scalar2Left 51 = -((431131362854304677208996370 * 10 ^ 70 + 519775262790521175143689145941487064654378131619521493856705277736779) * 10 ^ 70 + 6854133854484070932650582082673608725409583304980029468588439708675653)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_52 : Polynomial.coeff recurrence4Scalar2Left 52 = (29906863867243839986240757446 * 10 ^ 70 + 5347254779043115475551000547968233107448105797697320032322569017350082) * 10 ^ 70 + 2462591106904302510644765899333190987907919584849910971347998577210219

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_53 : Polynomial.coeff recurrence4Scalar2Left 53 = -((1917874575742775415377581014009 * 10 ^ 70 + 3147835025495337820209236597380085603101034649496080039489596327194578) * 10 ^ 70 + 2056169059121160957699180799765501609885385758916253207935900201803179)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_54 : Polynomial.coeff recurrence4Scalar2Left 54 = (114445292974590483979316725546876 * 10 ^ 70 + 1920502175581175794903574946557529319559277570361889020936523145696183) * 10 ^ 70 + 2893301687822865618065323907467731544478299558287524302293986701352351

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_55 : Polynomial.coeff recurrence4Scalar2Left 55 = -((6385049195718394969251400924123849 * 10 ^ 70 + 887184471287043240652038567485331015832875026504144830645043483441488) * 10 ^ 70 + 2879701227710833525572363557882031166110014808322665759037665037021512)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_56 : Polynomial.coeff recurrence4Scalar2Left 56 = (334258236692572019299040636650497249 * 10 ^ 70 + 6591005703888871253125567186026518718353913947129066110678163665849995) * 10 ^ 70 + 8438059673289864499114574445532857732673998083209178551739430020734484

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_57 : Polynomial.coeff recurrence4Scalar2Left 57 = -((16465571304902050102914474915265233708 * 10 ^ 70 + 8715155192118156909020618867876478745499772853315928958977583981621494) * 10 ^ 70 + 9553661822818319552586531367611674217648012036481831841639392685007732)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_58 : Polynomial.coeff recurrence4Scalar2Left 58 = (764946505421988680742659982152060323838 * 10 ^ 70 + 5503345732903235283738839057419394305267461655198382240297096783860779) * 10 ^ 70 + 5606815596821921777815637880952246744449220872084342602895199570120632

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_59 : Polynomial.coeff recurrence4Scalar2Left 59 = -((33577187869343965821485586534901868961735 * 10 ^ 70 + 4811775196380337137070087587382409662942903573452791875612486710791222) * 10 ^ 70 + 1450084233020131282875120408550446065458232732766618142578619681300222)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_60 : Polynomial.coeff recurrence4Scalar2Left 60 = (1394665828269289379653343442954617471117548 * 10 ^ 70 + 6357290465927037595448799696075617733263273168394890487755913377926213) * 10 ^ 70 + 3297585293568725233607171068084307698963877089141482261483949451081743

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_61 : Polynomial.coeff recurrence4Scalar2Left 61 = -((54883262492731551313231587249795758899531623 * 10 ^ 70 + 8738968331213913567889342434104914254888435224871186907475164594276409) * 10 ^ 70 + 1698300947234122298513148615638549613214303870743130201719457971634924)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_62 : Polynomial.coeff recurrence4Scalar2Left 62 = (2048219759157736260968817657524298266772227188 * 10 ^ 70 + 3130244685353673970701173925200568709270130680561701121946633507969617) * 10 ^ 70 + 5038847016014846447573300795814684623519153165125058501203906497916672

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_63 : Polynomial.coeff recurrence4Scalar2Left 63 = -((72543913268071684758729822390641690936796417765 * 10 ^ 70 + 3817380150287380288293052056233596166024137756883965915157284446975953) * 10 ^ 70 + 9941870353879462865932551357810498397940415636903141046446921655004739)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_64 : Polynomial.coeff recurrence4Scalar2Left 64 = (2439674106525211978404246556138789866204571347436 * 10 ^ 70 + 6529285846236082228315879099973159117426110506963554041306337521704740) * 10 ^ 70 + 8054290211381522917257675841123206986184149341073848983407940503465845

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_65 : Polynomial.coeff recurrence4Scalar2Left 65 = -((77925255789443283630190610766607318964643835628712 * 10 ^ 70 + 8017574595094827210448899175666015152907363413837734405931399882396974) * 10 ^ 70 + 2339168830384730399517785503793968898143950830083801551712810552396953)