Recurrence 4 lookup certificate: Scalar1Exceptional 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.recurrence4Scalar1Exceptional_coeff_316 :
Polynomial.coeff recurrence4Scalar1Exceptional 316 = (((23082723850639689437 * 10 ^ 70 + 8466517378319343115617727489841064795286428367814046848720699403031543) * 10 ^ 70 + 498633573177708568097222144650713454258242720651983465475561670674913) * 10 ^ 70 + 6154295743554251819565310886178013881530132500343420908748497944341987) * 10 ^ 70 + 3447935242349569314072407606188538038720858311800189840840638845044226
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_317 :
Polynomial.coeff recurrence4Scalar1Exceptional 317 = -((((13690065170089101436 * 10 ^ 70 + 9587330912313066577706307830606806724583824971803313753209873611219327) * 10 ^ 70 + 364783737919711710083745705389508424625460470312256770142815861190922) * 10 ^ 70 + 8542365203559306704040498708883919987788628050823840680158924096704854) * 10 ^ 70 + 5604051064813765079945898108713717115700833081367747126301088472825845)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_318 :
Polynomial.coeff recurrence4Scalar1Exceptional 318 = (((7967879427533889931 * 10 ^ 70 + 7089179331631790113133118721871533462905879394093602964185251000091950) * 10 ^ 70 + 420509298178286945974415375606305058455983150868371723647633319820339) * 10 ^ 70 + 1048295067399009928424571391292123115258603919634227269125525116598423) * 10 ^ 70 + 295718864742276399545394466083462400082398677896422305696892891212509
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_319 :
Polynomial.coeff recurrence4Scalar1Exceptional 319 = -((((4550392070168036549 * 10 ^ 70 + 5390894950460536124012233292981214075320729966316359750554867493308157) * 10 ^ 70 + 8503019642647439104165239211579682214746078956410303590098248828407265) * 10 ^ 70 + 4716725063321841869749518993497022852675323097711389582047327475455253) * 10 ^ 70 + 4423530055089197572733634218171818436013687274048144417129562546887613)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_320 :
Polynomial.coeff recurrence4Scalar1Exceptional 320 = (((2549859712001211970 * 10 ^ 70 + 2790344366645613191162198896347959200097765367680896912143143963717957) * 10 ^ 70 + 9513280757318747186566832081527723029959591276277983538526768168542961) * 10 ^ 70 + 6218342555934090992989182702897586505284321450359014996147962081104411) * 10 ^ 70 + 8566376736030420138754909210051843022087854462722779171372991284826682
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_321 :
Polynomial.coeff recurrence4Scalar1Exceptional 321 = -((((1402039320863081697 * 10 ^ 70 + 8201422247783862671809552600905796518744010485908605167994409674311824) * 10 ^ 70 + 6550842683027396320113299610256408611256359572118043256101572059534640) * 10 ^ 70 + 7408554967714064980467372139181188357688880679412354621107669776466851) * 10 ^ 70 + 338641076197165185364542692449965010486920933400220143506804050782590)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_322 :
Polynomial.coeff recurrence4Scalar1Exceptional 322 = (((756493178164995312 * 10 ^ 70 + 240461291682798059014608753383163734720596141721332943739081451936563) * 10 ^ 70 + 908907979151786103075187657399023476252197839038219413412353367166447) * 10 ^ 70 + 661924664176812691935052287315346573192440216588647568527570441696250) * 10 ^ 70 + 1722062507867757134887835945261709946544830372109197888261364262899501
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_323 :
Polynomial.coeff recurrence4Scalar1Exceptional 323 = -((((400568031792753592 * 10 ^ 70 + 5434772750859483013692091906288148310013018074043940702616847363314642) * 10 ^ 70 + 7400119744366185417343284391502904173116163058755370202001847580525773) * 10 ^ 70 + 9379604303715262854006055225114171796786363975720438515847300508643161) * 10 ^ 70 + 7612036738610891776150476308590667441122021765522810778767433213311702)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_324 :
Polynomial.coeff recurrence4Scalar1Exceptional 324 = (((208158981236852749 * 10 ^ 70 + 5668441537782538955510597630399834074310085338262597221703105428353652) * 10 ^ 70 + 9748566674847213194089266308859289083951786206411328534184130806152586) * 10 ^ 70 + 4470608377012910349963629860854162736463973631164800742205981440220217) * 10 ^ 70 + 1121098173034473319101398442772794110500427661426668695427599145097458
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_325 :
Polynomial.coeff recurrence4Scalar1Exceptional 325 = -((((106163386078011320 * 10 ^ 70 + 370238073885043601056149789266107833572351181167609605868980336574501) * 10 ^ 70 + 625554871116888936014234667956241056935239216437078570043268409795787) * 10 ^ 70 + 6790355126676034273464168007418517236971347213771476971105214889851919) * 10 ^ 70 + 27710308875035360001727763198744958910351730265541576447251205873744)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_326 :
Polynomial.coeff recurrence4Scalar1Exceptional 326 = (((53139523962106192 * 10 ^ 70 + 9408166179569629101381087084709364566262320835293740989739159758649629) * 10 ^ 70 + 3780239119735244247741842019385376996269305946725702620034218570038061) * 10 ^ 70 + 5989452065517576473065738527496810812496328387818917771125813443837634) * 10 ^ 70 + 7745526492997805162278686033551752827998953100543425044313630375223217
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_327 :
Polynomial.coeff recurrence4Scalar1Exceptional 327 = -((((26104396111202684 * 10 ^ 70 + 9390034878721959430342149708037670012865335178485014887092504964620385) * 10 ^ 70 + 2595418085652573551792871876573963917949037946256484461342870901412549) * 10 ^ 70 + 4337756252295291366844054510017085508149566166067231679154265492128445) * 10 ^ 70 + 7828118543149930561205146608248515694931521422003799411761236511683060)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_328 :
Polynomial.coeff recurrence4Scalar1Exceptional 328 = (((12584547503506720 * 10 ^ 70 + 2430994209128921588251237811823982855095928249119551436183577231565651) * 10 ^ 70 + 2583659979021762513013117604684944225661543665646651828921485834169606) * 10 ^ 70 + 6205095659732421453970258472928655850590712405826622554965480572773159) * 10 ^ 70 + 3103332092696735641559040715407524376748738926624414447026087227186254
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_329 :
Polynomial.coeff recurrence4Scalar1Exceptional 329 = -((((5953148938636584 * 10 ^ 70 + 2196866439399458493979521275817701004454013732798087859346535985217405) * 10 ^ 70 + 690607327248768710769595161151179205569199030854615131655350706491770) * 10 ^ 70 + 5795243913779823234486939599011970316967922009114432132936723452139124) * 10 ^ 70 + 67092956473890522689438801300918476529023288995490032162852104431638)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_330 :
Polynomial.coeff recurrence4Scalar1Exceptional 330 = (((2762974664185835 * 10 ^ 70 + 3280589299365943319754986047739531548646555675936489901599775074261104) * 10 ^ 70 + 7898342305447664103819600098442233324814323502681551288544076507716254) * 10 ^ 70 + 6745597314894047936508078589282514221741910321683093809274856084167306) * 10 ^ 70 + 5510240098938519906242384768871233464141769527437173962508757582573069
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_331 :
Polynomial.coeff recurrence4Scalar1Exceptional 331 = -((((1257873391985578 * 10 ^ 70 + 7415195492454484534411051176977632093824916145198417314142111152023830) * 10 ^ 70 + 4853903677821543329239147118812619028122172663308777308256537643841942) * 10 ^ 70 + 4386644005329059203020970792106973017146734430179663007609046509604143) * 10 ^ 70 + 4711001714992844701726616713594461448634931669710071035682429745476570)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_332 :
Polynomial.coeff recurrence4Scalar1Exceptional 332 = (((561565408960899 * 10 ^ 70 + 6225653936230383527306411622600440513766816708323611012386135065955465) * 10 ^ 70 + 6996081649867762061930046240107521455230707713239412830992875421979136) * 10 ^ 70 + 8859676677122997402658000706092862819335973548700935758413291464429763) * 10 ^ 70 + 4199574860600173590378887896509481184779989934862655047271854953006274
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_333 :
Polynomial.coeff recurrence4Scalar1Exceptional 333 = -((((245749415296568 * 10 ^ 70 + 8584487927957867550664728466085076187684241564797534481512661043722565) * 10 ^ 70 + 3230723010510451050425494850717381857173911165760216762860442010020818) * 10 ^ 70 + 6134311873739342963631582654840610826923006146868034136270994672318018) * 10 ^ 70 + 6099285845618314507985324393275248829690598176754047763110802476156996)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_334 :
Polynomial.coeff recurrence4Scalar1Exceptional 334 = (((105358767774819 * 10 ^ 70 + 3250524118059118917279894424623424423533043950852396315988454319913491) * 10 ^ 70 + 8002869947444412550278190409959004176184218065986012693497338146274839) * 10 ^ 70 + 4287597393814704409263518406756640291826142692893181278881429843869975) * 10 ^ 70 + 7186282193687244928451736315625057737472278046451911516726657152087685
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_335 :
Polynomial.coeff recurrence4Scalar1Exceptional 335 = -((((44217395876239 * 10 ^ 70 + 5793755513329290916964618617031785476082771864529492412051332336618911) * 10 ^ 70 + 4056029662699271335336071414915817152507944474533722816923088997745793) * 10 ^ 70 + 892621535372815611551054706916102400309094557022032732232877287234669) * 10 ^ 70 + 3885283844012189541690419663008331964587727116956276449108711683444299)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_336 :
Polynomial.coeff recurrence4Scalar1Exceptional 336 = (((18145529242631 * 10 ^ 70 + 8390066667775800286019772904036312317901483295587818470070583627833882) * 10 ^ 70 + 4279793392354934445147121799553566322817190844668531491466430885270926) * 10 ^ 70 + 4169168317134160420600344530372912304429051448702870006912636585150773) * 10 ^ 70 + 1125252736157008651178127583491406417688702829506344194821195986359769
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_337 :
Polynomial.coeff recurrence4Scalar1Exceptional 337 = -((((7269098397812 * 10 ^ 70 + 7164668445287887752627290013920385624217843948410033432955831540695023) * 10 ^ 70 + 8583067513275800467069585907746446494566820745943754599300761581711090) * 10 ^ 70 + 8362624741834310166546906501715112654514926252089358698356418774271595) * 10 ^ 70 + 6566247508447293005398864090600098819494687200613723158242336077814845)