Recurrence 4 lookup certificate: Scalar1First 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.recurrence4Scalar1First_coeff_330 :
Polynomial.coeff recurrence4Scalar1First 330 = (((892959632503004 * 10 ^ 70 + 9909211703986790806167155495563839833685435337031286128668607487975064) * 10 ^ 70 + 7030394691955019857357817856527304228990221853089078587320268577155564) * 10 ^ 70 + 5685582590779067280518987905918295544159564755770661262420515994955039) * 10 ^ 70 + 4147424677865491426679184791229696642769321545874652979306727898699368
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_331 :
Polynomial.coeff recurrence4Scalar1First 331 = -((((520607061361205 * 10 ^ 70 + 720031965399956741908307535046814462650323511291830696338021932000897) * 10 ^ 70 + 2473266656851413026643504428317283699731503246811128896368540832292247) * 10 ^ 70 + 1539394712879539010394490961674152380115484597543081452636870674910724) * 10 ^ 70 + 8068710672685218667311233994027349475363597848632793488621259734909832)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_332 :
Polynomial.coeff recurrence4Scalar1First 332 = (((296418398346675 * 10 ^ 70 + 8685580342182895797292725773614760579711394646166832419767164856127831) * 10 ^ 70 + 889151378912136826035704699662589222328333998129147404796572544411472) * 10 ^ 70 + 4092142569860651021875494491616908456424018192036214250138225023642907) * 10 ^ 70 + 8630278620060895085725221937441297233148500855247887559102972876201210
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_333 :
Polynomial.coeff recurrence4Scalar1First 333 = -((((164983923058507 * 10 ^ 70 + 2602963453857639592565362929050682630622294428567234851717095147410308) * 10 ^ 70 + 723015249497384958390373248191027885750580846504764926710536579199928) * 10 ^ 70 + 5946077058551886162445777929118015616216684450420960587681380449405172) * 10 ^ 70 + 4606107876571410692878834580543630489231508076557691176000168441387412)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_334 :
Polynomial.coeff recurrence4Scalar1First 334 = (((89847991528526 * 10 ^ 70 + 5802494215843710171505189759532468852986068702886766399696514214954990) * 10 ^ 70 + 8781860962603329644744072603503344019180792541718473916877032392355540) * 10 ^ 70 + 9344611179226387080573049635499591362443409586136332321575865722885867) * 10 ^ 70 + 2642674814007841591003295921932914068429681807873452562688948430626424
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_335 :
Polynomial.coeff recurrence4Scalar1First 335 = -((((47912322805909 * 10 ^ 70 + 9959868657346774083961508521260080944513795265550603671609570338162103) * 10 ^ 70 + 5783621853647267080051034286962991310722983357798868267962030847622103) * 10 ^ 70 + 9630453268588707671403457686495778544662084118328733870230960721024583) * 10 ^ 70 + 9983033906134651967982748714702042895887432538906246049194740529378603)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_336 :
Polynomial.coeff recurrence4Scalar1First 336 = (((25035163180287 * 10 ^ 70 + 7134125201219897880768058656314873300547846748286102023735100422015105) * 10 ^ 70 + 7072175119973423347647031751348178813373695611699184753431614296090044) * 10 ^ 70 + 4388035159134906258991314838416716750682615548628199668613850425801423) * 10 ^ 70 + 4217864951581813890580486440031596322934294189971977915150661546894042
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_337 :
Polynomial.coeff recurrence4Scalar1First 337 = -((((12825142567348 * 10 ^ 70 + 3771431913589638908105713403275840339049856693342783889243603778301434) * 10 ^ 70 + 8038722195847517365434256349082435325740030548656733942918175556756473) * 10 ^ 70 + 8136416603841086084699739073914389360032746457102841778894682066933590) * 10 ^ 70 + 1458631584859403800635544175460911973658621541477342903738804351615424)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_338 :
Polynomial.coeff recurrence4Scalar1First 338 = (((6444391532605 * 10 ^ 70 + 2685941389994674316553041214482318895012539500713989930132209634099236) * 10 ^ 70 + 8929485671310532998272618734291023056996816657025346637062868735129547) * 10 ^ 70 + 7167729966579085297730387106717367493917706416417736406592527151817209) * 10 ^ 70 + 7396554754590024370590590862810918758688836078560130630016515232742432
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_339 :
Polynomial.coeff recurrence4Scalar1First 339 = -((((3177368264022 * 10 ^ 70 + 6364466180882550629119027198307774348661582427616228248267415049942228) * 10 ^ 70 + 9911237525333681257324686251207174921011159663011409089203752606067978) * 10 ^ 70 + 5733659645764503885707055305201103644999482925417743110719183514633779) * 10 ^ 70 + 8220155210499187169140475310896434987489649619199181347584714160290581)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_340 :
Polynomial.coeff recurrence4Scalar1First 340 = (((1537583902812 * 10 ^ 70 + 1507187282857434718217518397347067444919000409452210647190830940138367) * 10 ^ 70 + 352538969641034010674799741465284303494503023715971054714821755274415) * 10 ^ 70 + 3908259915903411739498293403194095222987391546278033210409052659827004) * 10 ^ 70 + 9413352377788033952063853586601690827445048795638856526754659412637083
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_341 :
Polynomial.coeff recurrence4Scalar1First 341 = -((((730431708582 * 10 ^ 70 + 9956130790311222137386264847594932596593221633056423238924446745801009) * 10 ^ 70 + 2826472329254836412607174454818095034198248407610803182518771300439792) * 10 ^ 70 + 667703545132801186348461740602071064779288630465814326163994057619181) * 10 ^ 70 + 5616838497162570030977371546330493610404550912280243388884095271124705)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_342 :
Polynomial.coeff recurrence4Scalar1First 342 = (((340674386809 * 10 ^ 70 + 8821805697756992961610500276292818259955766989816958161428723384084832) * 10 ^ 70 + 4062994278381195584503902396247843348622571637387545518187639043093635) * 10 ^ 70 + 7823708020125228280939421103843055729696091261921936934619498648431222) * 10 ^ 70 + 9487748382986348556617867949030074512374944755704001350481277346359964
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_343 :
Polynomial.coeff recurrence4Scalar1First 343 = -((((156003348475 * 10 ^ 70 + 196736352184092452283644987984964636568390438809720541786187452885091) * 10 ^ 70 + 7066213932622104191814276554391003655564503047731307695536293224121593) * 10 ^ 70 + 9552289391424450951404780949963687449689622822721093075342419534916286) * 10 ^ 70 + 3995401865097628192535255852847698275552157198523625001515400530681495)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_344 :
Polynomial.coeff recurrence4Scalar1First 344 = (((70136353208 * 10 ^ 70 + 4013312222524135978056709718389278990515950172112621404011503542226458) * 10 ^ 70 + 4993787560345476509157921694442076281040490089871418925924415078168402) * 10 ^ 70 + 8395126202379110561707311379329939240751564141458526282881903261601563) * 10 ^ 70 + 1907382269033018607401718682598409498061722037451680523563929899331987
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_345 :
Polynomial.coeff recurrence4Scalar1First 345 = -((((30953451309 * 10 ^ 70 + 7113729956522345468477819410709466278383257450474076514656341951020625) * 10 ^ 70 + 3207427231771461318687885233896529266014029593839933831216680922316770) * 10 ^ 70 + 4856455672288439279847858035275305408278868843541852208632140852546808) * 10 ^ 70 + 1654563986693770700675760834354642046264481445640474487855503357318084)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_346 :
Polynomial.coeff recurrence4Scalar1First 346 = (((13406922525 * 10 ^ 70 + 1539062937107066068913298212590562013566565899643516622548876416918670) * 10 ^ 70 + 5951619005388620364613876699309507951926666938892092397736800785628722) * 10 ^ 70 + 1052038519379592379787710229432281188602567441597023787832092351851911) * 10 ^ 70 + 9291044129008407232988791922342623446405879853307987082632693870037969
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_347 :
Polynomial.coeff recurrence4Scalar1First 347 = -((((5697005138 * 10 ^ 70 + 7302841675957798479026378251429984375836554496412020554394361121141582) * 10 ^ 70 + 624180103297904106736753513736763485642377347547838288311434792434515) * 10 ^ 70 + 1845111835307473310334221808696695032513486438011728537786342469629892) * 10 ^ 70 + 4471109339148950018186531142608558548916515222872183867081823705752251)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_348 :
Polynomial.coeff recurrence4Scalar1First 348 = (((2373752054 * 10 ^ 70 + 931494082818702327465068879428613929580844858340522425987838047333260) * 10 ^ 70 + 2195343345613815435239386880239383231646814024353187788346445107785953) * 10 ^ 70 + 3712813791328561444333753316322145187667721309391529912672656643002703) * 10 ^ 70 + 6918730710991833482243577390527175338446700585360713698506258234884007
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_349 :
Polynomial.coeff recurrence4Scalar1First 349 = -((((969114555 * 10 ^ 70 + 2978621852622749767559541054206757362344594782814233213615772685087179) * 10 ^ 70 + 7102157576060580075026459365283773353842174246161513291282622804535144) * 10 ^ 70 + 1693703606792783783633548937412066492363611098034920912242752082852693) * 10 ^ 70 + 7184962747175547008181257597652082256549943443638012632011852081019566)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_350 :
Polynomial.coeff recurrence4Scalar1First 350 = (((387269661 * 10 ^ 70 + 4074146280988252347831070408300322383730000169659750834846605048384195) * 10 ^ 70 + 214734832917397232864748119150054932739748485908567700406789175321635) * 10 ^ 70 + 2246933020686581372915389643836419483536658471375249488599812008776975) * 10 ^ 70 + 6510116175348067493096669033978228903252618750570866848982122956875986
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_351 :
Polynomial.coeff recurrence4Scalar1First 351 = -((((151253192 * 10 ^ 70 + 5875604385660843250944419611218714354330205763385988316468452654457655) * 10 ^ 70 + 8453482303145117780453636673324738867824441802756734311543008872010119) * 10 ^ 70 + 6919466158195752897245636548233779612908230768965222713322776680880413) * 10 ^ 70 + 6992787308392587030121526781378992656029377550133731469561141164824481)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_352 :
Polynomial.coeff recurrence4Scalar1First 352 = (((57611355 * 10 ^ 70 + 3061536085009074624662389507335225874473063489797436345613822194263537) * 10 ^ 70 + 847160646361089362517656553744623826219106940108330254764268315785740) * 10 ^ 70 + 5434448572884262195460872139896541865257277856430787711544230491294677) * 10 ^ 70 + 5879593821810343494827778829903283531957856274254259589290495569773516
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_353 :
Polynomial.coeff recurrence4Scalar1First 353 = -((((21331238 * 10 ^ 70 + 5330515621612540574745347566457418843330014629644569902001201609971105) * 10 ^ 70 + 5640765221715441906746945828703955884922032127309323130267333788963907) * 10 ^ 70 + 1941956937679268515338908468832769298235760675105826158550827333084468) * 10 ^ 70 + 376255698242027116012371801074909618271489166998780499247604608817752)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_354 :
Polynomial.coeff recurrence4Scalar1First 354 = (((7639003 * 10 ^ 70 + 1355175555826894661477224774911999366701909379969959470017286421313637) * 10 ^ 70 + 9182831539305916292173041581978795716749742389713062011572385383436919) * 10 ^ 70 + 2795728837885502286951591927486837483684793202805488109224030340989672) * 10 ^ 70 + 336756494072717649177116525700549125396738861716495239185865938361117
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_355 :
Polynomial.coeff recurrence4Scalar1First 355 = -((((2624038 * 10 ^ 70 + 1694708556623681335925585946356433937429102661472106041308469375921181) * 10 ^ 70 + 620947290903900721642718071918272526504143189733177476082753559420039) * 10 ^ 70 + 9394110108638011648987510453939958824882333670400514652918836695284567) * 10 ^ 70 + 1275343783973577658823230416668564124612398040686828880942952572056876)