Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupB5A5Part0

Recurrence 2 lookup certificate: B5A5 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.recurrence2B5A5_coeff_0 :
Polynomial.coeff recurrence2B5A5 0 = -512
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_1 :
Polynomial.coeff recurrence2B5A5 1 = -196128
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_2 :
Polynomial.coeff recurrence2B5A5 2 = -7055788656
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_3 :
Polynomial.coeff recurrence2B5A5 3 = -3612890666128
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_4 :
Polynomial.coeff recurrence2B5A5 4 = 76638530985305740
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_5 :
Polynomial.coeff recurrence2B5A5 5 = -49420793424090909278
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_6 :
Polynomial.coeff recurrence2B5A5 6 = 40234244025010885088378
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_7 :
Polynomial.coeff recurrence2B5A5 7 = -16364375868967617715366912
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_8 :
Polynomial.coeff recurrence2B5A5 8 = 3540413305976529654299628632
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_9 :
Polynomial.coeff recurrence2B5A5 9 = -488649306782244962367000456098
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_10 :
Polynomial.coeff recurrence2B5A5 10 = 27413141233688613713804505773149
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_11 :
Polynomial.coeff recurrence2B5A5 11 = 2078138115228199855230217348907956
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_12 :
Polynomial.coeff recurrence2B5A5 12 = -529718667137543942424510307977277764
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_13 :
Polynomial.coeff recurrence2B5A5 13 = 49129835742333086315485517958639139220
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_14 :
Polynomial.coeff recurrence2B5A5 14 = -2515033458837774333831232670196051276410
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_15 :
Polynomial.coeff recurrence2B5A5 15 = 73146675109004402483767023223379711917464
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_16 :
Polynomial.coeff recurrence2B5A5 16 = -994429192235986021562928709112170887819217
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_17 :
Polynomial.coeff recurrence2B5A5 17 = -11413902045459441908704740518889256713451911
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_18 :
Polynomial.coeff recurrence2B5A5 18 = 2361458920843340991995088066376137404706402264
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_19 :
Polynomial.coeff recurrence2B5A5 19 = -223337871052218084246323960420046579701798325186
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_20 :
Polynomial.coeff recurrence2B5A5 20 = 11990460634996562695988049895446206742107702022823
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_21 :
Polynomial.coeff recurrence2B5A5 21 = -343838849377239996889606191237786904874793016634394
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_22 :
Polynomial.coeff recurrence2B5A5 22 = 3339764398508232132735899709948397381295078501587401
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_23 :
Polynomial.coeff recurrence2B5A5 23 = 84044448916700659153379810250901826600389029688942250
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_24 :
Polynomial.coeff recurrence2B5A5 24 = -1238320231714889262511150558464513461716719766914251627
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_25 :
Polynomial.coeff recurrence2B5A5 25 = -141089396206125699604979111233618145829382604133536305231
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_26 :
Polynomial.coeff recurrence2B5A5 26 = 8144090826294108282046575551249976371968719839357366792889
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_27 :
Polynomial.coeff recurrence2B5A5 27 = -247034177303386705018466872810404661751311596489844379007078
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_28 :
Polynomial.coeff recurrence2B5A5 28 = 5509518452187685069728122817415103964146228013831050078780499
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_29 :
Polynomial.coeff recurrence2B5A5 29 = -106304640900748874444981514460756869131722284206216467552195115
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_30 :
Polynomial.coeff recurrence2B5A5 30 = 1949698292728179051563636383213056763217236508321406254953500406
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_31 :
Polynomial.coeff recurrence2B5A5 31 = -33666377149688577570885822714034223630435090640848285267171847112
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_32 :
Polynomial.coeff recurrence2B5A5 32 = 502112714783096507034788594249026839013515544108483929667799440890
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_33 :
Polynomial.coeff recurrence2B5A5 33 = -5698999690180563856610771025438848654577321482072508688712432089482
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_34 :
Polynomial.coeff recurrence2B5A5 34 = 33757215789350542260114290077277540257179546617911581621595183273501
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_35 :
Polynomial.coeff recurrence2B5A5 35 = 393353013776651175946970386105279731890185261193103006583944928668829
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_36 :
Polynomial.coeff recurrence2B5A5 36 = -(1 * 10 ^ 70 + 7294456461931462787302965215573458925677000150672914281851012643274106)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_37 :
Polynomial.coeff recurrence2B5A5 37 = 36 * 10 ^ 70 + 6801165073762642670964967731412479538933435301708975512002423386240324
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_38 :
Polynomial.coeff recurrence2B5A5 38 = -(611 * 10 ^ 70 + 5619133074897808933740127140061069797545235432885064410557575197981869)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_39 :
Polynomial.coeff recurrence2B5A5 39 = 8850 * 10 ^ 70 + 2516000292433209229048961645294594982018060347785010687517011538810560
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_40 :
Polynomial.coeff recurrence2B5A5 40 = -(114566 * 10 ^ 70 + 8268526375944511145050611313047211002081493140972759706972344914278109)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_41 :
Polynomial.coeff recurrence2B5A5 41 = 1339547 * 10 ^ 70 + 1092926106489556310071624690227207638056643883750800583928472301093272
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_42 :
Polynomial.coeff recurrence2B5A5 42 = -(14246394 * 10 ^ 70 + 3053152952050798316763955989349426829592179700145229595103682879712145)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_43 :
Polynomial.coeff recurrence2B5A5 43 = 139196139 * 10 ^ 70 + 5285988047733270917688173204813473721323221884026785803613308715712063
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_44 :
Polynomial.coeff recurrence2B5A5 44 = -(1263386635 * 10 ^ 70 + 2555040234010374836089867126520647086470566961242302791875733412906526)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_45 :
Polynomial.coeff recurrence2B5A5 45 = 10732168877 * 10 ^ 70 + 5436264412772173729807127907381351282711948457848908825947630986056461
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_46 :
Polynomial.coeff recurrence2B5A5 46 = -(85452361286 * 10 ^ 70 + 4195447832441948004586242082383438596991915759148769708558000489803761)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_47 :
Polynomial.coeff recurrence2B5A5 47 = 636440723477 * 10 ^ 70 + 1044631631524470586196420583424854092079211737460467700884828514271190
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_48 :
Polynomial.coeff recurrence2B5A5 48 = -(4431343930180 * 10 ^ 70 + 8030270270324116480417042959327092652455862867288479792923416202287831)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_49 :
Polynomial.coeff recurrence2B5A5 49 = 28950711388686 * 10 ^ 70 + 5680033309382179803867387625304772664036368270461437756256009896758212
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_50 :
Polynomial.coeff recurrence2B5A5 50 = -(178580339859835 * 10 ^ 70 + 4819299078030145019193311201523261867501168176586608783489869762646370)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_51 :
Polynomial.coeff recurrence2B5A5 51 = 1044302986250442 * 10 ^ 70 + 4114279755193451428663342669678473543194844615774169436029470255861617
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_52 :
Polynomial.coeff recurrence2B5A5 52 = -(5781233198228835 * 10 ^ 70 + 442178956298599425354975652772218706750778627579089786586226241896617)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_53 :
Polynomial.coeff recurrence2B5A5 53 = 30122657881116622 * 10 ^ 70 + 5599995611807241397627532635293809852582991889319554707878452208112264
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_54 :
Polynomial.coeff recurrence2B5A5 54 = -(146891329198516626 * 10 ^ 70 + 6215991400987827015438957905490046850955114152529811891934045068210727)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_55 :
Polynomial.coeff recurrence2B5A5 55 = 670385955927150971 * 10 ^ 70 + 1356641854343164763619512757373060950883893291228024834593410526118459
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_56 :
Polynomial.coeff recurrence2B5A5 56 = -(2893383779316657063 * 10 ^ 70 + 6937062634224901487306754976960304223341147410792646576756885244286293)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_57 :
Polynomial.coeff recurrence2B5A5 57 = 12042839746609859004 * 10 ^ 70 + 329452763889807759145936048322697719333640640270700082517088578708309
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_58 :
Polynomial.coeff recurrence2B5A5 58 = -(48729548995213541657 * 10 ^ 70 + 1795860800098839280736728973442954585111547764311705696894059471156722)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_59 :
Polynomial.coeff recurrence2B5A5 59 = 184048556909700639878 * 10 ^ 70 + 6138817478225033435762842450408436826850499905112320857439592836036164
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_60 :
Polynomial.coeff recurrence2B5A5 60 = -(582768276361264140390 * 10 ^ 70 + 7066976207048479980519682281810024783124421745989044409166018600105232)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_61 :
Polynomial.coeff recurrence2B5A5 61 = 1309307530644466238292 * 10 ^ 70 + 290052624677434039733331633076022965987740686228554447555304623870980
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_62 :
Polynomial.coeff recurrence2B5A5 62 = -(2012260670167729121649 * 10 ^ 70 + 2110656780510929024541370794798323972430497495172524819170264631370971)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_63 :
Polynomial.coeff recurrence2B5A5 63 = 10312025452356734163176 * 10 ^ 70 + 2416344361292935257483304520649466886358614787589956072489457853629611
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_64 :
Polynomial.coeff recurrence2B5A5 64 = -(90484595353495780752015 * 10 ^ 70 + 5661155956101495240462445104302582089657133398969634413835354035838261)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_65 :
Polynomial.coeff recurrence2B5A5 65 = 330703686398681817994904 * 10 ^ 70 + 995836542248279888324267394488695406039696388217678442579209533176765
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_66 :
Polynomial.coeff recurrence2B5A5 66 = 549585703060654658135064 * 10 ^ 70 + 3004451799673560375316139127271050011851761062897678817950961099610432
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_67 :
Polynomial.coeff recurrence2B5A5 67 = -(10022114108828658645969014 * 10 ^ 70 + 2122855265381314736258559756451391508693999587639755972378699736890589)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_68 :
Polynomial.coeff recurrence2B5A5 68 = 32690436232669074248932938 * 10 ^ 70 + 6423908953302472043829498127974939130793678540896304971196830508172884
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_69 :
Polynomial.coeff recurrence2B5A5 69 = 33484773678803146345776055 * 10 ^ 70 + 3138255360589762641455205779664875472297567231527419531919150762415278
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_70 :
Polynomial.coeff recurrence2B5A5 70 = -(512124242060910882740147025 * 10 ^ 70 + 4096247085927483700833822087981613745972782171619544163598788601869957)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_71 :
Polynomial.coeff recurrence2B5A5 71 = 883378205697864783360569103 * 10 ^ 70 + 3315290787004148782718702571287112377779781169256095254491647010431802
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_72 :
Polynomial.coeff recurrence2B5A5 72 = 1854938110861690296029793834 * 10 ^ 70 + 9358457777517276755116686082207389689556259522118949295827601033013705
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_73 :
Polynomial.coeff recurrence2B5A5 73 = 2404904517652049818747318659 * 10 ^ 70 + 6385492411485499263321782585228875721251726247182958549857526838925893
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_74 :
Polynomial.coeff recurrence2B5A5 74 = -(20813338234613734708403321312 * 10 ^ 70 + 2778656574527874413641048194776586876608619397999285636971857543995919)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_75 :
Polynomial.coeff recurrence2B5A5 75 = -(687943900928278828945898393727 * 10 ^ 70 + 1413085476667554689035764697290035962427084528579810316307654801010129)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_76 :
Polynomial.coeff recurrence2B5A5 76 = 5438466589811649217440221110876 * 10 ^ 70 + 3301634799213953554761926274925696512820855673980664537556665914568104
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_77 :
Polynomial.coeff recurrence2B5A5 77 = -(4888661427271195343429335547994 * 10 ^ 70 + 2751424688639078226790651470708738959249026108761306736838266819864764)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_78 :
Polynomial.coeff recurrence2B5A5 78 = -(125765047240486500365698327816461 * 10 ^ 70 + 6392368624055119569980110128844673456077779558202299749679085287821877)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_79 :
Polynomial.coeff recurrence2B5A5 79 = 660241298695173323706040910023909 * 10 ^ 70 + 6200547603278575983348994583584452228927130026872050575255707835299364
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_80 :
Polynomial.coeff recurrence2B5A5 80 = -(45115928433582491090350496767041 * 10 ^ 70 + 9009399298158183141570472313050523204201884558645349490151029164935491)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_81 :
Polynomial.coeff recurrence2B5A5 81 = -(12502117024948274438277835064561688 * 10 ^ 70 + 2268670007625222028306432525293763953236223755399704485416546337025757)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_82 :
Polynomial.coeff recurrence2B5A5 82 = 46924743289043251861852685840785785 * 10 ^ 70 + 6701118631387370194329843298688979983397331849960720983754004737998668
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_83 :
Polynomial.coeff recurrence2B5A5 83 = 41455641286725217259936234640223761 * 10 ^ 70 + 7099086735305615737784926861097085148590847595018905755294177850072633
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_84 :
Polynomial.coeff recurrence2B5A5 84 = -(866540666595846629922104917744723840 * 10 ^ 70 + 785423321899303801146570557115342690339088942054904630410018911584788)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_85 :
Polynomial.coeff recurrence2B5A5 85 = 2138153772143649385560125475149517665 * 10 ^ 70 + 9547051158250049987923832423971618706576047399208792566282241686634292
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_86 :
Polynomial.coeff recurrence2B5A5 86 = 5873633165026873320984332379100395519 * 10 ^ 70 + 1939060995260928732160952186450195834360703778548740857974455261501417
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_87 :
Polynomial.coeff recurrence2B5A5 87 = -(46962457350173792837783388456976017482 * 10 ^ 70 + 2230935996789099129344954541955012944034506815704037249791424395675932)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_88 :
Polynomial.coeff recurrence2B5A5 88 = 52317925878723617353115150557676447707 * 10 ^ 70 + 7121081987088475166107870507704542227397763596610735816581217601441130
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_89 :
Polynomial.coeff recurrence2B5A5 89 = 505306753465437557167184303071616218039 * 10 ^ 70 + 6708811380225452158689542040566149278739611815019211592841036641868396
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_90 :
Polynomial.coeff recurrence2B5A5 90 = -(2202261449535010434163968064449512162791 * 10 ^ 70 + 8050786445327090195412725429132338058495504298172541498474542320581127)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_91 :
Polynomial.coeff recurrence2B5A5 91 = -(461761154426498668205086701151368638942 * 10 ^ 70 + 3550063674492397096921471902040393393825911153233560099114588862165407)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_92 :
Polynomial.coeff recurrence2B5A5 92 = 31977416377101920048553167418484054667234 * 10 ^ 70 + 1466874661113294784338129347080566789163474448047527346143022194828129
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_93 :
Polynomial.coeff recurrence2B5A5 93 = -(96447869995230567912752327918653666844960 * 10 ^ 70 + 5479302688685278985268922566509540457002064494171118781668820452828246)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_94 :
Polynomial.coeff recurrence2B5A5 94 = -(104536145826807997807115943201096874419200 * 10 ^ 70 + 7848871698979431205044655061953139355622671362859335895245996234073843)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_95 :
Polynomial.coeff recurrence2B5A5 95 = 1573367650147263580072359311233355797767655 * 10 ^ 70 + 5875106249716526937211656132287572551824236694866008961751718160516135
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_96 :
Polynomial.coeff recurrence2B5A5 96 = -(3978443746927996523155262065257612940926229 * 10 ^ 70 + 2226438312754317374870459170902411965518168008034768374021271186828480)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_97 :
Polynomial.coeff recurrence2B5A5 97 = -(5264601326761235880905001385479440741621568 * 10 ^ 70 + 8741731558492990534823729378944158075787305281519145572126108240095001)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_98 :
Polynomial.coeff recurrence2B5A5 98 = 62989457922188747333126280852545001330565412 * 10 ^ 70 + 5589478656417350081603199121058788287627559850711523059102042210272309
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_99 :
Polynomial.coeff recurrence2B5A5 99 = -(152228129947026790140370756113630363811684514 * 10 ^ 70 + 9409784843572759198823639447850326886588256684088245442609492448831601)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_100 :
Polynomial.coeff recurrence2B5A5 100 = -(167385292790887862063061754843699209562100112 * 10 ^ 70 + 1925407670018496626679792952406454805806670293390431640193126084880930)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_101 :
Polynomial.coeff recurrence2B5A5 101 = 2147880835150847994138379480283643842377642321 * 10 ^ 70 + 2062115809981214299375469930401018361567371679417953754059415418839319
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_102 :
Polynomial.coeff recurrence2B5A5 102 = -(5494623877420088579254490888705822446615587084 * 10 ^ 70 + 3939401275783115394678823457277113562176583584522885960758332095352338)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_103 :
Polynomial.coeff recurrence2B5A5 103 = -(2801353061546769508040666130786487613559974421 * 10 ^ 70 + 9923184386866642813990986158786999004407088936967392943419025219695920)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_104 :
Polynomial.coeff recurrence2B5A5 104 = 62499730823457233507900941407091275293484920376 * 10 ^ 70 + 1727125655462618325538866478494968248935789398079899691357656197035931
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_105 :
Polynomial.coeff recurrence2B5A5 105 = -(185664109930140299481737969322693150079597930461 * 10 ^ 70 + 3840098003079233313689281463710099957714429303989458834896474137267277)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_106 :
Polynomial.coeff recurrence2B5A5 106 = 60508186038433147621410291390990134861162280578 * 10 ^ 70 + 863032141810914184822328317293239212025092446288221446018263700737783
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_107 :
Polynomial.coeff recurrence2B5A5 107 = 1445727324665536949873882282826177199838408247820 * 10 ^ 70 + 7628970148506408252741329581817568959793303553863795013173938828818266
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_108 :
Polynomial.coeff recurrence2B5A5 108 = -(5481939719986811448183527340715528045462701330210 * 10 ^ 70 + 9783885511987216987784455360028171946401453447496016417532427095981202)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_109 :
Polynomial.coeff recurrence2B5A5 109 = 6687225982244327002398160479049647100492319993276 * 10 ^ 70 + 5937810928379501291911785819542961180845081552357488533766297513632788
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_110 :
Polynomial.coeff recurrence2B5A5 110 = 21794803711445893346563223230020283549030975949111 * 10 ^ 70 + 877787239281559223256629802933180234469328146693309946596410503422259
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_111 :
Polynomial.coeff recurrence2B5A5 111 = -(128537344573823515860825814251850354224141030072861 * 10 ^ 70 + 7876550105842506896890008298090389000020598716099483663952806671610876)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_112 :
Polynomial.coeff recurrence2B5A5 112 = 276837282412874354510705825164982584688005824422654 * 10 ^ 70 + 3458767499549862256203739577285214388591443266564841083188681200908344
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_113 :
Polynomial.coeff recurrence2B5A5 113 = 4770891539897432467085724213580522303332124043765 * 10 ^ 70 + 8218869599257814988002382007729871999793274181762954484147365952553719
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_114 :
Polynomial.coeff recurrence2B5A5 114 = -(2038606843272342957459658742486931504774367335739939 * 10 ^ 70 + 85643792930920817696253890034231180175970019430854061459312333210800)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_115 :
Polynomial.coeff recurrence2B5A5 115 = 7072816584894773207436366422914758822316623817193885 * 10 ^ 70 + 4845576826934958536552024126912392823555755062141441568641243337672163
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_116 :
Polynomial.coeff recurrence2B5A5 116 = -(10646016789721008740126969176069633355435941363945135 * 10 ^ 70 + 9970153177010394351738165237071854504554468090784480344397613245357742)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_117 :
Polynomial.coeff recurrence2B5A5 117 = -(10108359735580271902693303608865030715766867692965368 * 10 ^ 70 + 7800600033877894920143335160252089391195230049206228892756430980988133)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_118 :
Polynomial.coeff recurrence2B5A5 118 = 104558870520466199999349956567332148883338672861741214 * 10 ^ 70 + 3422160554715493986635444494810162344541154760632396861812600036353204
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_119 :
Polynomial.coeff recurrence2B5A5 119 = -(302760837749119624545599295230916723940787847864252537 * 10 ^ 70 + 5029867686598705207108784860975601426537439056351304069121434247107358)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_120 :
Polynomial.coeff recurrence2B5A5 120 = 422711544389109955843481518906490209782011011007617654 * 10 ^ 70 + 7177885256375121961127605782575343987645211138140050784569780674358589
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_121 :
Polynomial.coeff recurrence2B5A5 121 = 311072965803794884295475636191815247996894655559599821 * 10 ^ 70 + 1734830201499623783027877453566366629023491325880823021749158532362261
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_122 :
Polynomial.coeff recurrence2B5A5 122 = -(3519628598872765483350283717370279944458250313964182449 * 10 ^ 70 + 8113255697444396306285086676110537442409339778621911282583924669543218)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_123 :
Polynomial.coeff recurrence2B5A5 123 = 10623324124165816284703180362101213337050524676813918091 * 10 ^ 70 + 6627316297838418642179180419833000872063585591057492848750490211836131
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_124 :
Polynomial.coeff recurrence2B5A5 124 = -(18328563121949487226499513564651028257121794973838847931 * 10 ^ 70 + 5466871637884385839871533911121853397176884323627195829705439442924311)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_125 :
Polynomial.coeff recurrence2B5A5 125 = 8974023919204165749981836646197752100987002854760177542 * 10 ^ 70 + 1628636570281124820909059170639802099705087000590990438905536401751006
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_126 :
Polynomial.coeff recurrence2B5A5 126 = 60683729946416425780309892514589004647925259401433751380 * 10 ^ 70 + 5508015119499546491666693605071329431554148858341564766624912113181853
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_127 :
Polynomial.coeff recurrence2B5A5 127 = -(255463691729121037171467580481664923191220300740160345429 * 10 ^ 70 + 8912026291644702718672268750677147205334386709236312203524706047853337)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_128 :
Polynomial.coeff recurrence2B5A5 128 = 606543572243393734516848957764589121412451695785022833156 * 10 ^ 70 + 5216454072650744028386446925042474656423109813096384193560353788425947
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_129 :
Polynomial.coeff recurrence2B5A5 129 = -(958080272522351172082499586571422721004102243087948916880 * 10 ^ 70 + 8267876043187310442613185851935396747337831524527773126438978411918375)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_130 :
Polynomial.coeff recurrence2B5A5 130 = 695460399621480617323118227775029884243600426597402953206 * 10 ^ 70 + 8844305715294285056403859508768311465250399334811905801998954263467692
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_131 :
Polynomial.coeff recurrence2B5A5 131 = 1567723951587548541126846367561155916849247497683525453454 * 10 ^ 70 + 3789127839273236469896181634619903491805349424075355127796731355753372
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_132 :
Polynomial.coeff recurrence2B5A5 132 = -(8095755884502474779751919957718115026885445541543122544641 * 10 ^ 70 + 5439009586030065241778849176783853636619129307475619891913450454427990)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_133 :
Polynomial.coeff recurrence2B5A5 133 = 21506149044147142678809135588045111768168932129891561462563 * 10 ^ 70 + 863877428974956356731889876137628452617681324006866810005534567509138
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_134 :
Polynomial.coeff recurrence2B5A5 134 = -(43169513167468719310788489823976920270010713952248570518133 * 10 ^ 70 + 9343579772159136809484366537688460687145375816403846441234336994322297)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_135 :
Polynomial.coeff recurrence2B5A5 135 = 70415394103525877200388196607983448066179082707676636449786 * 10 ^ 70 + 6144582242908691097029425612320193704925262315670847057579500941072156
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_136 :
Polynomial.coeff recurrence2B5A5 136 = -(93179888933750955339721850079709797102476490030382719515507 * 10 ^ 70 + 2224239374254746011220806635571772692296182661609783346523779906096891)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_137 :
Polynomial.coeff recurrence2B5A5 137 = 91708479312566736806648423253530303653846102804724696569386 * 10 ^ 70 + 7863612600510908025617508866701962682074927808359336440997550814474155
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_138 :
Polynomial.coeff recurrence2B5A5 138 = -(37576001951732482216207535846932954448275181651083757898263 * 10 ^ 70 + 7441704380845435819407581335636633145515579653954021949306856294983046)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_139 :
Polynomial.coeff recurrence2B5A5 139 = -(100103156609474544090869673445340371890641276998680194648197 * 10 ^ 70 + 5629763975888291549500234251138204994651269069606711562273540636662257)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_140 :
Polynomial.coeff recurrence2B5A5 140 = 343239093126850199409266810923880763812956127035691909230815 * 10 ^ 70 + 7588071527522148754190743858863786417317427862705583765342042333879395
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_141 :
Polynomial.coeff recurrence2B5A5 141 = -(690980098621763725340786814082182642068815880733572108827186 * 10 ^ 70 + 7075212575917088856337679401744734938389912233274947238716711140748755)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_142 :
Polynomial.coeff recurrence2B5A5 142 = 1109129407487677851175861106516722343951030740824667791701334 * 10 ^ 70 + 7352227265382854579038445938443184327271255507397204734267923468599643
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_143 :
Polynomial.coeff recurrence2B5A5 143 = -(1529013062289423212879401365969267128192659865689374493890043 * 10 ^ 70 + 4362360699391505494387685600480645577207225247359634370384579539975817)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_144 :
Polynomial.coeff recurrence2B5A5 144 = 1859584225053634310869286211417725448481432170020717162132843 * 10 ^ 70 + 7814181273419172063942596781036779429943702408729129609763134622044370
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_145 :
Polynomial.coeff recurrence2B5A5 145 = -(2011317215075961494351340962022835915923937671187966192434168 * 10 ^ 70 + 4420060624743909468507100661374392437232588925919444920828476296645899)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_146 :
Polynomial.coeff recurrence2B5A5 146 = 1924612952831771395070233917109735001585396706886867624217480 * 10 ^ 70 + 3493226954118467439807332128749333266789099768831077075478782535535533
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_147 :
Polynomial.coeff recurrence2B5A5 147 = -(1592036901296927825444330876397693050583979339325035682681958 * 10 ^ 70 + 5518284332240674905529927540457694385803472480271200829789023732179868)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_148 :
Polynomial.coeff recurrence2B5A5 148 = 1064946972295092797812317873723683816227612700681325549666359 * 10 ^ 70 + 9997639275351658009663599065551326074293901361762891711920430058497377
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_149 :
Polynomial.coeff recurrence2B5A5 149 = -(440875901971212736872812383350688882379819217417589778707022 * 10 ^ 70 + 5915433452113749523599927524086640465178442361821377864985805613692931)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_150 :
Polynomial.coeff recurrence2B5A5 150 = -(164142422274706658835691488914614542392034628405314118141418 * 10 ^ 70 + 2401434226499981749700275178698778191994387492673927115843743800818346)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_151 :
Polynomial.coeff recurrence2B5A5 151 = 648025153437456784317220019643038658119138516933896880022418 * 10 ^ 70 + 4845033193928136148085770992094126998386637407472999842601064934057920
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_152 :
Polynomial.coeff recurrence2B5A5 152 = -(948140119629534616840808969400682473330237126023123945034358 * 10 ^ 70 + 213382402575974839554201509837396658565336563635920543042439513299269)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_153 :
Polynomial.coeff recurrence2B5A5 153 = 1051771277483126411177091412017410904613197809049076821790900 * 10 ^ 70 + 7054392722756323597129145797250854069360094858937811957607139166771314
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_154 :
Polynomial.coeff recurrence2B5A5 154 = -(990126751197832012635280173916724501654442171502752436207128 * 10 ^ 70 + 9529498338587504886993620821564429075128729739747832589072009157884006)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_155 :
Polynomial.coeff recurrence2B5A5 155 = 820789252702054112683085934788606507696256372999186696660648 * 10 ^ 70 + 903674665838052990301917064622792982519158332931540479017459039305036
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_156 :
Polynomial.coeff recurrence2B5A5 156 = -(606768236744900267375177945674278031122884002698666810331845 * 10 ^ 70 + 2947850488367330966872007893855147851772227798200302362802823779666109)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_157 :
Polynomial.coeff recurrence2B5A5 157 = 399678817821254759883412578517026377162076081214038789710220 * 10 ^ 70 + 1681277082460903087875720420784371451197422159665882873558968826993879
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_158 :
Polynomial.coeff recurrence2B5A5 158 = -(231172205416096983983285409492526635887787507607781219828473 * 10 ^ 70 + 3262393966256186893259204421500724798085300687262005907468297637539918)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_159 :
Polynomial.coeff recurrence2B5A5 159 = 112690599799975751598621819620240003099731877147266982929069 * 10 ^ 70 + 6002473408124197868911900916884366487607199122722530150655794127778391
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_160 :
Polynomial.coeff recurrence2B5A5 160 = -(40762053434369645662935395757595682993534955501519515882292 * 10 ^ 70 + 2262708445303468574718085798865813070387218944492936178222162293984502)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_161 :
Polynomial.coeff recurrence2B5A5 161 = 4169589151242372274043552027739937198512238908318314990761 * 10 ^ 70 + 1214460083711533136920009121189549440176452395660858354811275096657392
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_162 :
Polynomial.coeff recurrence2B5A5 162 = 9897756572368838469914250770415119348386004520657265924878 * 10 ^ 70 + 5761730848523856757391783355161271507250147496168613644298420998034077
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_163 :
Polynomial.coeff recurrence2B5A5 163 = -(12088798687349315439660253301780397506666120717294490090796 * 10 ^ 70 + 2625993756775314513017133634675764881719323770284781868750374386269628)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_164 :
Polynomial.coeff recurrence2B5A5 164 = 9528674209605353324366951819035388156853996771399484937925 * 10 ^ 70 + 5576351158608024104444087375641974042092076006829152398342526096658923
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_165 :
Polynomial.coeff recurrence2B5A5 165 = -(6082045909492992782126766409548919988818228660750720656960 * 10 ^ 70 + 4212701664400434130440457219567624739517234671123193014538160077205791)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_166 :
Polynomial.coeff recurrence2B5A5 166 = 3329378534968224915952869711204042863718687213561003482639 * 10 ^ 70 + 3361667133399304978824122091907973077499131112149362484073415742092298
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_167 :
Polynomial.coeff recurrence2B5A5 167 = -(1587859632975653034360677559561395179957681717274778495435 * 10 ^ 70 + 7843415477681565644046905817079382179235044997196316866583662261623401)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_168 :
Polynomial.coeff recurrence2B5A5 168 = 655564405273264130450923549481434063714824424671240023170 * 10 ^ 70 + 458318199050918503101132272618939666094288559433818312678068203960556
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_169 :
Polynomial.coeff recurrence2B5A5 169 = -(226453472558118999596474230769943760253357500799161312021 * 10 ^ 70 + 8498511231353842853149339635192487010012748920676356704910528631076818)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_170 :
Polynomial.coeff recurrence2B5A5 170 = 58625648371274781941207455395395452388756711289418046206 * 10 ^ 70 + 8299273689226009319288265519648688185476031583395416092279112245504262
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_171 :
Polynomial.coeff recurrence2B5A5 171 = -(5729302416722074527709154148625568130681095607061605708 * 10 ^ 70 + 9839840570744790587129317371418956001113676798093791912165952712859775)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_172 :
Polynomial.coeff recurrence2B5A5 172 = -(5235709782651674518679389748590043289673434581577840857 * 10 ^ 70 + 1044486175220024663411764204745893348311960062087925166630613535587677)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_173 :
Polynomial.coeff recurrence2B5A5 173 = 4582200271156396903317117203645928456427735769176338349 * 10 ^ 70 + 297841837557299410649287065427855275372310677639479332382848940996008
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_174 :
Polynomial.coeff recurrence2B5A5 174 = -(2401952298446584753933229781291467602678622571345139624 * 10 ^ 70 + 6787808783090641289239667232474408020945126073040171613828484563000805)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_175 :
Polynomial.coeff recurrence2B5A5 175 = 985677411404353201323607245531612942629421681952456202 * 10 ^ 70 + 5410970966409471767394859367753867007001897136806545743296708787864847
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_176 :
Polynomial.coeff recurrence2B5A5 176 = -(334824481514258366563219740130861114538906204865806677 * 10 ^ 70 + 4212848644678838646833810974928428648823786701030019038321164697617890)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_177 :
Polynomial.coeff recurrence2B5A5 177 = 94106235894983541712245006949983373082038216711349221 * 10 ^ 70 + 6887943518285479863013700581042627752108373741343891643790674682993077
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_178 :
Polynomial.coeff recurrence2B5A5 178 = -(20739032414285275493481513634443919575650549122153821 * 10 ^ 70 + 9916168928929790921184366575384303173411596543970995166581434316944164)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_179 :
Polynomial.coeff recurrence2B5A5 179 = 2834060067307601147533497066315176222810608011959334 * 10 ^ 70 + 1055627289802933936189503961855741924064847577482571382916402172535441
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_180 :
Polynomial.coeff recurrence2B5A5 180 = 220688535630019188077025806541585528267101162993529 * 10 ^ 70 + 6079748339094371980909447489436145870791717576738895337518850105147701
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_181 :
Polynomial.coeff recurrence2B5A5 181 = -(314123646666485604440753544055749747628593804491032 * 10 ^ 70 + 9844261471080193043643259040809474821869362698884973669400878677969663)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_182 :
Polynomial.coeff recurrence2B5A5 182 = 129610169257758281812656635969602764774613669964118 * 10 ^ 70 + 786863363147181389921568933858993307709366894649312935620072537633670
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_183 :
Polynomial.coeff recurrence2B5A5 183 = -(37449517741539888528515585121180099819333577095602 * 10 ^ 70 + 1223174667537092550052377350495644303880289780640852720884398789433959)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_184 :
Polynomial.coeff recurrence2B5A5 184 = 8336930703580920543561281382089166105903633195264 * 10 ^ 70 + 4380308465985345739947926914526141281538976786164460780999091285490443
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_185 :
Polynomial.coeff recurrence2B5A5 185 = -(1394019968598910021949220606435100657081021785946 * 10 ^ 70 + 5522863993779665746914735347521911921217968416140334419134405032306514)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_186 :
Polynomial.coeff recurrence2B5A5 186 = 140645446988531119719001924961257696384469636477 * 10 ^ 70 + 1959813720616926907410142570579329141454861372945972485216688492062889
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_187 :
Polynomial.coeff recurrence2B5A5 187 = 7045040302098309440176425153243645447417333812 * 10 ^ 70 + 4546365733788993513835514009805224078989818000370631989885482110901672
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_188 :
Polynomial.coeff recurrence2B5A5 188 = -(7271361280006741620864297116686179761642257990 * 10 ^ 70 + 2725044201512930144664466912872559609044517187903680387679318244054230)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_189 :
Polynomial.coeff recurrence2B5A5 189 = 1969455556162122745924130424320397789189267149 * 10 ^ 70 + 4067425776415279053976773168543013042885924222650141139246817029572351
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_190 :
Polynomial.coeff recurrence2B5A5 190 = -(349148242103567956460855304370865506344404839 * 10 ^ 70 + 7824557647983639638950737773145291744023406577555925904104153194285777)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_191 :
Polynomial.coeff recurrence2B5A5 191 = 42202240919709485453596158744773289710320561 * 10 ^ 70 + 3281811942971197333520642553388089019186578313237034565731433717978842
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_192 :
Polynomial.coeff recurrence2B5A5 192 = -(2547735052055596756079375294623372537518407 * 10 ^ 70 + 9760378638113871111464052477175914575431669587004955199692147371798433)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_193 :
Polynomial.coeff recurrence2B5A5 193 = -(246118157511574268138095826320703648465070 * 10 ^ 70 + 1015907610132757058490813459427526105004543115443554916569074384544771)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_194 :
Polynomial.coeff recurrence2B5A5 194 = 93992511154313650107373356945329907276479 * 10 ^ 70 + 8809769674028143621073672385275944277991183139940796911601407429506578
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_195 :
Polynomial.coeff recurrence2B5A5 195 = -(14153236388243137952880475325109521793518 * 10 ^ 70 + 1585937257492641984215667823907352332803344266529806529502781682518066)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_196 :
Polynomial.coeff recurrence2B5A5 196 = 1242350220787096967785004541583433298486 * 10 ^ 70 + 4988422011300904308336771682161905400483373025624265639364402357296320
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_197 :
Polynomial.coeff recurrence2B5A5 197 = -(39180630515027524310712879890681276496 * 10 ^ 70 + 3909050657575645974560978151893951369820234952326118619614176771678863)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_198 :
Polynomial.coeff recurrence2B5A5 198 = -(6071559239363060106785981334306409753 * 10 ^ 70 + 5398083183370623492976689516179067992258160451970799692436123016830022)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_199 :
Polynomial.coeff recurrence2B5A5 199 = 1068247939634884782456620841318081550 * 10 ^ 70 + 514483720870887331739945856463355838055386897875545414055102412252132
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_200 :
Polynomial.coeff recurrence2B5A5 200 = -(78160995504168717437949561779933756 * 10 ^ 70 + 4054926407005589569244237168490269233287224249407792347378949172309505)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_201 :
Polynomial.coeff recurrence2B5A5 201 = 1730048054778737671349856631330205 * 10 ^ 70 + 3848427805824495038802543144386363311956178613225807424850122079643874
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_202 :
Polynomial.coeff recurrence2B5A5 202 = 204034497266724750862656476574665 * 10 ^ 70 + 3355867102318132952799717358110414307044603816693112089573267619961852
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_203 :
Polynomial.coeff recurrence2B5A5 203 = -(20612313305516690567747711860799 * 10 ^ 70 + 7230308731295885494331970438510650676669158338015520608378486400950499)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_204 :
Polynomial.coeff recurrence2B5A5 204 = 630281626675886773609982451778 * 10 ^ 70 + 1386499228021273131459329905152231574102089510931220897857479870419749
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_205 :
Polynomial.coeff recurrence2B5A5 205 = 15428696143066533574880343833 * 10 ^ 70 + 1407149809084184627844649073346534934326384979758956408705194650272665
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_206 :
Polynomial.coeff recurrence2B5A5 206 = -(1629304320782318618716345362 * 10 ^ 70 + 3282924543958298520555060175625444421939724584557077433335385018337113)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_207 :
Polynomial.coeff recurrence2B5A5 207 = 27020529264836867674026136 * 10 ^ 70 + 3407320299091791478566809327510855125192573572874350899334295019743677
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_208 :
Polynomial.coeff recurrence2B5A5 208 = 885238383063937365790665 * 10 ^ 70 + 890184902172044604446739746808938348752801548818551304497770690274655
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_209 :
Polynomial.coeff recurrence2B5A5 209 = -(28464735335564663097533 * 10 ^ 70 + 2120129000869000421640880551360150463348800030452316980102123136742999)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_210 :
Polynomial.coeff recurrence2B5A5 210 = -(121428171715428443955 * 10 ^ 70 + 5308831206896571434101248353211616305720199861374736501020900282303830)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_211 :
Polynomial.coeff recurrence2B5A5 211 = 8000003564062630129 * 10 ^ 70 + 1072428735813389262913428610086409181211631173445105867657636704324894
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_212 :
Polynomial.coeff recurrence2B5A5 212 = 6667149733609417 * 10 ^ 70 + 7683782118665805562778812288405587186182330573713939342330760926296801
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_213 :
Polynomial.coeff recurrence2B5A5 213 = -(837229976328711 * 10 ^ 70 + 3708608716198212496760155968575481427729640925482720204763835829753790)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_214 :
Polynomial.coeff recurrence2B5A5 214 = -(1150194700862 * 10 ^ 70 + 7211815385818142308523730745936879093375620220260374456221468851440179)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_215 :
Polynomial.coeff recurrence2B5A5 215 = 34023915890 * 10 ^ 70 + 5851386290370559492904342596337569485747955386465953098881710874563979
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_216 :
Polynomial.coeff recurrence2B5A5 216 = 64250754 * 10 ^ 70 + 1311005678125917278756788964454113918013840714334408935079632999822716
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_217 :
Polynomial.coeff recurrence2B5A5 217 = -(555376 * 10 ^ 70 + 1187060285924750180376912432689161227463802305237486228577602097297955)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_218 :
Polynomial.coeff recurrence2B5A5 218 = -(935 * 10 ^ 70 + 5795371096106573372887299832420474988709115996499856642685747796117245)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_219 :
Polynomial.coeff recurrence2B5A5 219 = 4 * 10 ^ 70 + 3970408537271538877536147239046343874458798692036138828397822447884816
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5A5_coeff_220 :
Polynomial.coeff recurrence2B5A5 220 = 41437633035796276550795972156754284418344811110145717032823462056508