Recurrence 2 lookup certificate: Scalar4Left coefficient convolution #
This is a checked coefficient-lookup shard for the second pseudo-division recurrence in the order-seven certificate.
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_18 :
Polynomial.coeff recurrence2Scalar4Left 18 = -23430702017616767049471792857469124382796049633144194910
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_19 :
Polynomial.coeff recurrence2Scalar4Left 19 = 1576670171102617405145499229608703461206148315810353471742
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_20 :
Polynomial.coeff recurrence2Scalar4Left 20 = -68103763373302658199272942793891232198813260624059635503571
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_21 :
Polynomial.coeff recurrence2Scalar4Left 21 = 463556092563538155467063618731935082607760207513827681568542
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_22 :
Polynomial.coeff recurrence2Scalar4Left 22 = 212077828412794900708209573518363154141900991034532985454709394
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_23 :
Polynomial.coeff recurrence2Scalar4Left 23 = -21563634934583553774872246322045742082573292593045303297413171139
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_24 :
Polynomial.coeff recurrence2Scalar4Left 24 = 1333282281365816240105459835853696820079876161584762611236831563547
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_25 :
Polynomial.coeff recurrence2Scalar4Left 25 = -60807583974362519645261544810082714888439405592432915023027555597115
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_26 :
Polynomial.coeff recurrence2Scalar4Left 26 = 2013248388204667552906846551827887535812692456423544555763911021054225
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_27 :
Polynomial.coeff recurrence2Scalar4Left 27 = -(2 * 10 ^ 70 + 8986439423828736442110284169221325278527573123114133995972528076145794)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_28 :
Polynomial.coeff recurrence2Scalar4Left 28 = -(219 * 10 ^ 70 + 8965918132177172132082250894233577846775941695429538913394488089906654)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_29 :
Polynomial.coeff recurrence2Scalar4Left 29 = 24108 * 10 ^ 70 + 9234579868217336148394543364856094166008303690683840931012286092449629
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_30 :
Polynomial.coeff recurrence2Scalar4Left 30 = -(1408553 * 10 ^ 70 + 2378014761901078974387330247992022158452352463151475115238898772772753)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_31 :
Polynomial.coeff recurrence2Scalar4Left 31 = 58823933 * 10 ^ 70 + 154974858633850563692511011982018717561367361381028821398311436237835
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_32 :
Polynomial.coeff recurrence2Scalar4Left 32 = -(1780648013 * 10 ^ 70 + 2611747409626184656588103682290689221198567340303779096603379010227739)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_33 :
Polynomial.coeff recurrence2Scalar4Left 33 = 30134985660 * 10 ^ 70 + 126353924168788188951458650196845207550945473587614074878449319270125
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_34 :
Polynomial.coeff recurrence2Scalar4Left 34 = 655364427484 * 10 ^ 70 + 444569516868842022325174195832552171819661956300107204810584625603566
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_35 :
Polynomial.coeff recurrence2Scalar4Left 35 = -(89696341495680 * 10 ^ 70 + 2207694183813309396743050674237108893482257157405605223359026646365163)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_36 :
Polynomial.coeff recurrence2Scalar4Left 36 = 5019814753525830 * 10 ^ 70 + 7317034388221932694505695688552855551609957988663134956460776351731082
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_37 :
Polynomial.coeff recurrence2Scalar4Left 37 = -(199368843359121784 * 10 ^ 70 + 9977652421264249610583544319262247295787073541384799382810622190187490)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_38 :
Polynomial.coeff recurrence2Scalar4Left 38 = 5895326800941292117 * 10 ^ 70 + 6879268733586991591577162716296336997734894236036102860521606066865127
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_39 :
Polynomial.coeff recurrence2Scalar4Left 39 = -(117030100343280354936 * 10 ^ 70 + 2515549257020526698602540317679570767219933508003283892752348380765270)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_40 :
Polynomial.coeff recurrence2Scalar4Left 40 = 499005196038419342018 * 10 ^ 70 + 4170517570199162786169524987120085072340091290210659277813146054393497
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_41 :
Polynomial.coeff recurrence2Scalar4Left 41 = 80833446280423561797157 * 10 ^ 70 + 7362622286688572225948317898240325053252519628162058565546197175149601
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_42 :
Polynomial.coeff recurrence2Scalar4Left 42 = -(4634419049988368744655188 * 10 ^ 70 + 5033053160838156415702704440173041232413471013816907576007095662673355)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_43 :
Polynomial.coeff recurrence2Scalar4Left 43 = 175297643615179704140275767 * 10 ^ 70 + 5242732929426214177951911112327807843733894564914982933441164667554473
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_44 :
Polynomial.coeff recurrence2Scalar4Left 44 = -(5543051820028558968847251855 * 10 ^ 70 + 1771771814937978653917490282321665083603552356272986993810778698313456)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_45 :
Polynomial.coeff recurrence2Scalar4Left 45 = 157910760567086430038781225143 * 10 ^ 70 + 9261775352503345110090550347086834672432167101359008481377277080807293
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_46 :
Polynomial.coeff recurrence2Scalar4Left 46 = -(4159057175286965550827200143121 * 10 ^ 70 + 2926771075769229406420557495365992954984625820825936084126092967455717)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_47 :
Polynomial.coeff recurrence2Scalar4Left 47 = 101399590812515289185476229359571 * 10 ^ 70 + 7408971919102211087421523591420020348637617931659126143324164401139110
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_48 :
Polynomial.coeff recurrence2Scalar4Left 48 = -(2265291884852132627402505400221095 * 10 ^ 70 + 4796977560588440404197598694298174671097613700548592570859634571886991)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_49 :
Polynomial.coeff recurrence2Scalar4Left 49 = 45714549737470130831468626779449967 * 10 ^ 70 + 9950739562764966502534653630886424835895236208804422416822153986778689
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_50 :
Polynomial.coeff recurrence2Scalar4Left 50 = -(818513967386699179029688236377472048 * 10 ^ 70 + 8925538353956947665156342926069218866588714906110080440418012409918444)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_51 :
Polynomial.coeff recurrence2Scalar4Left 51 = 12627826242785478045667504706484551955 * 10 ^ 70 + 6429604983498427958578929737566587382011899048678590875384719356694394
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_52 :
Polynomial.coeff recurrence2Scalar4Left 52 = -(156819616353213802862358173642913345703 * 10 ^ 70 + 6431055561652685934022819262256336206134589741413424048678939194452340)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_53 :
Polynomial.coeff recurrence2Scalar4Left 53 = 1208633110943457278846296325981627106582 * 10 ^ 70 + 4174592361085376410955379640167564973009982272832362797650071035304620
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_54 :
Polynomial.coeff recurrence2Scalar4Left 54 = 7562790878416542496328751633792260192045 * 10 ^ 70 + 7291502947604900057701602493416047102830506586717084787569968647857737
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_55 :
Polynomial.coeff recurrence2Scalar4Left 55 = -(567185960810854824895431611626428888858577 * 10 ^ 70 + 6726918630618915314584256991189916419954736088887222426388484574037069)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_56 :
Polynomial.coeff recurrence2Scalar4Left 56 = 15021353045865382119845439130478587096206858 * 10 ^ 70 + 6257980136819028008794762552647535548244932109413308021072987193664252
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_57 :
Polynomial.coeff recurrence2Scalar4Left 57 = -(297703767789669991649003069175028176567301119 * 10 ^ 70 + 5172867621223179642375491468704460695487910214510910213609604584033066)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_58 :
Polynomial.coeff recurrence2Scalar4Left 58 = 4929645260551758591686918307384108652939991068 * 10 ^ 70 + 1688853034947744488248370141848794068015206131453660055768553156081188
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_59 :
Polynomial.coeff recurrence2Scalar4Left 59 = -(70099177609659576686252366912052886211757468128 * 10 ^ 70 + 4509905662518242151847146224009093358440499605330194268774845421334187)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_60 :
Polynomial.coeff recurrence2Scalar4Left 60 = 847671373781160556385946520086936527354257281881 * 10 ^ 70 + 6666838705068044803575012958233211596351440187461351047866293291933651
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_61 :
Polynomial.coeff recurrence2Scalar4Left 61 = -(8186382222859420488712542623456079336624899449959 * 10 ^ 70 + 4527755234564256629937648779798751147232458823832041993475900625336087)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_62 :
Polynomial.coeff recurrence2Scalar4Left 62 = 47306780163745908574724892086246897929382684507016 * 10 ^ 70 + 9603742459839271595226157618640881203160851781425420583572975531892702
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_63 :
Polynomial.coeff recurrence2Scalar4Left 63 = 326263829585230058557581311156470085386374223058714 * 10 ^ 70 + 7953198908602351359922887435038394377476197392679434952485804719314655
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_64 :
Polynomial.coeff recurrence2Scalar4Left 64 = -(16720618914622408723066293319398545787966217221584634 * 10 ^ 70 + 4832928123859413972621189232568228362324649384284509771773834950522064)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_65 :
Polynomial.coeff recurrence2Scalar4Left 65 = 357234593989662243724486898876736216275639292088753457 * 10 ^ 70 + 4807229984723324734819049837876512960314944597013022834793983314277519
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_66 :
Polynomial.coeff recurrence2Scalar4Left 66 = -(5925166687153367775248417747319476261974032035014188266 * 10 ^ 70 + 753934650541441846395764779058980189210799186023130620869230681858029)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_67 :
Polynomial.coeff recurrence2Scalar4Left 67 = 85194920489177093459538884521126603613996091867940527833 * 10 ^ 70 + 9475746905653441633527642275090390445945190603489074423386763659080320
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_68 :
Polynomial.coeff recurrence2Scalar4Left 68 = -(1106592673422591030275754224577269956321925124826899863956 * 10 ^ 70 + 1572821862663696498026816092646257654494911957648352018900803676236598)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_69 :
Polynomial.coeff recurrence2Scalar4Left 69 = 13251165073357879851148625970204280431101173787338299108914 * 10 ^ 70 + 3949456067820255133916038766419731126498699334780064890820890221980591
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_70 :
Polynomial.coeff recurrence2Scalar4Left 70 = -(148018036205260394701837316605554205814152021655536575207078 * 10 ^ 70 + 9017236973142252320254999409577528977306061819107321096530450855753577)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_71 :
Polynomial.coeff recurrence2Scalar4Left 71 = 1553961763702209444216274667947875511823126448361876312953384 * 10 ^ 70 + 4494931082092341938085191887182762125030457819743044140021138669475547
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_72 :
Polynomial.coeff recurrence2Scalar4Left 72 = -(15413148240547630375768530690775037525471258453857581768219308 * 10 ^ 70 + 838187368981096205844925887745075281851793038118094201181742273642371)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_73 :
Polynomial.coeff recurrence2Scalar4Left 73 = 144984078371076915950435719825304020879519265176819758171548844 * 10 ^ 70 + 56367194326432726862036194845301243949535538280036342187852196539870
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_74 :
Polynomial.coeff recurrence2Scalar4Left 74 = -(1297142686599829014867246999146187516635950977630280406197511888 * 10 ^ 70 + 4472310054112509609478605764636193838323830805851313927558834933745401)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_75 :
Polynomial.coeff recurrence2Scalar4Left 75 = 11063306293503269831160427659071006111540883012164021915318625007 * 10 ^ 70 + 3147701519058705250556261306842645699964456426994065932113510422479533
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_76 :
Polynomial.coeff recurrence2Scalar4Left 76 = -(90117211332298513137489195726344261056893215281903015576578068604 * 10 ^ 70 + 8669642416485590013301720187969969402400897659253070098317944051262283)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_77 :
Polynomial.coeff recurrence2Scalar4Left 77 = 702108175503203978499206708927134470142067406119668600427284583876 * 10 ^ 70 + 6385130335379197271390925763279710567794520399209121167614888774024727
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_78 :
Polynomial.coeff recurrence2Scalar4Left 78 = -(5238490021645901434433772507484263254661869703394361264077681251374 * 10 ^ 70 + 6215262125950286349176390192447370629054132332535079778869743008238959)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_79 :
Polynomial.coeff recurrence2Scalar4Left 79 = 37467463804797816496775020832147555178935655096452248360876686794589 * 10 ^ 70 + 5310691773533876858148313934221204817675599227406770490146330083981969
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_80 :
Polynomial.coeff recurrence2Scalar4Left 80 = -(257106964558488542312954964430126928934701236314822672477526631502490 * 10 ^ 70 + 7131059366131392488544407564446479385167917193095159682199914430699847)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_81 :
Polynomial.coeff recurrence2Scalar4Left 81 = 1693895385799078221440858661547773364314750665507129686356857334005949 * 10 ^ 70 + 1060873772566704149382404751371140355255038256131097020630836661183342
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_82 :
Polynomial.coeff recurrence2Scalar4Left 82 = -((1 * 10 ^ 70 + 720555808862915651047778512998384040691388914887209578747263234228881) * 10 ^ 70 + 5200903346980499695892961339094369271736387895429261280837386265405389)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_83 :
Polynomial.coeff recurrence2Scalar4Left 83 = (6 * 10 ^ 70 + 5207193824539433741292617907912889407978046004339520107548506320019279) * 10 ^ 70 + 1807080647500018910692556142044656190093367176657002838544355471254923
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_84 :
Polynomial.coeff recurrence2Scalar4Left 84 = -((38 * 10 ^ 70 + 1288515378118517554508472123113108118457580113675944813687202493019115) * 10 ^ 70 + 2805675364766482132290205970533595765855565283609535515019469978325339)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_85 :
Polynomial.coeff recurrence2Scalar4Left 85 = (214 * 10 ^ 70 + 3697828050315527606498741228852274732319188100337870768764326355803816) * 10 ^ 70 + 7029120829415827634823499411964806517233979973679384795519776371911964
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_86 :
Polynomial.coeff recurrence2Scalar4Left 86 = -((1158 * 10 ^ 70 + 8601194924718108295650632249945175199715312795196984387755988169047757) * 10 ^ 70 + 5454506359993429095648849574776395044633714531119533688032049434651954)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_87 :
Polynomial.coeff recurrence2Scalar4Left 87 = (6022 * 10 ^ 70 + 6963623452124263460047940823289445462679081138948060351614734779204042) * 10 ^ 70 + 8096099316293865643980934250050140259137779906009771232781629042666857
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_88 :
Polynomial.coeff recurrence2Scalar4Left 88 = -((30081 * 10 ^ 70 + 4966460481797082615588067743579432274001939637142057766392531763486302) * 10 ^ 70 + 2460948193375347641438046870305447481670278327632443335058227315534431)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_89 :
Polynomial.coeff recurrence2Scalar4Left 89 = (144317 * 10 ^ 70 + 5922511039527020472348498607943248158643727743058097888233760535366928) * 10 ^ 70 + 3238181497321623225395342585046093354647089132487895262417491953754494
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_90 :
Polynomial.coeff recurrence2Scalar4Left 90 = -((664496 * 10 ^ 70 + 7701043297331545868301708226480686112808475340091487181811584393833257) * 10 ^ 70 + 8123885060643387070938964422481878061023868328334145265560447426714359)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_91 :
Polynomial.coeff recurrence2Scalar4Left 91 = (2932876 * 10 ^ 70 + 8700021393984013774246021668053376491510961578308269018188713768494381) * 10 ^ 70 + 4753203148809989603108690707519656363484254327090231087025547229961466