Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence4LookupScalar2FirstPart0.Coefficients0To52

Recurrence 4 lookup certificate: Scalar2First 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.recurrence4Scalar2First_coeff_0 :
Polynomial.coeff recurrence4Scalar2First 0 = 0
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_1 :
Polynomial.coeff recurrence4Scalar2First 1 = -4478585163154794200093651455596016765017858048
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_2 :
Polynomial.coeff recurrence4Scalar2First 2 = 26930821020513676202167999028265183488289416543232
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_3 :
Polynomial.coeff recurrence4Scalar2First 3 = -60537483962024339189216517869488293995417400461486592
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_4 :
Polynomial.coeff recurrence4Scalar2First 4 = 45344773146786063916402308011398880709253200494285345280
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_5 :
Polynomial.coeff recurrence4Scalar2First 5 = 58827588115646807780566651106555902852566093494674698122032
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_6 :
Polynomial.coeff recurrence4Scalar2First 6 = -168419459268969594906586497535741075898426227198070632123956200
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_7 :
Polynomial.coeff recurrence4Scalar2First 7 = 170798540160019085925271793170513679335573070010390213175796117336
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_8 :
Polynomial.coeff recurrence4Scalar2First 8 = -88613814129859775596556440053216104877274564991670273733510432590884
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_9 :
Polynomial.coeff recurrence4Scalar2First 9 = 2 * 10 ^ 70 + 2197902270774629782629746149751946765359719793984068103784360621949864
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_10 :
Polynomial.coeff recurrence4Scalar2First 10 = -(191 * 10 ^ 70 + 4730666793398846485585189004306448134202250450516612101520680770663760)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_11 :
Polynomial.coeff recurrence4Scalar2First 11 = 58203 * 10 ^ 70 + 8729818254351199303456645106378513537890789297296632310506929289797708
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_12 :
Polynomial.coeff recurrence4Scalar2First 12 = -(61887210 * 10 ^ 70 + 5858818984124381163768695670766883429385988878824215301890639874781340)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_13 :
Polynomial.coeff recurrence4Scalar2First 13 = 15926107419 * 10 ^ 70 + 6129725699561108403785526177959178017228555283708238048481940445258400
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_14 :
Polynomial.coeff recurrence4Scalar2First 14 = -(3752911519780 * 10 ^ 70 + 1482795568368662308898011144585992306493816296200800694768335784469262)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_15 :
Polynomial.coeff recurrence4Scalar2First 15 = 9975982715564966 * 10 ^ 70 + 8471743437389032751889676335359485784544858278811770079690584736338142
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_16 :
Polynomial.coeff recurrence4Scalar2First 16 = -(9794654786324610378 * 10 ^ 70 + 4261802795128624963456996086132463128039142050185115771912466144792680)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_17 :
Polynomial.coeff recurrence4Scalar2First 17 = 4629480631418272854493 * 10 ^ 70 + 6383297964105696224855317445392735955805367703306990380142219265054884
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_18 :
Polynomial.coeff recurrence4Scalar2First 18 = -(917981163334058445488403 * 10 ^ 70 + 749565633929741975987096560601582196692634524236201552663679509706845)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_19 :
Polynomial.coeff recurrence4Scalar2First 19 = -(246511251437454678024846003 * 10 ^ 70 + 4059812271182549405936611934566606187822925796755862376633856554505771)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_20 :
Polynomial.coeff recurrence4Scalar2First 20 = 265665324932310552040065787035 * 10 ^ 70 + 2807058050182328521021660709281258364656291998128919833066253160439059
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_21 :
Polynomial.coeff recurrence4Scalar2First 21 = -(111229781878794774010969828879737 * 10 ^ 70 + 4985714598505628705002712882342438576265601024291806113166173847445295)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_22 :
Polynomial.coeff recurrence4Scalar2First 22 = 30302458927473172850141526325596461 * 10 ^ 70 + 9764748995072444781107528717377706502962506328131715317204566605693807
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_23 :
Polynomial.coeff recurrence4Scalar2First 23 = -(5826418333706457367261473042901998305 * 10 ^ 70 + 6382496226664340740377836082412473829628454299490057236481457344724538)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_24 :
Polynomial.coeff recurrence4Scalar2First 24 = 817745936670760360649400287908521654936 * 10 ^ 70 + 3567068633004814752793934445915552440142375877378816718801695747317140
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_25 :
Polynomial.coeff recurrence4Scalar2First 25 = -(112621853985428674618538126610592137237418 * 10 ^ 70 + 8847119683711328220362236916359138604240195519212483752845609015937635)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_26 :
Polynomial.coeff recurrence4Scalar2First 26 = 33786567579532122210595669873551197032125815 * 10 ^ 70 + 2231953986039610948795978291396566793120089686245281314610668238700449
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_27 :
Polynomial.coeff recurrence4Scalar2First 27 = -(14467625342537742175796517399980975003422549018 * 10 ^ 70 + 6545565494037990081670829728281750965293262922338552392959048061263492)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_28 :
Polynomial.coeff recurrence4Scalar2First 28 = 5083343627702361234738210308202340122469403602402 * 10 ^ 70 + 6888360194839916981845843616232161849028179662235327755250446973403521
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_29 :
Polynomial.coeff recurrence4Scalar2First 29 = -(1413486306316786245742475931692056269785274448041271 * 10 ^ 70 + 4445507301222969536641484262189818495204842184673758846012889224572139)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_30 :
Polynomial.coeff recurrence4Scalar2First 30 = 322747808690968091697078353495493468746492771572467833 * 10 ^ 70 + 2118588115180150189955120078122880471643811341469569877768007562530477
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_31 :
Polynomial.coeff recurrence4Scalar2First 31 = -(62069047950206724668311559873550087106746944842746788034 * 10 ^ 70 + 403700138073149475554555033160758357157320747935156086890493409268615)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_32 :
Polynomial.coeff recurrence4Scalar2First 32 = 10142994358592368643935661186907293555053995267550348270875 * 10 ^ 70 + 439275285935232100351803507565792617089942385400320443012762837527405
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_33 :
Polynomial.coeff recurrence4Scalar2First 33 = -(1395501471472422315880908058860825366129089475380035215255680 * 10 ^ 70 + 5598448856484721858390328985665403565488593057225728705589832235616994)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_34 :
Polynomial.coeff recurrence4Scalar2First 34 = 155217288417022324076654730462600468835838788574902370781005971 * 10 ^ 70 + 3631726442652647059178537494720966652075834075107268784494724833966916
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_35 :
Polynomial.coeff recurrence4Scalar2First 35 = -(12106422790070300049517527185399990556538351741831458589112780718 * 10 ^ 70 + 8616576918607185796171368510053742294348843111430153355175685135267465)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_36 :
Polynomial.coeff recurrence4Scalar2First 36 = 151272691364337929251563141143482743007187032537611364240942359831 * 10 ^ 70 + 5652041336150790712636522262842281213590788001461644262815613435632210
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_37 :
Polynomial.coeff recurrence4Scalar2First 37 = 163893910867054262260415492076033131664616181893902031793510911582153 * 10 ^ 70 + 2319755055817375556317288425808643592728507912081663150207681185861176
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_38 :
Polynomial.coeff recurrence4Scalar2First 38 = -((3 * 10 ^ 70 + 8607300626520326015041025841927311674893693081287204452055900910130478) * 10 ^ 70 + 6125524966805737546707374759327773022660646534853535657109763750461257)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_39 :
Polynomial.coeff recurrence4Scalar2First 39 = (593 * 10 ^ 70 + 521234461240098784373861374030543822818271522732498892370429113838198) * 10 ^ 70 + 3370203123385275762743537540162315223573170073279906582143359207914440
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_40 :
Polynomial.coeff recurrence4Scalar2First 40 = -((71665 * 10 ^ 70 + 6642702561924097795235269001317041208310558545775640371540063572561104) * 10 ^ 70 + 6813343343534162895762142830475243599720342386934456038721082800520500)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_41 :
Polynomial.coeff recurrence4Scalar2First 41 = (7062103 * 10 ^ 70 + 1393266340853460422087467773472313000181241093761575781598180502303420) * 10 ^ 70 + 8082626467624792202626990668713283682898753219459160782942066303665732
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_42 :
Polynomial.coeff recurrence4Scalar2First 42 = -((550994181 * 10 ^ 70 + 6010274525046551347268941678800977311312133440455077966196019944546070) * 10 ^ 70 + 9609513929598321204800328659592569084639892232637570688339360335787695)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_43 :
Polynomial.coeff recurrence4Scalar2First 43 = (28596860894 * 10 ^ 70 + 53114725694848964870396263104107007710736898057890990069983371700520) * 10 ^ 70 + 5821234580264853586360597814628326483090420736614407961051650364961281
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_44 :
Polynomial.coeff recurrence4Scalar2First 44 = (220692487678 * 10 ^ 70 + 3022411957302412907758617856105230926144720982470693517035398931846448) * 10 ^ 70 + 8425403219767062409893852941451937985602866035440799668901241845460045
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_45 :
Polynomial.coeff recurrence4Scalar2First 45 = -((300269344380338 * 10 ^ 70 + 644746677824139980744126585086428924840118328612868033975483389803965) * 10 ^ 70 + 3831149306541835830987067462550543883294041116326918399018290219613783)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_46 :
Polynomial.coeff recurrence4Scalar2First 46 = (49457659447827314 * 10 ^ 70 + 1656573034966052278458595664183919394962831187392553435555672757049984) * 10 ^ 70 + 5537863291993887754584315955455243308079158250603299383494361222647624
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_47 :
Polynomial.coeff recurrence4Scalar2First 47 = -((5831870899690734757 * 10 ^ 70 + 9264645656856561104020215423412478063186410498738709554843953099350852) * 10 ^ 70 + 5212729060237072456488393225872562783398395012585859838034659292159591)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_48 :
Polynomial.coeff recurrence4Scalar2First 48 = (575533450170690840722 * 10 ^ 70 + 9818647223272149229522183890530877749064996426342761755854797909588377) * 10 ^ 70 + 5042171987155069941263361830291012925885567608862270227728409208618083
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_49 :
Polynomial.coeff recurrence4Scalar2First 49 = -((50091110474216138502719 * 10 ^ 70 + 1456026317595632490953649949875786443214407778815392021381230177793996) * 10 ^ 70 + 9082297980418718761900012016325316147737462490873217375526146675678786)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_50 :
Polynomial.coeff recurrence4Scalar2First 50 = (3941117128749189144322141 * 10 ^ 70 + 6499344951990071166036851081156905768003018523154366577355579440441361) * 10 ^ 70 + 5996217865936248340170311998796695735404352135366579054658772663669943
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_51 :
Polynomial.coeff recurrence4Scalar2First 51 = -((284276692043181283346322362 * 10 ^ 70 + 6970124051064813388102649141029264949894216035689052247820383281192845) * 10 ^ 70 + 6496425982683476767616288857512452103785321374150845375957474263026112)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_52 :
Polynomial.coeff recurrence4Scalar2First 52 = (18967636205399420665509333108 * 10 ^ 70 + 4073393477341791061611548423550310887885407743745006965665334051062034) * 10 ^ 70 + 6087150381369266741680599847731419564848490705032950566210850548159502