Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupScalar3MainPart0.Coefficients0To92

Recurrence 2 lookup certificate: Scalar3Main coefficient convolution #

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

source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_0 :
Polynomial.coeff recurrence2Scalar3Main 0 = 0
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_1 :
Polynomial.coeff recurrence2Scalar3Main 1 = -245760
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_2 :
Polynomial.coeff recurrence2Scalar3Main 2 = -1311992320
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_3 :
Polynomial.coeff recurrence2Scalar3Main 3 = 15309813383136
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_4 :
Polynomial.coeff recurrence2Scalar3Main 4 = 75631528883148544
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_5 :
Polynomial.coeff recurrence2Scalar3Main 5 = 271674164254755462272
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_6 :
Polynomial.coeff recurrence2Scalar3Main 6 = 51568935578271997340632
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_7 :
Polynomial.coeff recurrence2Scalar3Main 7 = 394764270841824131681727984
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_8 :
Polynomial.coeff recurrence2Scalar3Main 8 = -58088187846002845877333521560
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_9 :
Polynomial.coeff recurrence2Scalar3Main 9 = 4354756223246642437773912829632
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_10 :
Polynomial.coeff recurrence2Scalar3Main 10 = -325644257316674834181757354723616
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_11 :
Polynomial.coeff recurrence2Scalar3Main 11 = -23602872492138760706393068834941981282
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_12 :
Polynomial.coeff recurrence2Scalar3Main 12 = 13265522306052799426670269555122825978344
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_13 :
Polynomial.coeff recurrence2Scalar3Main 13 = -6330471829925992442926744533082033760930028
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_14 :
Polynomial.coeff recurrence2Scalar3Main 14 = 1922287186365074682972795392149898577288561856
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_15 :
Polynomial.coeff recurrence2Scalar3Main 15 = -444247922720559587497894708827731257275215626371
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_16 :
Polynomial.coeff recurrence2Scalar3Main 16 = 78480218586310739943961266428842541323090812784831
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_17 :
Polynomial.coeff recurrence2Scalar3Main 17 = -10710283776665076329832858548470947425732812068078443
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_18 :
Polynomial.coeff recurrence2Scalar3Main 18 = 1126575424414204354197440921581550758587724833659305554
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_19 :
Polynomial.coeff recurrence2Scalar3Main 19 = -88073231685375457542935853044498048485253862089421839547
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_20 :
Polynomial.coeff recurrence2Scalar3Main 20 = 4683015102321041169192232790198483407446974306383909308421
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_21 :
Polynomial.coeff recurrence2Scalar3Main 21 = -104284078421291561932768727206338131440827945483353340761144
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_22 :
Polynomial.coeff recurrence2Scalar3Main 22 = -7579946663234040830810074100376587993754108563103976680955241
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_23 :
Polynomial.coeff recurrence2Scalar3Main 23 = 901759311704842513829284094333003996486686541286904865385320195
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_24 :
Polynomial.coeff recurrence2Scalar3Main 24 = -35729763379853399161267607759076708586457891815405780244323280779
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_25 :
Polynomial.coeff recurrence2Scalar3Main 25 = -1000263313359525976321882487756350780577972402473385342015745054109
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_26 :
Polynomial.coeff recurrence2Scalar3Main 26 = 243398801024327857543664047081766683664295359819489144324955638204646
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_27 :
Polynomial.coeff recurrence2Scalar3Main 27 = -(1 * 10 ^ 70 + 8458003714193447565318022088395281778530070433424433078154780705736229)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_28 :
Polynomial.coeff recurrence2Scalar3Main 28 = 80 * 10 ^ 70 + 8255101880701443171687727983152638435968872145198849602159849579894179
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_29 :
Polynomial.coeff recurrence2Scalar3Main 29 = -(1140 * 10 ^ 70 + 3188351929780232647906802221570056793279724912920014630455687188002170)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_30 :
Polynomial.coeff recurrence2Scalar3Main 30 = -(142778 * 10 ^ 70 + 1376282949187815216754182858140932403774993570342289704659789148476618)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_31 :
Polynomial.coeff recurrence2Scalar3Main 31 = 14504545 * 10 ^ 70 + 3840987844428104717738891567373082599718892282773422786595403871638193
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_32 :
Polynomial.coeff recurrence2Scalar3Main 32 = -(733501814 * 10 ^ 70 + 5262815492264368213200804537689189653643637339717844660672814109923430)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_33 :
Polynomial.coeff recurrence2Scalar3Main 33 = 17513217870 * 10 ^ 70 + 2420286179397995954377947975549108004121029192110699295955458197358812
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_34 :
Polynomial.coeff recurrence2Scalar3Main 34 = 563078368443 * 10 ^ 70 + 5898730253253831971385024523876314299672471354373526816730286309530464
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_35 :
Polynomial.coeff recurrence2Scalar3Main 35 = -(87423553119555 * 10 ^ 70 + 1521522396198998363542726331492141168799244108619885383950729745224828)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_36 :
Polynomial.coeff recurrence2Scalar3Main 36 = 5501889379195231 * 10 ^ 70 + 6106027895961654574939918872160719874588556597038533785623371079167032
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_37 :
Polynomial.coeff recurrence2Scalar3Main 37 = -(241319835167300312 * 10 ^ 70 + 8294454578014080453863030482897267495788396044565339777043010091064772)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_38 :
Polynomial.coeff recurrence2Scalar3Main 38 = 8075979082654781860 * 10 ^ 70 + 8766347180000188106125150110346017907890272699505358504010897349763398
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_39 :
Polynomial.coeff recurrence2Scalar3Main 39 = -(208300368214149398159 * 10 ^ 70 + 5326557497581885308067567661123185867630603967326002037800575258611638)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_40 :
Polynomial.coeff recurrence2Scalar3Main 40 = 3942655720847704878625 * 10 ^ 70 + 5164392491488193638549875504047435697294938088811547704702249784915514
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_41 :
Polynomial.coeff recurrence2Scalar3Main 41 = -(44153111236255400919835 * 10 ^ 70 + 4506785300120363135726449581498728512542521746808155578769547758173590)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_42 :
Polynomial.coeff recurrence2Scalar3Main 42 = -(148018050700570702956362 * 10 ^ 70 + 1786402723130927099878641160709430505784925978449582069348329731218404)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_43 :
Polynomial.coeff recurrence2Scalar3Main 43 = 17908834076533072589016357 * 10 ^ 70 + 2595302901545484311190590312119363408953692739757401375885946551114293
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_44 :
Polynomial.coeff recurrence2Scalar3Main 44 = -(325216933841026665200983882 * 10 ^ 70 + 6386654460486778361360616282066864735101419308037953239446613884544289)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_45 :
Polynomial.coeff recurrence2Scalar3Main 45 = -(487852107054551946007278509 * 10 ^ 70 + 8881169015385282169221203014932097400544560292323735410588162285078209)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_46 :
Polynomial.coeff recurrence2Scalar3Main 46 = 157882416744305531094111040086 * 10 ^ 70 + 1814970612897287895904074069738881441170709221299908436322628114983398
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_47 :
Polynomial.coeff recurrence2Scalar3Main 47 = -(3178070250341754040243755261061 * 10 ^ 70 + 3577627538204263624432512982284477545940339842760115920483591367028210)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_48 :
Polynomial.coeff recurrence2Scalar3Main 48 = -(25689603788054134668600257392225 * 10 ^ 70 + 4839595200611279246810047050916878156588007739015235173558973552588756)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_49 :
Polynomial.coeff recurrence2Scalar3Main 49 = 3594658928979383000695485057755748 * 10 ^ 70 + 3438115603127321094795891108884967312939329129190119156393922171769229
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_50 :
Polynomial.coeff recurrence2Scalar3Main 50 = -(133765867343342917505890315501497897 * 10 ^ 70 + 3416957986207080067425456056754560881748589991326444424758566229233287)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_51 :
Polynomial.coeff recurrence2Scalar3Main 51 = 3420234522222403472599471298875946272 * 10 ^ 70 + 8946301449010154294663281788752747631665996545354268880164141334465938
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_52 :
Polynomial.coeff recurrence2Scalar3Main 52 = -(69106315696247092605933880251695264303 * 10 ^ 70 + 2199499718038458190911127592695048624393923717356530349738965960297088)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_53 :
Polynomial.coeff recurrence2Scalar3Main 53 = 1153424444419026053450213911370233093261 * 10 ^ 70 + 4275885047114291701611856704678823338808265924110721169756322972757240
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_54 :
Polynomial.coeff recurrence2Scalar3Main 54 = -(15889720578160343529594999037423083427738 * 10 ^ 70 + 8696551912231595968090682591365739731478042025337762417820953236432832)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_55 :
Polynomial.coeff recurrence2Scalar3Main 55 = 167737360310022384295187121764025475388700 * 10 ^ 70 + 4488795935151003688695875501852358164852548567219339896845361355471372
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_56 :
Polynomial.coeff recurrence2Scalar3Main 56 = -(834878349824233133943970738815337423211187 * 10 ^ 70 + 5623168198033480414896646162700804175696700525944822201286616739052500)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_57 :
Polynomial.coeff recurrence2Scalar3Main 57 = -(18614194096183298039959873750837109495746896 * 10 ^ 70 + 5021588273088444452443266932573463092871841379336482532963011654443851)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_58 :
Polynomial.coeff recurrence2Scalar3Main 58 = 765214652499646783916608851875444568635604610 * 10 ^ 70 + 2379636872651892656448747197452267519096518217252382725534332834762989
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_59 :
Polynomial.coeff recurrence2Scalar3Main 59 = -(17830021007412740676263924828713164150478634333 * 10 ^ 70 + 9668322996197399993480223094514980148383492494370004662033431519057909)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_60 :
Polynomial.coeff recurrence2Scalar3Main 60 = 331310038798715851688869252673524609802425419730 * 10 ^ 70 + 9402354061217405138578092783727952819646419397720522163542073995198160
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_61 :
Polynomial.coeff recurrence2Scalar3Main 61 = -(5288387483601610191807282987241243066749084134357 * 10 ^ 70 + 2310876688318849113455640322660424603672656763482537819653208891224427)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_62 :
Polynomial.coeff recurrence2Scalar3Main 62 = 74277414660947702584209974972533762969212731151462 * 10 ^ 70 + 5043309773770934785476208309953198236701429652469570178931236790727930
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_63 :
Polynomial.coeff recurrence2Scalar3Main 63 = -(922147780911870948127518066521202227131300462659690 * 10 ^ 70 + 4767053980232582951711032636473590427434838980047164689083631759709991)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_64 :
Polynomial.coeff recurrence2Scalar3Main 64 = 10004940697351475191825332483505154064274533804325068 * 10 ^ 70 + 9989166133704868780619773018049614467353324367944612122440804715650718
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_65 :
Polynomial.coeff recurrence2Scalar3Main 65 = -(91110929153882400569014551786448622878585253584825304 * 10 ^ 70 + 2503208452190615586132456801031730492750271318929583554272575146688341)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_66 :
Polynomial.coeff recurrence2Scalar3Main 66 = 605723289506369087678931661703864219638035348039281349 * 10 ^ 70 + 5816040082431347823376381550503534174673435249987672642918198509090544
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_67 :
Polynomial.coeff recurrence2Scalar3Main 67 = -(707669801987491593810273341508215908419619099807908309 * 10 ^ 70 + 9789205427394706836825169721067312940444150187386898370941357214632410)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_68 :
Polynomial.coeff recurrence2Scalar3Main 68 = -(66361154567105791223020280951479479659231001700886194703 * 10 ^ 70 + 9330037543811599035898916484089379577741422437413131637733552585556900)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_69 :
Polynomial.coeff recurrence2Scalar3Main 69 = 1524581352927181922033976438412367204556372094661178490485 * 10 ^ 70 + 4396669084445293364625410623623789136992571662652549880985227556633600
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_70 :
Polynomial.coeff recurrence2Scalar3Main 70 = -(24082441776638628436236131725558123158904284495816524641763 * 10 ^ 70 + 8863104061912882329806323620152391949635140858288180109288352303677968)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_71 :
Polynomial.coeff recurrence2Scalar3Main 71 = 319981957108878818665488835012985479296853833997172887910061 * 10 ^ 70 + 2717511505269486028909038392885734058888495282598687380272430362526942
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_72 :
Polynomial.coeff recurrence2Scalar3Main 72 = -(3797615266186443600656545844375942992293840121251640799169988 * 10 ^ 70 + 9503950125731146350549275216408063846381046306290146077020808410188632)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_73 :
Polynomial.coeff recurrence2Scalar3Main 73 = 41340776516153804701991082569869546463250745823311297649728439 * 10 ^ 70 + 2503312607967270118570587086194083302744938317292107715570050644390344
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_74 :
Polynomial.coeff recurrence2Scalar3Main 74 = -(418766817035324663714854191111524590185036232727185670315344279 * 10 ^ 70 + 7291647307452942428819570258516206052567788798123925342929360399281734)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_75 :
Polynomial.coeff recurrence2Scalar3Main 75 = 3982516472627718637649389027816136742435452691805403540693978538 * 10 ^ 70 + 3540512003576917614622709304579917914012773583520888781072815650339289
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_76 :
Polynomial.coeff recurrence2Scalar3Main 76 = -(35772901203534890970652297433613340045179301182042547880830778267 * 10 ^ 70 + 3035732035202731997357439169363321408853377237389441905980054331443799)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_77 :
Polynomial.coeff recurrence2Scalar3Main 77 = 304816307088226381429220524214338299806416130121864222487305496621 * 10 ^ 70 + 5203402047871717633953163653822801295752493993664076102863747485672175
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_78 :
Polynomial.coeff recurrence2Scalar3Main 78 = -(2471669456544676759824767268595084137972625308667788995328269285611 * 10 ^ 70 + 2251943279044739825876588252785238211776171328221231516565164583620607)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_79 :
Polynomial.coeff recurrence2Scalar3Main 79 = 19117764382591653848727237650198034299579412829623393691709594181687 * 10 ^ 70 + 6044627074734369696987149608755777796572018192105009393366339375849232
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_80 :
Polynomial.coeff recurrence2Scalar3Main 80 = -(141301888830277807391794390714681700826531076660018973532432258506188 * 10 ^ 70 + 2277532928165228491333780742128357456439494856955784105935296439122255)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_81 :
Polynomial.coeff recurrence2Scalar3Main 81 = 999341727611627107350634841081280675251489912335934674727830547373700 * 10 ^ 70 + 1702405589150329256617225173326219119691032178436903490682637116099696
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_82 :
Polynomial.coeff recurrence2Scalar3Main 82 = -(6770339176035814903189342414514032683032991831412257118616850578085321 * 10 ^ 70 + 8732677033736694458609881885005304516277749475158774706338028298405228)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_83 :
Polynomial.coeff recurrence2Scalar3Main 83 = (4 * 10 ^ 70 + 3978355075972550212350258695276509098747709840058443361851905362054427) * 10 ^ 70 + 2703184587955548833873257343716886709547124145005172537605632431543053
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_84 :
Polynomial.coeff recurrence2Scalar3Main 84 = -((27 * 10 ^ 70 + 4122871150705538237390564269945971351491235739202216709156643887264774) * 10 ^ 70 + 4780028998422874059765383960170897230420357042839679286530782710318134)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_85 :
Polynomial.coeff recurrence2Scalar3Main 85 = (164 * 10 ^ 70 + 629366693320983062116141341673005770526214350849685690069845576223586) * 10 ^ 70 + 6018567684340532884215781492187250760132540142515907776164366193779428
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_86 :
Polynomial.coeff recurrence2Scalar3Main 86 = -((943 * 10 ^ 70 + 2481593584546441267097643292023792598908493890321530330005505667795626) * 10 ^ 70 + 7643216248790363618597657031740189653249684758747332221671708897474253)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_87 :
Polynomial.coeff recurrence2Scalar3Main 87 = (5210 * 10 ^ 70 + 3345960869256264098112254672605545012219275673570816995704599497219609) * 10 ^ 70 + 1444003754188771737936315199697554940657867083318261795262625665577213
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_88 :
Polynomial.coeff recurrence2Scalar3Main 88 = -((27648 * 10 ^ 70 + 5714411997741965122944441527097976641021710769314753426129634638609847) * 10 ^ 70 + 1538706063919804213896446904983034307596076831097169289853967688804500)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_89 :
Polynomial.coeff recurrence2Scalar3Main 89 = (140887 * 10 ^ 70 + 2307514964015034376695173348516686156610736447900092359725505306854649) * 10 ^ 70 + 9219168381439987367659654212494101095162417045797168399219932708191093
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_90 :
Polynomial.coeff recurrence2Scalar3Main 90 = -((688970 * 10 ^ 70 + 7865903080167333034015121548787041144487784217678169583223599419964242) * 10 ^ 70 + 651166483111418530904672246537303380317029251393924927449326582680355)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_91 :
Polynomial.coeff recurrence2Scalar3Main 91 = (3231055 * 10 ^ 70 + 843049410789766319514741882297757340879152264964558918882570548847267) * 10 ^ 70 + 1288517010305836840704505689675121601264773456134939880068792671076922
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_92 :
Polynomial.coeff recurrence2Scalar3Main 92 = -((14518587 * 10 ^ 70 + 8562852510669818494698714551422713837187027828811042175874312216634628) * 10 ^ 70 + 2290328757678049121423509148344197970842302144989154682670707302240386)