Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupScalar2LeftPart0.Coefficients0To92

Recurrence 2 lookup certificate: Scalar2Left coefficient convolution #

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

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_35 :
Polynomial.coeff recurrence2Scalar2Left 35 = -(6514450474045 * 10 ^ 70 + 3192117893236711817920234772389016650418524838897600282199218740338155)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_36 :
Polynomial.coeff recurrence2Scalar2Left 36 = 487282175073455 * 10 ^ 70 + 929169693017287691475336309166371483048994511411900458505850020935487
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_37 :
Polynomial.coeff recurrence2Scalar2Left 37 = -(22746990136592715 * 10 ^ 70 + 2730781420168240476997367043142698659815719543075170127956645024775154)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_38 :
Polynomial.coeff recurrence2Scalar2Left 38 = 812271057511571795 * 10 ^ 70 + 4458400888741861927271013787436781045597593404714804680231928848511432
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_39 :
Polynomial.coeff recurrence2Scalar2Left 39 = -(22541731383609462687 * 10 ^ 70 + 8990525514577332299322862685042038255384553864361580077389218789685753)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_40 :
Polynomial.coeff recurrence2Scalar2Left 40 = 448778547124029972947 * 10 ^ 70 + 4551624909081664266421528977604579433001481737622606547350770774186464
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_41 :
Polynomial.coeff recurrence2Scalar2Left 41 = -(4044672538816681952742 * 10 ^ 70 + 7388391609617100530953754659597661180929416956784555793271455221496193)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_42 :
Polynomial.coeff recurrence2Scalar2Left 42 = -(122952503385007611848133 * 10 ^ 70 + 8010834268453708298271805782231255053693522128032343825650840474670167)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_43 :
Polynomial.coeff recurrence2Scalar2Left 43 = 7391923306620800312375099 * 10 ^ 70 + 2198312993390289347941944126866636909299643583810476732817135555444818
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_44 :
Polynomial.coeff recurrence2Scalar2Left 44 = -(219995366876803091568304114 * 10 ^ 70 + 3463361958085961389493379767219358708263628868023025474972744194104623)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_45 :
Polynomial.coeff recurrence2Scalar2Left 45 = 4710714825510915786422753400 * 10 ^ 70 + 3426029699663490197900085542366679180804359748951766799914365160102551
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_46 :
Polynomial.coeff recurrence2Scalar2Left 46 = -(83276584457121403660242988188 * 10 ^ 70 + 2753642487445998961139258492796128803323756979706528788221488999133186)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_47 :
Polynomial.coeff recurrence2Scalar2Left 47 = 1542105123031731461618138312942 * 10 ^ 70 + 3756465917016360841340251783368437535800707384058835177441468061990153
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_48 :
Polynomial.coeff recurrence2Scalar2Left 48 = -(39142665086015022902882868866820 * 10 ^ 70 + 3013443689191911450299303976739900306050433706745716713590278213291840)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_49 :
Polynomial.coeff recurrence2Scalar2Left 49 = 1195257042247813646643464523710336 * 10 ^ 70 + 4330856921076860369075467300671817779076451844968421745059800859547543
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_50 :
Polynomial.coeff recurrence2Scalar2Left 50 = -(33980330113825803410981958771426073 * 10 ^ 70 + 5327546812469453009198170603841581347349384836395315067314397849338345)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_51 :
Polynomial.coeff recurrence2Scalar2Left 51 = 821105170909730501121708028373599740 * 10 ^ 70 + 2721066529837215585347858212460993795280627888491296220333579306587340
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_52 :
Polynomial.coeff recurrence2Scalar2Left 52 = -(16648918692762438262616681173809013046 * 10 ^ 70 + 7152029189423621187303587254148435373239505759865718799018285119488628)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_53 :
Polynomial.coeff recurrence2Scalar2Left 53 = 282249230664182337650827168764921262309 * 10 ^ 70 + 5951152207618325090756730401537707999687135413390656466914347344808031
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_54 :
Polynomial.coeff recurrence2Scalar2Left 54 = -(3898596611445870451703727890221121205401 * 10 ^ 70 + 8176839286287074378699818914458924175043450621663852800965671552383847)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_55 :
Polynomial.coeff recurrence2Scalar2Left 55 = 39204929340230800059014746262207335617234 * 10 ^ 70 + 4586855524113787573172583804057544796535808793597798346109259468375797
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_56 :
Polynomial.coeff recurrence2Scalar2Left 56 = -(111766540798516298197587797323985213866934 * 10 ^ 70 + 7731683656913586065327364178532773626901744464613147885696717914174952)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_57 :
Polynomial.coeff recurrence2Scalar2Left 57 = -(7203966099826935877280736865448943698449904 * 10 ^ 70 + 1247361854292825335123535082797295258979360840062083481585038929543933)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_58 :
Polynomial.coeff recurrence2Scalar2Left 58 = 244794217244704337141682671508798983517174205 * 10 ^ 70 + 2624542390080919706790253655590521101320996641168797862689336957367861
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_59 :
Polynomial.coeff recurrence2Scalar2Left 59 = -(5398974594395137268743829891170197063539421426 * 10 ^ 70 + 8302326666513492514817747338248817625866481735185303166318080047488212)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_60 :
Polynomial.coeff recurrence2Scalar2Left 60 = 96817752849741796622419306456103367068640410324 * 10 ^ 70 + 9547207725809411422483504997171492786090380746516259313933833927476901
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_61 :
Polynomial.coeff recurrence2Scalar2Left 61 = -(1486374858148276198311819067015716813059363513578 * 10 ^ 70 + 6115442498009952592431153656773921228312460420801750750492024627954788)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_62 :
Polynomial.coeff recurrence2Scalar2Left 62 = 19623413909393901991282353564704953304675805051053 * 10 ^ 70 + 9755553930185972997973907000345848957314164033684708156423374296643950
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_63 :
Polynomial.coeff recurrence2Scalar2Left 63 = -(215586538084572651598016830715467217632451566690911 * 10 ^ 70 + 3595689577481660966668588426351217937413935964778251900508817304858084)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_64 :
Polynomial.coeff recurrence2Scalar2Left 64 = 1735170733468349916310043373257386695775276753848534 * 10 ^ 70 + 9397532051696765058285243707519155696423362677533156186900583846025970
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_65 :
Polynomial.coeff recurrence2Scalar2Left 65 = -(3385907550573403540077628921048123691583102295166379 * 10 ^ 70 + 3269464254339738817558900156816346321167023848335455818125330934842625)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_66 :
Polynomial.coeff recurrence2Scalar2Left 66 = -(232830205355849095414969789836458958940252547661402334 * 10 ^ 70 + 227559665032124906358251857521060197468535595261485256997776401892702)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_67 :
Polynomial.coeff recurrence2Scalar2Left 67 = 6387567811206810542834182445575605036092758425854630370 * 10 ^ 70 + 4909481620461424129553737735026533478579281692865057523290824979811046
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_68 :
Polynomial.coeff recurrence2Scalar2Left 68 = -(117102457676071340869968629944502007325374816305114451708 * 10 ^ 70 + 5781987068130552883935802284006326635247692029542442623041496077927937)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_69 :
Polynomial.coeff recurrence2Scalar2Left 69 = 1789262554301831334992147854737252764393645757492492191531 * 10 ^ 70 + 5748676433739351192331594763648804784814593490200562024504534109012148
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_70 :
Polynomial.coeff recurrence2Scalar2Left 70 = -(24300803355724518334105100001941477544575780170732637549379 * 10 ^ 70 + 4096610195963911085425294357272615553125428914201844896188045896533269)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_71 :
Polynomial.coeff recurrence2Scalar2Left 71 = 301781199392324330030836470033104875320381195918341077462494 * 10 ^ 70 + 7006890161627451939303262213244787829884910543016567628856739136241621
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_72 :
Polynomial.coeff recurrence2Scalar2Left 72 = -(3479175121644930073083817451354372434724477866306854198607899 * 10 ^ 70 + 8440730661392592156998172849147111629519053426586576071232040549374699)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_73 :
Polynomial.coeff recurrence2Scalar2Left 73 = 37581083199818579932951535145082112560997198518984955363868341 * 10 ^ 70 + 3135842940166160930645617645179666266495405033366329605005018039346269
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_74 :
Polynomial.coeff recurrence2Scalar2Left 74 = -(382671168490014286438332741066337464055393088613499199922192356 * 10 ^ 70 + 52695632843544571726519501883947879608959335497095092326604987275616)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_75 :
Polynomial.coeff recurrence2Scalar2Left 75 = 3689293314953338549749233476236943540737999920754907149174391000 * 10 ^ 70 + 5652803744371633007595532880322659766875795795520690360427920020142985
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_76 :
Polynomial.coeff recurrence2Scalar2Left 76 = -(33787744726819881861470323391918932813376164735479765111402259190 * 10 ^ 70 + 3951747153520345710919521617696737641340944626635691747897874775980510)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_77 :
Polynomial.coeff recurrence2Scalar2Left 77 = 294718355550947044365649171448470962218400154277982121469482365610 * 10 ^ 70 + 5862784399547174058131343271717257203979630251653290339727674813814066
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_78 :
Polynomial.coeff recurrence2Scalar2Left 78 = -(2453574224273264227980320308939672591229613740406427661708332162111 * 10 ^ 70 + 9802253314936304489815248633387137937033627244937369318838477632362764)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_79 :
Polynomial.coeff recurrence2Scalar2Left 79 = 19528679628202398349780310163671838375911042301272797349851152125528 * 10 ^ 70 + 368616024564606895177990222949377138103894026544606830690088232826560
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_80 :
Polynomial.coeff recurrence2Scalar2Left 80 = -(148806932796755723596588006156871748258654598616870748760566736886845 * 10 ^ 70 + 4470597434393683724323471812116677232268529584767795237198908959193275)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_81 :
Polynomial.coeff recurrence2Scalar2Left 81 = 1086749884754588267393733176580871654477447487810520139641842261902556 * 10 ^ 70 + 6789066874613138780541933870481231677293973268769732387311611293578596
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_82 :
Polynomial.coeff recurrence2Scalar2Left 82 = -(7613468073789463212192873414692256303447111512727455300665098088724754 * 10 ^ 70 + 26380284801347395283674542119956209448154298500390777818742332907693)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_83 :
Polynomial.coeff recurrence2Scalar2Left 83 = (5 * 10 ^ 70 + 1204314254865166213767475670857560016049845592631218497836263257857457) * 10 ^ 70 + 8963039404408754870513019259418732526736557607136679556856779296324270
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_84 :
Polynomial.coeff recurrence2Scalar2Left 84 = -((33 * 10 ^ 70 + 809102846814970458531257869101825766696471133678107865893511150200160) * 10 ^ 70 + 1469141110699685743707856856152394922271466973756741382217758163495172)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_85 :
Polynomial.coeff recurrence2Scalar2Left 85 = (205 * 10 ^ 70 + 4134701132078945450769468969856347053385523967076581718842068114851468) * 10 ^ 70 + 3040939777543560004135661035191913082716520267271874143563593967581020
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_86 :
Polynomial.coeff recurrence2Scalar2Left 86 = -((1226 * 10 ^ 70 + 4448521164850441036711001360900899102478852122772403678709465076444964) * 10 ^ 70 + 7760621846758170593776374510055525627831382564310653560562761633846177)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_87 :
Polynomial.coeff recurrence2Scalar2Left 87 = (7043 * 10 ^ 70 + 686814827633286085668130915197678885194282213635944034737495905423956) * 10 ^ 70 + 2424121228167773522307692908591413659292254800585661362084809956876334
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_88 :
Polynomial.coeff recurrence2Scalar2Left 88 = -((38906 * 10 ^ 70 + 4757774210024060294068546807931011247091679588738824289497684143908854) * 10 ^ 70 + 74909911104934272253506009461529513462655188099653263136084198017728)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_89 :
Polynomial.coeff recurrence2Scalar2Left 89 = (206724 * 10 ^ 70 + 6267474681411197620082216357550361779121234218375808860204253443012199) * 10 ^ 70 + 9165082750488335182018330827859403011854394396125624190932386979381121
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_90 :
Polynomial.coeff recurrence2Scalar2Left 90 = -((1056207 * 10 ^ 70 + 7680277299344252509559475940288934755160126920542564329852514144204152) * 10 ^ 70 + 96175803096461064779463780823033871160914630235252144801168008778758)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_91 :
Polynomial.coeff recurrence2Scalar2Left 91 = (5186693 * 10 ^ 70 + 8439748252386095895521287020526186398922323599257938781387137491764374) * 10 ^ 70 + 4505343653105755097382058353461801537692683230136311783545705550583119
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_92 :
Polynomial.coeff recurrence2Scalar2Left 92 = -((24464821 * 10 ^ 70 + 6132300824182064683784861445028743484039200211795026279322788325707681) * 10 ^ 70 + 9247822129104357842156346278935930756091528356209921963038231637336778)