Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence4LookupScalar0MainPart2.Coefficients277To302

Recurrence 4 lookup certificate: Scalar0Main coefficient convolution #

This is a checked coefficient-lookup shard for the fourth pseudo-division recurrence in the order-seven certificate.

source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_277 :
Polynomial.coeff recurrence4Scalar0Main 277 = (((8655522599276278811347099468 * 10 ^ 70 + 2913207067861278755179597904544965464004293085243636699102570102068711) * 10 ^ 70 + 5602574059751752891893752766861982167702151913928571757110130648202263) * 10 ^ 70 + 812698427356845297675428121015230037483473462594796930749279132136154) * 10 ^ 70 + 519018474275804959369083367368956292289510935639016949496076065613546
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_278 :
Polynomial.coeff recurrence4Scalar0Main 278 = -((((6726450539442572675168856616 * 10 ^ 70 + 6390570004122698985489034692517444272869391892814348136966505537455111) * 10 ^ 70 + 3357675924793995782970977535153260526689100957105590087070275897004290) * 10 ^ 70 + 5899415290830839887202383018737654254969878927927892858865914020977462) * 10 ^ 70 + 9006269851784420325202854419277603698283572588811457342138188132495236)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_279 :
Polynomial.coeff recurrence4Scalar0Main 279 = (((5146801278999889073525065706 * 10 ^ 70 + 3963735351092309981868567781302544402194495198879583445769858728115438) * 10 ^ 70 + 2628796245379337897044067224770430067269014731486214282990351391319485) * 10 ^ 70 + 9807613512585873341558955320048767491997464622998486673842117597844052) * 10 ^ 70 + 1449091825260576679821968981297379815399390528670970366762341352706141
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_280 :
Polynomial.coeff recurrence4Scalar0Main 280 = -((((3876836598710549174057804028 * 10 ^ 70 + 9254629390845967883315951780158380004442803399822639399943347684267313) * 10 ^ 70 + 422514187975915803590715203496278633251984158140859350441295894713958) * 10 ^ 70 + 5438036578139453827569767246659381664367774477444099146850521438585435) * 10 ^ 70 + 7932541883291134605563012837010267949823195165000488064387152594153663)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_281 :
Polynomial.coeff recurrence4Scalar0Main 281 = (((2874206544155961510353377899 * 10 ^ 70 + 1799452705938121664481531890805631885030553088598055207328756407384551) * 10 ^ 70 + 7969870045097726219542998690373233029389971625234238084731338701362248) * 10 ^ 70 + 6921814692259676248935422040476236488163085156914485394498305571651718) * 10 ^ 70 + 6194763681483630239526293036895193923146817693430287121398329243710185
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_282 :
Polynomial.coeff recurrence4Scalar0Main 282 = -((((2096762053773696155389359383 * 10 ^ 70 + 8391103793091113336376877869668435078195025296812347136521000012350349) * 10 ^ 70 + 5508744697924963996155233313654625496602735010548583611721118590111845) * 10 ^ 70 + 4583593459486256785875524012659263511610760742819449607140172098683596) * 10 ^ 70 + 3063416430547851222705763783216129412621773545146013575228584332536629)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_283 :
Polynomial.coeff recurrence4Scalar0Main 283 = (((1504650104590878789724967685 * 10 ^ 70 + 7045104536741854874181499339114016446594519477150376041504814116635072) * 10 ^ 70 + 1511152345444120599191242471154249983017659582090963404032582936322650) * 10 ^ 70 + 150326896547556602942332500055395447424715337166187448051491381065270) * 10 ^ 70 + 6971583569405619494905308869059693596313027482906116694129443255568384
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_284 :
Polynomial.coeff recurrence4Scalar0Main 284 = -((((1061719594019440059198693394 * 10 ^ 70 + 519915661416499997737980190456661810274879046403845838854121423440594) * 10 ^ 70 + 2798191967495216924152691666990462565417133409272192972405208528681174) * 10 ^ 70 + 1326465730265928723490834777968833068077428170265682137050467338293122) * 10 ^ 70 + 3222567474545642630774886360966682394557417367981891192320579296969682)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_285 :
Polynomial.coeff recurrence4Scalar0Main 285 = (((736317258640736722900251606 * 10 ^ 70 + 6443870656171904617872070343983595125269582070593004755321792306012397) * 10 ^ 70 + 3521238941437568370366866742235842873984373294042279058950538653932414) * 10 ^ 70 + 9096637310170396455263349807850212701555556086746486658048049944707724) * 10 ^ 70 + 5532940979492172361023783176608681747523748980479707498707702495011708
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_286 :
Polynomial.coeff recurrence4Scalar0Main 286 = -((((501582996776778380256790365 * 10 ^ 70 + 4171235169898424519082021944724027607622860933209403045217066567616742) * 10 ^ 70 + 6888959616421399726522883051590934378460785036458179073351016554817081) * 10 ^ 70 + 8247458930941472880440095532236506016955953766237611172390698433270137) * 10 ^ 70 + 3320216095330464454513004444770404414682559479802446484736486500093573)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_287 :
Polynomial.coeff recurrence4Scalar0Main 287 = (((335365453425583745405195669 * 10 ^ 70 + 8508869155648173779284755605027454085232940003821989013953401987885047) * 10 ^ 70 + 2598010234786125771478506481928951451637913662923915705176960937274332) * 10 ^ 70 + 6943752629918090485570562689737867883525321537208151521335588512975045) * 10 ^ 70 + 8986728610197290711762538691421567111113833002495862197515224352958335
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_288 :
Polynomial.coeff recurrence4Scalar0Main 288 = -((((219875576404014074449752398 * 10 ^ 70 + 2413694079903071565567497799719406708707139606390429521320318030354736) * 10 ^ 70 + 5785427673668289521607287971220714112275401406663943359725111227201578) * 10 ^ 70 + 4746516648944926641931695793729903434174212932620261541381026087774238) * 10 ^ 70 + 3872922695284264738756882769728672683595328693736621757077165131341516)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_289 :
Polynomial.coeff recurrence4Scalar0Main 289 = (((141182578131743387170350811 * 10 ^ 70 + 9067608853033578907325572969758421197467921698777468341437500465195589) * 10 ^ 70 + 2587571006530455755523790594682827546645423770333738773385088178683094) * 10 ^ 70 + 3136185989981359439738970363490446037501260593571866883502040494563158) * 10 ^ 70 + 2578429750170974921693103804125673721574683106568439423893218277332087
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_290 :
Polynomial.coeff recurrence4Scalar0Main 290 = -((((88637707745398620426939694 * 10 ^ 70 + 9128254414236669636268767565447302149613849201951323630743962601938453) * 10 ^ 70 + 5934479035682336736778642719828502571795302577692991483936279837897170) * 10 ^ 70 + 1575910605535568498180457757791710470144942144612933398733418524206267) * 10 ^ 70 + 7440648767424870423816232830427050138713850562663136325793550240104249)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_291 :
Polynomial.coeff recurrence4Scalar0Main 291 = (((54290174121050280163231046 * 10 ^ 70 + 1009428123793588581528496851775544339797265201315635610492629525067238) * 10 ^ 70 + 5683164505730155113016883984633404857076443041571273624987450865864228) * 10 ^ 70 + 1389313407968988228086126352568603483254470745429217383352579436744942) * 10 ^ 70 + 451171179929950011254878817608295089759896535864663787486632938742033
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_292 :
Polynomial.coeff recurrence4Scalar0Main 292 = -((((32339269403049455661343512 * 10 ^ 70 + 4124603392083756037059142439217025459816135038089705259609188834075520) * 10 ^ 70 + 8190743105488696784651157248645447893352220655993481037389507868856199) * 10 ^ 70 + 7452983353741510383535631033673295892737066700886541611326945707374261) * 10 ^ 70 + 8412583726439799025217072659586591838129559983405052578598768206869931)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_293 :
Polynomial.coeff recurrence4Scalar0Main 293 = (((18649056686018448219407524 * 10 ^ 70 + 7688166561354914613873338970164675851316744732175252118177244722255290) * 10 ^ 70 + 5726503899445126238687290222280370885394609574039298871025611451338849) * 10 ^ 70 + 5079907940538043982957711231492895571724317551188961701513937672792682) * 10 ^ 70 + 6141923449763086905613550954692287048879462865647928732604532888043824
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_294 :
Polynomial.coeff recurrence4Scalar0Main 294 = -((((10337847867889493192741562 * 10 ^ 70 + 9017498763270694786552268308071185501203291098527521474359248892110110) * 10 ^ 70 + 6562138142016785730774962786780387023614884818200460390126487026865804) * 10 ^ 70 + 6799660940286527888740513135490853164424653976628579775991140796881) * 10 ^ 70 + 817325551164038862906719820286053298812596019127517388474366442744708)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_295 :
Polynomial.coeff recurrence4Scalar0Main 295 = (((5444339480736519766292045 * 10 ^ 70 + 8214425552470402143232809617746040250437242789432537525851143642519138) * 10 ^ 70 + 4652592440156695067158109133672398065088275211087164299237938714239208) * 10 ^ 70 + 6618439587640432267633912026623439436063004497049828777286601251617451) * 10 ^ 70 + 5021380851234514505744138602785958736825129824765237081372863212217553
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_296 :
Polynomial.coeff recurrence4Scalar0Main 296 = -((((2665426137482510851070439 * 10 ^ 70 + 999129489468950598385938036840456254016351807424496007264777619369741) * 10 ^ 70 + 8833917628790723689279391800452161686928975827193773558990739708526135) * 10 ^ 70 + 4867185055813279884554261585786514712623395751508059900493059121368788) * 10 ^ 70 + 7294402469649570337387121734265926021100520560424954478874237722746573)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_297 :
Polynomial.coeff recurrence4Scalar0Main 297 = (((1156808678714015901918155 * 10 ^ 70 + 8321441097964550912032004754621326214536207416678212469049433759433674) * 10 ^ 70 + 3925816782471204497436076770189096883113650484733500124878901921018066) * 10 ^ 70 + 408477882951153806710551401622544934270329228338525297369321704946525) * 10 ^ 70 + 8562219383075788782247585659343575699568666377917266833676661701024492
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_298 :
Polynomial.coeff recurrence4Scalar0Main 298 = -((((385870136888829256453883 * 10 ^ 70 + 2530322057859327020592791476378358332514692927512834309342652879909575) * 10 ^ 70 + 2189198467794042020305958985378786499769590924113220533541024718819901) * 10 ^ 70 + 4440824727881281986560433350490042111769970374179895964353562798783738) * 10 ^ 70 + 2754241827001469470443727194667795910132026614583677922292330754397218)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_299 :
Polynomial.coeff recurrence4Scalar0Main 299 = (((26224574678300755842770 * 10 ^ 70 + 981873338280275903203314404607423841422522345349536034112050156362026) * 10 ^ 70 + 3489299922014694472032484956988648074368254569809323981468041918734130) * 10 ^ 70 + 999227764533052597249313441430883687066927582647705643445948270866508) * 10 ^ 70 + 877940016749313857830309900359735874948976224022669686699954920565163
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_300 :
Polynomial.coeff recurrence4Scalar0Main 300 = (((115746533961228421590195 * 10 ^ 70 + 4659280008832592386333685306156690435217034509375315874085197379161103) * 10 ^ 70 + 2713263164125181479455118589419173869580219515424986572444291014912766) * 10 ^ 70 + 361100568642337441372182243113666226936083461896403084376184026241469) * 10 ^ 70 + 4374046530118734716055984807036558762762153404494092939440014384344156
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_301 :
Polynomial.coeff recurrence4Scalar0Main 301 = -((((150642881576481194457169 * 10 ^ 70 + 7720922895768723182624116703729342794099782521163445033165952217738752) * 10 ^ 70 + 4188457555904616744276020904686327054079341945405918712592402787498284) * 10 ^ 70 + 5000043621341928248838601172982598698757304104189971814612733254862352) * 10 ^ 70 + 3623367868420069460949002491293524764878635104545280089213567970087652)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_302 :
Polynomial.coeff recurrence4Scalar0Main 302 = (((138777569889727507263015 * 10 ^ 70 + 9382832075217484561866645223026991424241953782402738357837364325378094) * 10 ^ 70 + 333178562143113176866725471995690863936157764843339572298681712848763) * 10 ^ 70 + 4773269613329033441867592866602970247997716495122372021736404980984947) * 10 ^ 70 + 2728888266211371207210367686343456904887909144511718583395390635801200