Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence4LookupScalar1FirstPart0.Coefficients0To52

Recurrence 4 lookup certificate: Scalar1First coefficient convolution #

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

source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_0 :
Polynomial.coeff recurrence4Scalar1First 0 = 0
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_1 :
Polynomial.coeff recurrence4Scalar1First 1 = -83921241414679494612514457632606701454786560
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_2 :
Polynomial.coeff recurrence4Scalar1First 2 = 755720455248389530300398836042458145231921405952
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_3 :
Polynomial.coeff recurrence4Scalar1First 3 = -2508464416318493024073950905368412761160370779436544
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_4 :
Polynomial.coeff recurrence4Scalar1First 4 = 3424997062089538418437735461688297806132496909889284992
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_5 :
Polynomial.coeff recurrence4Scalar1First 5 = 189654811169388450017263673475555333579509073549440171424
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_6 :
Polynomial.coeff recurrence4Scalar1First 6 = -6963871838947980811918702695455460414417060948566410552958736
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_7 :
Polynomial.coeff recurrence4Scalar1First 7 = 9922442307317059931713646142343991127570937169188664901567055464
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_8 :
Polynomial.coeff recurrence4Scalar1First 8 = -6832908761679528931317110691808838093746078136846256309090786638020
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_9 :
Polynomial.coeff recurrence4Scalar1First 9 = 2689346335338665652936184569676131828434689251833930198673951075042976
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_10 :
Polynomial.coeff recurrence4Scalar1First 10 = -(77 * 10 ^ 70 + 6336955848046617127294957053702182462942399775518340533578607562730994)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_11 :
Polynomial.coeff recurrence4Scalar1First 11 = 27797 * 10 ^ 70 + 5985320553296031520745717776465414902701064559782133748746554838747962
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_12 :
Polynomial.coeff recurrence4Scalar1First 12 = -(9725821 * 10 ^ 70 + 5539380773441982446850712128148393798192609483087260935038556552150718)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_13 :
Polynomial.coeff recurrence4Scalar1First 13 = 353062902 * 10 ^ 70 + 76236152189380126829840713492955948701938056745809673303046821531582
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_14 :
Polynomial.coeff recurrence4Scalar1First 14 = 1603452813540 * 10 ^ 70 + 6230545848618260432873123213282622122936586163621328167563595607261726
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_15 :
Polynomial.coeff recurrence4Scalar1First 15 = -(717384148963929 * 10 ^ 70 + 9364752718098076276267621099517988531640045055330221266251448300743563)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_16 :
Polynomial.coeff recurrence4Scalar1First 16 = 52131950749769755 * 10 ^ 70 + 7584798262323255329500894668067865214233114290503470698058301919407237
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_17 :
Polynomial.coeff recurrence4Scalar1First 17 = 63585837482009695225 * 10 ^ 70 + 8558234069105983583072186085184337876100239887011799799506899236343550
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_18 :
Polynomial.coeff recurrence4Scalar1First 18 = -(19742197688587044657839 * 10 ^ 70 + 1721587418981396353110430102936583986388250230924185356498402144158136)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_19 :
Polynomial.coeff recurrence4Scalar1First 19 = -(6051894335397930196383994 * 10 ^ 70 + 4854978597051294571115594350404180625293578834960586273191257513074912)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_20 :
Polynomial.coeff recurrence4Scalar1First 20 = 7213705877891596789105406644 * 10 ^ 70 + 6529832007836710392806813928213296519954661726436543680841055850749201
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_21 :
Polynomial.coeff recurrence4Scalar1First 21 = -(3219888279753296615070556680317 * 10 ^ 70 + 3645226301976690379580885455361202312374224135116032529884358012071039)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_22 :
Polynomial.coeff recurrence4Scalar1First 22 = 926603025311867555557812463585745 * 10 ^ 70 + 5093961152667778440015685693165882992704792120628746494183596245801160
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_23 :
Polynomial.coeff recurrence4Scalar1First 23 = -(187958511267445165566769524244690134 * 10 ^ 70 + 2839118109268216877968636322648178323958510949786474606270817782287972)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_24 :
Polynomial.coeff recurrence4Scalar1First 24 = 27492306543626947925427366255336411023 * 10 ^ 70 + 9819772633147297966568249188210234112917970670765072612313934724848501
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_25 :
Polynomial.coeff recurrence4Scalar1First 25 = -(3513391992147239777574098148479189620394 * 10 ^ 70 + 2438578302748512700314573653331777947693830410494263261836795897761252)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_26 :
Polynomial.coeff recurrence4Scalar1First 26 = 883593466274621906223991240474939195322811 * 10 ^ 70 + 2979477366505944778796837206384992313310904773746868929598971625170777
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_27 :
Polynomial.coeff recurrence4Scalar1First 27 = -(380759931322769073506716772799837645351611894 * 10 ^ 70 + 9903684559221094601472307572175434102056956263078299730145445540615256)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_28 :
Polynomial.coeff recurrence4Scalar1First 28 = 139627377733442140055518080487177164640351996229 * 10 ^ 70 + 9824391009255331385274501117512715137748807087214892056214907027336833
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_29 :
Polynomial.coeff recurrence4Scalar1First 29 = -(39978470924065643159788147417204321639671645649885 * 10 ^ 70 + 6060785012050057452236029518852100774920074968876466888980566831831228)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_30 :
Polynomial.coeff recurrence4Scalar1First 30 = 9256498927054789728253207085285046450191331942059768 * 10 ^ 70 + 9735171751416986732254298286499663374523574209517856727007883079045492
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_31 :
Polynomial.coeff recurrence4Scalar1First 31 = -(1776797298843391320071269212361220577628006248376043057 * 10 ^ 70 + 9371767638628893951162275816099467007288780382373438652199851888494166)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_32 :
Polynomial.coeff recurrence4Scalar1First 32 = 283588104105129461584239237915212938158729572616447337138 * 10 ^ 70 + 578204505524571956201002469562474858841529542361337497422346010856972
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_33 :
Polynomial.coeff recurrence4Scalar1First 33 = -(36563129477597504979308197256453649768229099512925330395603 * 10 ^ 70 + 3445184381066090714883591663668421677015026972139855376053865817547689)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_34 :
Polynomial.coeff recurrence4Scalar1First 34 = 3393882822862044158084888531429122557165448440002545621621947 * 10 ^ 70 + 4621643938903998598016817786146381434595232544299949501827418686825264
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_35 :
Polynomial.coeff recurrence4Scalar1First 35 = -(96531038551013832337936885725066696653787653431617769038871537 * 10 ^ 70 + 1055759586254850502154494723419476593694836191439916836525894675602317)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_36 :
Polynomial.coeff recurrence4Scalar1First 36 = -(44921612191205236074785122347627333162078288520165368837895593044 * 10 ^ 70 + 6875190665343400302193142303407100514595700223539742500324174392655905)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_37 :
Polynomial.coeff recurrence4Scalar1First 37 = 12978218690712376958243994931405388990713525129009997646997322678016 * 10 ^ 70 + 2784020825953993047052299435959681756690789856129317366861523734589873
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_38 :
Polynomial.coeff recurrence4Scalar1First 38 = -(2313821426928161184079895165510769951549585776745582846237475403346386 * 10 ^ 70 + 1975132711406834225283144894100151376739705165973214716565547164049215)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_39 :
Polynomial.coeff recurrence4Scalar1First 39 = (32 * 10 ^ 70 + 3154083162212312378743651880180144864105519392415955283924982140941044) * 10 ^ 70 + 2191846507825750381202769345252697431981276365779174782763175695149281
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_40 :
Polynomial.coeff recurrence4Scalar1First 40 = -((3731 * 10 ^ 70 + 9189787995306366058346841370063922005990945651330034788587791583030146) * 10 ^ 70 + 832436736076175184838346656764681230339301750814148235581619786867747)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_41 :
Polynomial.coeff recurrence4Scalar1First 41 = (356663 * 10 ^ 70 + 2260483735476973677205405529007650817663506157074346616211499831153738) * 10 ^ 70 + 7624120897073303043248562335944416527691486784529420992805633259639163
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_42 :
Polynomial.coeff recurrence4Scalar1First 42 = -((26708646 * 10 ^ 70 + 1086968061873001995224178025163072419814850209314357564168687144913385) * 10 ^ 70 + 5391781045053867942542225337136488885538657672826688451341969374035833)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_43 :
Polynomial.coeff recurrence4Scalar1First 43 = (1204924481 * 10 ^ 70 + 305548294369999339443823625601415132090183827672410965276332801451647) * 10 ^ 70 + 5790350657807317003422162156243367463448188383912027420984376006129816
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_44 :
Polynomial.coeff recurrence4Scalar1First 44 = (49909625388 * 10 ^ 70 + 3799573598782121146432047298319326536051504737352400023968994729540953) * 10 ^ 70 + 1423197148762288516435533648129831071805816944529437363394118291286180
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_45 :
Polynomial.coeff recurrence4Scalar1First 45 = -((20588932483548 * 10 ^ 70 + 1853308524052892953863798550589143191698831931513235710293177411688967) * 10 ^ 70 + 1061891013551821084134311156551470686426039448544277662436181356221986)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_46 :
Polynomial.coeff recurrence4Scalar1First 46 = (3172112892382242 * 10 ^ 70 + 7343993203384050189635113397663276728568196811771076394144515688655306) * 10 ^ 70 + 7999495565033059612986965280503456511391531897348007682360195567509907
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_47 :
Polynomial.coeff recurrence4Scalar1First 47 = -((369834223728667023 * 10 ^ 70 + 8775766011742240086152563742286334642487576379872860320720442866835627) * 10 ^ 70 + 1761832294818280888183988160340107417277052360503656188216270827058362)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_48 :
Polynomial.coeff recurrence4Scalar1First 48 = (36680935416985922145 * 10 ^ 70 + 6510690872046055282659704279882971826077428650094457620801454926196171) * 10 ^ 70 + 5398699618039725847768877021599273215820533267310059635700014252392359
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_49 :
Polynomial.coeff recurrence4Scalar1First 49 = -((3231809418021637281009 * 10 ^ 70 + 619340699783661693318298608193429781728799434811047134154570146502189) * 10 ^ 70 + 6789697528241911910660117611012042070009445578831857244571133679225577)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_50 :
Polynomial.coeff recurrence4Scalar1First 50 = (258421781475828468777311 * 10 ^ 70 + 5569453907538964153169983550869058830440569426198032495428626862084350) * 10 ^ 70 + 926860138134331219018650197049724866310942049761418246713289240004048
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_51 :
Polynomial.coeff recurrence4Scalar1First 51 = -((18989908323419432140985753 * 10 ^ 70 + 4204703094139043737495161032447179122859190946268079548621064542130104) * 10 ^ 70 + 3617033803550526575243104207583138383760963565994808468623088628180309)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_52 :
Polynomial.coeff recurrence4Scalar1First 52 = (1292882527048244485569181565 * 10 ^ 70 + 5942591536279853443815513600728542685590242299893261730838561900153208) * 10 ^ 70 + 2751473030152928900735733798580044171079225888403260487493221417448689