Recurrence 4 lookup certificate: Scalar1Left 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.recurrence4Scalar1Left_coeff_41 :
Polynomial.coeff recurrence4Scalar1Left 41 = (1148846 * 10 ^ 70 + 1626572250667005079425759856297232727257996451614468228865094920222026) * 10 ^ 70 + 3792495794554404785681662751583174858064112866812140091935480513022931
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_42 :
Polynomial.coeff recurrence4Scalar1Left 42 = -((124308326 * 10 ^ 70 + 3221735196797081044441833709157382764775843958464065854995075992914235) * 10 ^ 70 + 10252046830046343361212501601916422917948223909433562945445174033837)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_43 :
Polynomial.coeff recurrence4Scalar1Left 43 = (10913350609 * 10 ^ 70 + 3225905214195092533048606518572526601835524101804677867375848131920922) * 10 ^ 70 + 2969121297382274173820844489849694431048179651609709824595325739709436
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_44 :
Polynomial.coeff recurrence4Scalar1Left 44 = -((739332237013 * 10 ^ 70 + 7504607518401542299917024329655125842142354044791876901123928470328442) * 10 ^ 70 + 8075615207926955139669317154830048393559817964842013129583655107410632)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_45 :
Polynomial.coeff recurrence4Scalar1Left 45 = (28902952590510 * 10 ^ 70 + 5214474693553824868924779110769165782742141414723386825438643958872162) * 10 ^ 70 + 772477451838890395178278622616462989142547151883703274294522444572154
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_46 :
Polynomial.coeff recurrence4Scalar1Left 46 = (1433083287659396 * 10 ^ 70 + 5182620558734669929277434720698797523685607495836743829463563897269255) * 10 ^ 70 + 5592188378715877942958035305732199235488182575508901428184224619185139
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_47 :
Polynomial.coeff recurrence4Scalar1Left 47 = -((467825012025360587 * 10 ^ 70 + 1229019258667720152222877242863814248283457028901049268262574229044204) * 10 ^ 70 + 2911267944771046770336243144437473159491353247110663938414554785326295)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_48 :
Polynomial.coeff recurrence4Scalar1Left 48 = (64357831141051309904 * 10 ^ 70 + 7550022315575286603205434792065644540527317658217170067568085056690785) * 10 ^ 70 + 8593564258855357598288974834245892632080546773583592928303714330123153
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_49 :
Polynomial.coeff recurrence4Scalar1Left 49 = -((6780283266861045609800 * 10 ^ 70 + 7146285368243627927768157052128879010501561634520113784553497703404740) * 10 ^ 70 + 5692723102804397706380259354327566626733494837786774798519315844539137)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_50 :
Polynomial.coeff recurrence4Scalar1Left 50 = (610168502147786387417529 * 10 ^ 70 + 3610903284770278198739749426641189494694081413204614037087598518002998) * 10 ^ 70 + 6814344214990134625063780258654579733723893496350998192641617502700328
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_51 :
Polynomial.coeff recurrence4Scalar1Left 51 = -((48887946504534378661299359 * 10 ^ 70 + 4375449768558053770594703440818438198096539657645964227289110978414487) * 10 ^ 70 + 4905676138968354679254882647990583976697812655438731515697504218436751)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_52 :
Polynomial.coeff recurrence4Scalar1Left 52 = (3560679445490136693662319550 * 10 ^ 70 + 4647344494608828640323442988044477726519204161207628088669710350554821) * 10 ^ 70 + 6527557643248453634950335476913092626890225239088447104248380336495307
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_53 :
Polynomial.coeff recurrence4Scalar1Left 53 = -((238646809675073624706211386436 * 10 ^ 70 + 4141306506171006693083216261805812214440741256522335866169879438367425) * 10 ^ 70 + 3560394786854932913407908441894571920508140415362523344006947170201688)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_54 :
Polynomial.coeff recurrence4Scalar1Left 54 = (14836786514148983290105204548637 * 10 ^ 70 + 6587187293508553269601859475571523704217474189671877080096985616506811) * 10 ^ 70 + 8058757587765952306334152399140680840848249995540124865331357280859805
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_55 :
Polynomial.coeff recurrence4Scalar1Left 55 = -((860447010897594386915041264688006 * 10 ^ 70 + 5265920558591492832269040048350859057150167833076428391937893708536744) * 10 ^ 70 + 9545687732039591013881292421284666174229994695004407607661927952325489)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_56 :
Polynomial.coeff recurrence4Scalar1Left 56 = (46742964372635072294072957003256544 * 10 ^ 70 + 4904727091637327378814984400813374904218998835370483493206938808708853) * 10 ^ 70 + 9375192573660945834370959759206586832704162003901519962842455986849666
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_57 :
Polynomial.coeff recurrence4Scalar1Left 57 = -((2386216665867495163519465091104100735 * 10 ^ 70 + 1907936441170802483191698657078080190816223344543582264579029549836029) * 10 ^ 70 + 9047086916480904166455746045302324492675210655788063413020486493014131)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_58 :
Polynomial.coeff recurrence4Scalar1Left 58 = (114765201730165933141693608321536500188 * 10 ^ 70 + 7382531825053547069957739742583549980024061209554012745228799589462386) * 10 ^ 70 + 2696726090768896127999945140139119095395214778587672750965328414116970
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_59 :
Polynomial.coeff recurrence4Scalar1Left 59 = -((5210875159667630936719224841498579927975 * 10 ^ 70 + 6856249408647331795947989159777786803072861048405605265955119854644814) * 10 ^ 70 + 7875165961771509647075662453475601817506846425321267945540017287272128)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_60 :
Polynomial.coeff recurrence4Scalar1Left 60 = (223738594196880232461554248417531322898954 * 10 ^ 70 + 7016823691268610999203068389219404389291632299746922216999937936891549) * 10 ^ 70 + 5452978925730142787868006974668739393136901899950988218424626420984124
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_61 :
Polynomial.coeff recurrence4Scalar1Left 61 = -((9096987294408812842074380093160974537091082 * 10 ^ 70 + 3204832670381819113453642940792988055689068156606539976185468732631170) * 10 ^ 70 + 368662891600321197146854251398542174155105780570175058582533381925572)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_62 :
Polynomial.coeff recurrence4Scalar1Left 62 = (350641481928570222263478078266082979191703866 * 10 ^ 70 + 9235609072650698007686601735613198215683923741117847445691302442993742) * 10 ^ 70 + 9971172206746708703087862030096286737605837989009835841634093464442485
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_63 :
Polynomial.coeff recurrence4Scalar1Left 63 = -((12823808366569304465001724623884927802456498291 * 10 ^ 70 + 9969983796099265273748866418791053591085291967605405685769401837610523) * 10 ^ 70 + 4168215909657886497860008241588146969861930893181790973108078775779987)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_64 :
Polynomial.coeff recurrence4Scalar1Left 64 = (445284741373591801078605305672985401823601325496 * 10 ^ 70 + 5530801315266029942761163081991696212557191768215546373468357062459479) * 10 ^ 70 + 9843808370801173515709496157274526438564892382348949360444765766899993
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_65 :
Polynomial.coeff recurrence4Scalar1Left 65 = -((14685946089273671127277102050077392688640489173671 * 10 ^ 70 + 3369080307753899659948392867563739013794184714393524295305836441440582) * 10 ^ 70 + 3573338226450530566029013851835824820283823337100393178033835932774035)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_66 :
Polynomial.coeff recurrence4Scalar1Left 66 = (460121910934922548055121423059897461076770400474722 * 10 ^ 70 + 1258019505228362489233071073004623390128835813067357314083796418291910) * 10 ^ 70 + 2933449273451948981283574011047813536830572833175748483766321368409517
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_67 :
Polynomial.coeff recurrence4Scalar1Left 67 = -((13692500228338617985877875048806420663373835425181025 * 10 ^ 70 + 2615731608165097880640727509892121915318074024056398614173181858510825) * 10 ^ 70 + 1470346815514409985843539542685648913225142788783032499120439357642556)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_68 :
Polynomial.coeff recurrence4Scalar1Left 68 = (386812428029844055545897810595385365863151180546812759 * 10 ^ 70 + 4620160469540114108078017996693006107924004381483026570338740879107311) * 10 ^ 70 + 5225654811531264242027628243624435737429930960160157004798537253261952
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_69 :
Polynomial.coeff recurrence4Scalar1Left 69 = -((10362891398884054381157678296779478938966774179586587648 * 10 ^ 70 + 3120303204651012185444888839768890028628971745664567383476460472141421) * 10 ^ 70 + 3396181779674732956463888731845972429674708206745698559577191077728288)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_70 :
Polynomial.coeff recurrence4Scalar1Left 70 = (262834534570918265924859582973296467155649575441531300942 * 10 ^ 70 + 152975579874813740810233484226540240232651321417949087604842321580769) * 10 ^ 70 + 5048059233583509320184263296298291703231545068894593228816909215869509
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_71 :
Polynomial.coeff recurrence4Scalar1Left 71 = -((6293989670181592235016332602295101387829989261085438577955 * 10 ^ 70 + 4600304166630872454343665481268687728452509453689892288180394475626303) * 10 ^ 70 + 7992432390920348999397602249737382195501576748086737702988558661803898)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_72 :
Polynomial.coeff recurrence4Scalar1Left 72 = (141692697025926772899155886331354035503894189025498995750862 * 10 ^ 70 + 5115399134217000855242725012174807279109370154950764524786577064757357) * 10 ^ 70 + 5261281937729863266322240661404374283432979179499407835860932828720898
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_73 :
Polynomial.coeff recurrence4Scalar1Left 73 = -((2977984861340611018823121761970407706910997721066846574446565 * 10 ^ 70 + 7805324934295045106160888420637470993378943910155543154887642668285641) * 10 ^ 70 + 5781375178675759466112660908163798170999522144727434806741046822482320)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_74 :
Polynomial.coeff recurrence4Scalar1Left 74 = (57738442344721287215089886848936175877840210588918246766682761 * 10 ^ 70 + 408708600045991348866855012557095907504682872654688907855401071968475) * 10 ^ 70 + 340328575376606051615884953787294458326655913630536335612987862360050