Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupScalar3LeftPart0.Coefficients0To92

Recurrence 2 lookup certificate: Scalar3Left 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.recurrence2Scalar3Left_coeff_0 :
Polynomial.coeff recurrence2Scalar3Left 0 = 0
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_1 :
Polynomial.coeff recurrence2Scalar3Left 1 = -245760
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_2 :
Polynomial.coeff recurrence2Scalar3Left 2 = 687245312
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_3 :
Polynomial.coeff recurrence2Scalar3Left 3 = -9256293744576
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_4 :
Polynomial.coeff recurrence2Scalar3Left 4 = 30125217094481216
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_5 :
Polynomial.coeff recurrence2Scalar3Left 5 = -71050586121319762032
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_6 :
Polynomial.coeff recurrence2Scalar3Left 6 = 311760030220255739426608
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_7 :
Polynomial.coeff recurrence2Scalar3Left 7 = 338934473124034921396472352
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_8 :
Polynomial.coeff recurrence2Scalar3Left 8 = -372161296286781465245466607876
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_9 :
Polynomial.coeff recurrence2Scalar3Left 9 = 603742422986770487146438708710444
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_10 :
Polynomial.coeff recurrence2Scalar3Left 10 = -456718416651077057108147616929121136
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_11 :
Polynomial.coeff recurrence2Scalar3Left 11 = 278317280540231373999369627371644994768
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_12 :
Polynomial.coeff recurrence2Scalar3Left 12 = -131869353245064667288454540673336426817704
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_13 :
Polynomial.coeff recurrence2Scalar3Left 13 = 45748469501893500238647114360638762580127324
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_14 :
Polynomial.coeff recurrence2Scalar3Left 14 = -12128709964311914042867738708995566102663554032
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_15 :
Polynomial.coeff recurrence2Scalar3Left 15 = 2459054115218102255755713392975425238930980471332
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_16 :
Polynomial.coeff recurrence2Scalar3Left 16 = -384729505548982166948654861171654778370809941611896
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_17 :
Polynomial.coeff recurrence2Scalar3Left 17 = 45535789306667430074554415923027111452112235322760896
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_18 :
Polynomial.coeff recurrence2Scalar3Left 18 = -3823547880900833013131431428802165226305817965174888277
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_19 :
Polynomial.coeff recurrence2Scalar3Left 19 = 175004428538837092561553054708575013731086940907522039817
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_20 :
Polynomial.coeff recurrence2Scalar3Left 20 = 6398142727807668921588816599497444558986447853128729064391
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_21 :
Polynomial.coeff recurrence2Scalar3Left 21 = -2179402807363742550636303749448984651195103924162141914339311
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_22 :
Polynomial.coeff recurrence2Scalar3Left 22 = 245176608425451463427662055226031868551627850303688629855524249
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_23 :
Polynomial.coeff recurrence2Scalar3Left 23 = -18618980063502709257367472575574750179185365310794911661228763717
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_24 :
Polynomial.coeff recurrence2Scalar3Left 24 = 1068109329996553308050376422599327097821858002281409864901739734401
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_25 :
Polynomial.coeff recurrence2Scalar3Left 25 = -47441384615457273023222157503445983843388678138288271285931412995983
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_26 :
Polynomial.coeff recurrence2Scalar3Left 26 = 1540059667603449985033226832346467097546296323183751632404778480940538
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_27 :
Polynomial.coeff recurrence2Scalar3Left 27 = -(2 * 10 ^ 70 + 2057596737375442048129240974481777422007737454398012343917049093996872)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_28 :
Polynomial.coeff recurrence2Scalar3Left 28 = -(160 * 10 ^ 70 + 3711392152711451611967621514692520230788940312813453291491626695096234)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_29 :
Polynomial.coeff recurrence2Scalar3Left 29 = 18062 * 10 ^ 70 + 3731039818426984192014415344363698081178816960635746493360433385202710
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_30 :
Polynomial.coeff recurrence2Scalar3Left 30 = -(1108058 * 10 ^ 70 + 5988972274404202657412318490712847769337503169679000206620301804389038)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_31 :
Polynomial.coeff recurrence2Scalar3Left 31 = 49967087 * 10 ^ 70 + 6429679646239649691417753552573760073221414624939560022623878319540667
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_32 :
Polynomial.coeff recurrence2Scalar3Left 32 = -(1713394123 * 10 ^ 70 + 5146952897406614493822909311821871416645100990250275332421609428548499)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_33 :
Polynomial.coeff recurrence2Scalar3Left 33 = 40643247191 * 10 ^ 70 + 1240018961738461227092770984053346643315121551234855756511418886872395
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_34 :
Polynomial.coeff recurrence2Scalar3Left 34 = -(224627461461 * 10 ^ 70 + 1512112860241754992000107358750264107792239355346452129889032042576039)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_35 :
Polynomial.coeff recurrence2Scalar3Left 35 = -(42947228664254 * 10 ^ 70 + 2144334965758465319280485382728463509430058785165192699605777932126774)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_36 :
Polynomial.coeff recurrence2Scalar3Left 36 = 3134354329988829 * 10 ^ 70 + 6901110973877362801495978576344775269745982378768536804247339870037040
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_37 :
Polynomial.coeff recurrence2Scalar3Left 37 = -(143433832156514698 * 10 ^ 70 + 1946663384672290065004332484600209949956107870479876892718342180297556)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_38 :
Polynomial.coeff recurrence2Scalar3Left 38 = 4933223796638204263 * 10 ^ 70 + 620693561004447120307324733506150867153309222749817363997988468556571
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_39 :
Polynomial.coeff recurrence2Scalar3Left 39 = -(127872946059917261382 * 10 ^ 70 + 7246838948355878036965947593384827662991091844906069979842657215908883)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_40 :
Polynomial.coeff recurrence2Scalar3Left 40 = 2224690320310088765149 * 10 ^ 70 + 1908235475185135263553371703151235146867759194512661202420116256573490
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_41 :
Polynomial.coeff recurrence2Scalar3Left 41 = -(9352208636275718022210 * 10 ^ 70 + 3852834873375798916078767899026660917317784044378707404169693944621950)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_42 :
Polynomial.coeff recurrence2Scalar3Left 42 = -(1007972341566048561635064 * 10 ^ 70 + 7639173192316251079778411151600425858933929607984349354870047656602192)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_43 :
Polynomial.coeff recurrence2Scalar3Left 43 = 46181671834291773002447720 * 10 ^ 70 + 1308575198512383143656485117047874379561640923894564721654574822801185
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_44 :
Polynomial.coeff recurrence2Scalar3Left 44 = -(1319891967077812779628888123 * 10 ^ 70 + 5419642692182095813163840754006804328111006339158061842492829378441401)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_45 :
Polynomial.coeff recurrence2Scalar3Left 45 = 31327451792552796525757672466 * 10 ^ 70 + 7317408270089723607489678554252491740657781162627882681291405005739359
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_46 :
Polynomial.coeff recurrence2Scalar3Left 46 = -(727331151093621652333920025390 * 10 ^ 70 + 7118186533989183940466400006165453694031921241447414215501908385472631)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_47 :
Polynomial.coeff recurrence2Scalar3Left 47 = 18181002880584541846740582736254 * 10 ^ 70 + 2490224216449398454721689836623418151349583827743846416933424814325689
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_48 :
Polynomial.coeff recurrence2Scalar3Left 48 = -(474079087292926724418473427561272 * 10 ^ 70 + 5324270139942909390222863137215978335814300238492304164875957935239764)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_49 :
Polynomial.coeff recurrence2Scalar3Left 49 = 11771999972251108122944110116274285 * 10 ^ 70 + 1364871538513053393607895386496201027353341007049697674766784462265150
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_50 :
Polynomial.coeff recurrence2Scalar3Left 50 = -(261346174293242024937339792115637758 * 10 ^ 70 + 873610213342881809835690357355103611183638237936985401881697165872803)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_51 :
Polynomial.coeff recurrence2Scalar3Left 51 = 5031940621009312687011833085238619096 * 10 ^ 70 + 688014332257412528835598153890335756133498952142521901281610692285648
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_52 :
Polynomial.coeff recurrence2Scalar3Left 52 = -(82130754007047038771906828616078899611 * 10 ^ 70 + 4045770201602963205526260720844515910347287723321092679982466569747044)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_53 :
Polynomial.coeff recurrence2Scalar3Left 53 = 1084536306817753280772516725387128674919 * 10 ^ 70 + 7974675663997422203930420474732868669345965971644608838886692866210305
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_54 :
Polynomial.coeff recurrence2Scalar3Left 54 = -(9784510427231693939826234571964980428028 * 10 ^ 70 + 1988625765663025393652974930185905522179794586028054845255032120114445)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_55 :
Polynomial.coeff recurrence2Scalar3Left 55 = -(5750488658510595088669447162954449656815 * 10 ^ 70 + 6728287061737061329106597142763797009777723569791255116799836383897196)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_56 :
Polynomial.coeff recurrence2Scalar3Left 56 = 2840896520662452137193306299260353071398606 * 10 ^ 70 + 1843427073180680618658001882136045248430163835048304574612362145962969
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_57 :
Polynomial.coeff recurrence2Scalar3Left 57 = -(83341169731321662290956484358300712974087597 * 10 ^ 70 + 7199451938771797580444316071555484927993085572826198399047104795814678)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_58 :
Polynomial.coeff recurrence2Scalar3Left 58 = 1730920678101355993505253028341155448530562504 * 10 ^ 70 + 8826763943963402805532810102770334750260121916488323724942598542320309
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_59 :
Polynomial.coeff recurrence2Scalar3Left 59 = -(29713163917223402917971295612156346030453358162 * 10 ^ 70 + 9987564993685897299169565927052339118616193697399994081076022408888543)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_60 :
Polynomial.coeff recurrence2Scalar3Left 60 = 437899282647239075946203778780440414745355929952 * 10 ^ 70 + 8385884224149954747881237721523394321849714855933596309501488295569768
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_61 :
Polynomial.coeff recurrence2Scalar3Left 61 = -(5524595768264981517066942237061700763214474894040 * 10 ^ 70 + 7321529263379914539918504811059912122893137421470572627999465782093711)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_62 :
Polynomial.coeff recurrence2Scalar3Left 62 = 56948185678460688426802494670931488502758626733714 * 10 ^ 70 + 2736473575698884502192473896394493792288550205790119583746919547044535
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_63 :
Polynomial.coeff recurrence2Scalar3Left 63 = -(396328172124407472000469707653905375504151391074111 * 10 ^ 70 + 6832977091098696697153484989179652868945371775478230608822637467010398)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_64 :
Polynomial.coeff recurrence2Scalar3Left 64 = -(621005887149142592384921192149849874840117697030578 * 10 ^ 70 + 7739801773687424940342775071571933927691966931036293247858835258988140)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_65 :
Polynomial.coeff recurrence2Scalar3Left 65 = 87618736010987108224239543104735877209679448869551142 * 10 ^ 70 + 5523288531519408030285282148876975809945351940125543939410655553300244
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_66 :
Polynomial.coeff recurrence2Scalar3Left 66 = -(2063964997857926450398075459130548922795296660299383373 * 10 ^ 70 + 5436024345048438845810230668568177801588688151990467100950982164201764)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_67 :
Polynomial.coeff recurrence2Scalar3Left 67 = 35724248171161328208723973124713435850124627050507765471 * 10 ^ 70 + 2456265592158240131554351920458175247111446742171043626447308870553275
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_68 :
Polynomial.coeff recurrence2Scalar3Left 68 = -(527513824611510836694545306721378392464672888277741562973 * 10 ^ 70 + 1371831601672213236579825699579972351118872472701800884387642235027754)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_69 :
Polynomial.coeff recurrence2Scalar3Left 69 = 6988946149027836292586165725820362333223229848387302527532 * 10 ^ 70 + 1842896040150225946724181525655129091163273296121915830448226885925849
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_70 :
Polynomial.coeff recurrence2Scalar3Left 70 = -(85068447728416971702300173025293943348208641284131361050676 * 10 ^ 70 + 9518547940925781539305732348755735332649780018903062874698506739780326)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_71 :
Polynomial.coeff recurrence2Scalar3Left 71 = 963911507191639691212903573642204379156169344598023090154249 * 10 ^ 70 + 555084167036874844117715084339860882113685736726844263490362484897370
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_72 :
Polynomial.coeff recurrence2Scalar3Left 72 = -(10251729313403730120276074479586266180544349277136053132530266 * 10 ^ 70 + 8370327500278002440237446046111880114218407655259700068324793480775324)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_73 :
Polynomial.coeff recurrence2Scalar3Left 73 = 102914566201746902042910215021696123643863814457592057490310718 * 10 ^ 70 + 8846088629137240213864782209109544100687648947157517305398252368797967
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_74 :
Polynomial.coeff recurrence2Scalar3Left 74 = -(979120365354053779779598280675636051490815534805224248713448863 * 10 ^ 70 + 3126285335852912867542297211354582640099117875502443521687438700966095)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_75 :
Polynomial.coeff recurrence2Scalar3Left 75 = 8855571467083609885755367581398847405733906933704680612784342214 * 10 ^ 70 + 9148584252590661799271527147934166224705011831432576261316909919290984
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_76 :
Polynomial.coeff recurrence2Scalar3Left 76 = -(76326886423588361372130689156088414643630979451880821455761122661 * 10 ^ 70 + 6582584721239302844985022382362543107000223681713863065589236372139299)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_77 :
Polynomial.coeff recurrence2Scalar3Left 77 = 628161244608972405569101414228266327812221205348278473454421004593 * 10 ^ 70 + 4839170749728233649152169721903198817603763426843607447818595280182319
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_78 :
Polynomial.coeff recurrence2Scalar3Left 78 = -(4944108750732081274829737173855612925551257658177368175943149411637 * 10 ^ 70 + 9191014050254834806711690423637629208072503510493473006518223111629665)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_79 :
Polynomial.coeff recurrence2Scalar3Left 79 = 37263953870491220747868528518260401825231120786702889540285187286938 * 10 ^ 70 + 898517954918517094103058096183146652383489411247236054733506151741571
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_80 :
Polynomial.coeff recurrence2Scalar3Left 80 = -(269234482113354249417593310833989763124708593287623895226829574730091 * 10 ^ 70 + 2468948449543457472416356659068603260681018450106240137886724080260559)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_81 :
Polynomial.coeff recurrence2Scalar3Left 81 = 1866331191926036038808599987960202519031561977543592090014984403632639 * 10 ^ 70 + 9122327021325348313104516310231098367373110941739577532431847336739241
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_82 :
Polynomial.coeff recurrence2Scalar3Left 82 = -((1 * 10 ^ 70 + 2421543676983478364626835218362415449320410882856962403037827901279277) * 10 ^ 70 + 8037010575574319492337772758721520833698986611436946564864600701001820)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_83 :
Polynomial.coeff recurrence2Scalar3Left 83 = (7 * 10 ^ 70 + 9424186561875074830797285803764259835306991264639476259990641103494073) * 10 ^ 70 + 2886763208486711646316462826158718565712148726337630471733138702403987
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_84 :
Polynomial.coeff recurrence2Scalar3Left 84 = -((48 * 10 ^ 70 + 8128876780736136679619153810497174994769517701346413834517600756675673) * 10 ^ 70 + 9648133810543434615408011092894350232956027340221519649565836865644963)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_85 :
Polynomial.coeff recurrence2Scalar3Left 85 = (288 * 10 ^ 70 + 4583555775376393159428873936933558507374491089298079907531032274674260) * 10 ^ 70 + 6219327554703322469927993193537759779214867573748207710525019750504551
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_86 :
Polynomial.coeff recurrence2Scalar3Left 86 = -((1639 * 10 ^ 70 + 4541863226844702405186963501503114766531727573534323315429060310470245) * 10 ^ 70 + 9505602863807752581411736845558392626694747671781154296268778199034485)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_87 :
Polynomial.coeff recurrence2Scalar3Left 87 = (8962 * 10 ^ 70 + 1230735438752633436863020284877156335428964841711466963212634963531006) * 10 ^ 70 + 4715203882529490512315181435259765585334565405605550886471883418653349
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_88 :
Polynomial.coeff recurrence2Scalar3Left 88 = -((47115 * 10 ^ 70 + 7069318047299819360231910968385873018094013189547479024148068319717008) * 10 ^ 70 + 1401788653534415995740575915093694042714822102318863269048470442338926)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_89 :
Polynomial.coeff recurrence2Scalar3Left 89 = (238138 * 10 ^ 70 + 3576497312540170336968610577202958655422709036794390217529272780917643) * 10 ^ 70 + 8480677985342958135306687964312451993295977826403268803281369406890338
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_90 :
Polynomial.coeff recurrence2Scalar3Left 90 = -((1156607 * 10 ^ 70 + 3348835319110668265951497574604253866696968400045048104916348773239066) * 10 ^ 70 + 6742403946821895053550605871368062147579640971589466492210519932330306)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_91 :
Polynomial.coeff recurrence2Scalar3Left 91 = (5394253 * 10 ^ 70 + 1684234993015372976951940990338806509992266196763260292259750194227023) * 10 ^ 70 + 3220000916755377329271418582561661212119067751959561322043155202562814
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_92 :
Polynomial.coeff recurrence2Scalar3Left 92 = -((24134776 * 10 ^ 70 + 6430055112302294871553258127315624339222251367162639466430990326121522) * 10 ^ 70 + 3773623959900046007268680068994182600924517601496585375560632327868620)