Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupScalar4ShiftPart0.Coefficients0To91

Recurrence 2 lookup certificate: Scalar4Shift 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.recurrence2Scalar4Shift_coeff_0 :
Polynomial.coeff recurrence2Scalar4Shift 0 = 0
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_1 :
Polynomial.coeff recurrence2Scalar4Shift 1 = -18616320
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_2 :
Polynomial.coeff recurrence2Scalar4Shift 2 = -86085473280
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_3 :
Polynomial.coeff recurrence2Scalar4Shift 3 = -653845232887728
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_4 :
Polynomial.coeff recurrence2Scalar4Shift 4 = -1759627223865466168
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_5 :
Polynomial.coeff recurrence2Scalar4Shift 5 = -5089912252186246527920
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_6 :
Polynomial.coeff recurrence2Scalar4Shift 6 = 36384057211809888422344
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_7 :
Polynomial.coeff recurrence2Scalar4Shift 7 = 2536510807817426456476115760
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_8 :
Polynomial.coeff recurrence2Scalar4Shift 8 = -1490108743313765272220937059608
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_9 :
Polynomial.coeff recurrence2Scalar4Shift 9 = 3063948890803397330597364255138264
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_10 :
Polynomial.coeff recurrence2Scalar4Shift 10 = -1272909368524094231027237140120394160
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_11 :
Polynomial.coeff recurrence2Scalar4Shift 11 = 830159471203764364250132330193286012084
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_12 :
Polynomial.coeff recurrence2Scalar4Shift 12 = -335747645432826665752924540534773821441974
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_13 :
Polynomial.coeff recurrence2Scalar4Shift 13 = 103468708523233241926323915034642975241344414
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_14 :
Polynomial.coeff recurrence2Scalar4Shift 14 = -23739216294813522485372260375062102643165969694
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_15 :
Polynomial.coeff recurrence2Scalar4Shift 15 = 4111270808710063716625779350387751626869899609664
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_16 :
Polynomial.coeff recurrence2Scalar4Shift 16 = -541156875506926247790155007350157110686847756372052
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_17 :
Polynomial.coeff recurrence2Scalar4Shift 17 = 50643720829429837382794737563517163562263582771217595
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_18 :
Polynomial.coeff recurrence2Scalar4Shift 18 = -2802129552868454518251234141501131930005936794135819876
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_19 :
Polynomial.coeff recurrence2Scalar4Shift 19 = -28204354260149165988318160364044275592637140884438089734
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_20 :
Polynomial.coeff recurrence2Scalar4Shift 20 = 24303370803551539293735984305645142681838451544656896879848
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_21 :
Polynomial.coeff recurrence2Scalar4Shift 21 = -2777673435013683380823351399124169752905025979256072168951085
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_22 :
Polynomial.coeff recurrence2Scalar4Shift 22 = 183353575087504018685363604685851747656550192057573290421641944
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_23 :
Polynomial.coeff recurrence2Scalar4Shift 23 = -6943738583518476430993736937765083595548839825111701117997925134
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_24 :
Polynomial.coeff recurrence2Scalar4Shift 24 = 46954165765694654818600740250394242970849456307436363161974976679
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_25 :
Polynomial.coeff recurrence2Scalar4Shift 25 = 9566092535251612766053383750754036494633627414618312545635010991999
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_26 :
Polynomial.coeff recurrence2Scalar4Shift 26 = -225802715413063673463428208008508487634335786557546093964568430436283
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_27 :
Polynomial.coeff recurrence2Scalar4Shift 27 = -(4 * 10 ^ 70 + 8718270911865048952234558284034881966388641220365228077118482407000154)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_28 :
Polynomial.coeff recurrence2Scalar4Shift 28 = 627 * 10 ^ 70 + 2379260068730934938850056804662122286550045629606624099476972917497735
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_29 :
Polynomial.coeff recurrence2Scalar4Shift 29 = -(44615 * 10 ^ 70 + 6409084310027048243234133529751464528988718460813332105807938147177283)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_30 :
Polynomial.coeff recurrence2Scalar4Shift 30 = 2324541 * 10 ^ 70 + 600384320691129093855118021776311609909809058292941340232109691870191
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_31 :
Polynomial.coeff recurrence2Scalar4Shift 31 = -(94360625 * 10 ^ 70 + 2220077528885186678516945001186203775116438300806484294886377764604280)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_32 :
Polynomial.coeff recurrence2Scalar4Shift 32 = 2826476416 * 10 ^ 70 + 2292990929735743355778703590509132394427705946236297278708161801330410
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_33 :
Polynomial.coeff recurrence2Scalar4Shift 33 = -(38387715470 * 10 ^ 70 + 4388941965741945893563592543658302593777334144408812426095042257398110)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_34 :
Polynomial.coeff recurrence2Scalar4Shift 34 = -(2220803296096 * 10 ^ 70 + 9158269388672582496382439725809651341078738039179673906263185510453816)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_35 :
Polynomial.coeff recurrence2Scalar4Shift 35 = 221724065360911 * 10 ^ 70 + 2972363089323915523406901924720041555975034680099547240629737604802606
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_36 :
Polynomial.coeff recurrence2Scalar4Shift 36 = -(11600859248608932 * 10 ^ 70 + 8411287165600902333353977188847750345015754227968435988329220067585840)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_37 :
Polynomial.coeff recurrence2Scalar4Shift 37 = 442262459690611246 * 10 ^ 70 + 2669915869794750635325021124963177275395723576612251949452181088719688
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_38 :
Polynomial.coeff recurrence2Scalar4Shift 38 = -(13069370847345907978 * 10 ^ 70 + 7810972912357237757050373157053855132481226130669509204921355575610267)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_39 :
Polynomial.coeff recurrence2Scalar4Shift 39 = 303433502976192050803 * 10 ^ 70 + 9099024334351808010553619997448228518048324059870467043420199410449100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_40 :
Polynomial.coeff recurrence2Scalar4Shift 40 = -(5691483725261066663271 * 10 ^ 70 + 6846128381805940094458250121979535228506446728397926219718844796786314)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_41 :
Polynomial.coeff recurrence2Scalar4Shift 41 = 105747362947552271948778 * 10 ^ 70 + 7693635853292990356153211520798597322792378264066522614686397979447348
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_42 :
Polynomial.coeff recurrence2Scalar4Shift 42 = -(3131147637032718221827385 * 10 ^ 70 + 9808487051784021999216365959831647354595689091235817663043588198254198)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_43 :
Polynomial.coeff recurrence2Scalar4Shift 43 = 132564427630225772967349624 * 10 ^ 70 + 9315590454530997721581610580002428893851070497855000220445908401877139
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_44 :
Polynomial.coeff recurrence2Scalar4Shift 44 = -(5192610546125521711509556219 * 10 ^ 70 + 366543689663567661685312411433445576917762180859757219506067457121877)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_45 :
Polynomial.coeff recurrence2Scalar4Shift 45 = 167669243010062071473824599825 * 10 ^ 70 + 2933227220873236114969092606465794739587967100377571648347218507456949
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_46 :
Polynomial.coeff recurrence2Scalar4Shift 46 = -(4492996626652958094265418245929 * 10 ^ 70 + 4854751640664824603469396501011824498321772114563574748163803385448461)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_47 :
Polynomial.coeff recurrence2Scalar4Shift 47 = 102001536510693622673366268481835 * 10 ^ 70 + 6294986358727542488592830115000385357755992355308177866579336112489770
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_48 :
Polynomial.coeff recurrence2Scalar4Shift 48 = -(1990787691052707496499039611595772 * 10 ^ 70 + 8394528356830320790339765659473082572572825486033569048374016293288240)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_49 :
Polynomial.coeff recurrence2Scalar4Shift 49 = 33487735383266991591158956561820876 * 10 ^ 70 + 8932171736328751069130450571587106120913775258755711565660938123615089
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_50 :
Polynomial.coeff recurrence2Scalar4Shift 50 = -(474548599248266520577454270489400707 * 10 ^ 70 + 1588936832960973213040767248875248598453618117309143979950270541262296)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_51 :
Polynomial.coeff recurrence2Scalar4Shift 51 = 5117385967113750864089424093850970964 * 10 ^ 70 + 9893296585007007098661876670447449447876239647652627075098642832258699
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_52 :
Polynomial.coeff recurrence2Scalar4Shift 52 = -(20640911620768007235620309831964200371 * 10 ^ 70 + 4385762354539517720117751814796657424510951909099519776359062011545646)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_53 :
Polynomial.coeff recurrence2Scalar4Shift 53 = -(893771073554016419533661616845937192308 * 10 ^ 70 + 4177935536665627688877463402378224728146169688437342570103527327836927)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_54 :
Polynomial.coeff recurrence2Scalar4Shift 54 = 34971207294076245970313242029678821272543 * 10 ^ 70 + 8329117251928420917993496023454961242188488417663613335231955771847153
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_55 :
Polynomial.coeff recurrence2Scalar4Shift 55 = -(846711912687671046298438242678177418730317 * 10 ^ 70 + 1897523329590915108310872060609815857358257056912234062311167677510114)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_56 :
Polynomial.coeff recurrence2Scalar4Shift 56 = 16447307732368636055325531124529708438164980 * 10 ^ 70 + 5903407382953410444133546667594537807056605891739310338621053374346110
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_57 :
Polynomial.coeff recurrence2Scalar4Shift 57 = -(271627251696055035717500240711064490501588060 * 10 ^ 70 + 3082558196654696550996137355438535732874537065735899181314680118400218)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_58 :
Polynomial.coeff recurrence2Scalar4Shift 58 = 3853584179635834177003216116384668967854001880 * 10 ^ 70 + 2306894758577135537214396780184909528836772629215296556683021715411698
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_59 :
Polynomial.coeff recurrence2Scalar4Shift 59 = -(45958626356006936924832221426535085169385503904 * 10 ^ 70 + 6014110354757140428364262899023641521333398662975391792983003525794576)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_60 :
Polynomial.coeff recurrence2Scalar4Shift 60 = 421458207009349833903524214229884304864464133855 * 10 ^ 70 + 6566854315157077816573885502070830023265734129913704855438198356551480
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_61 :
Polynomial.coeff recurrence2Scalar4Shift 61 = -(1788411920507960956227054019221628535944017569248 * 10 ^ 70 + 5972774741236681739273426109220718483683249346037040818595464945953805)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_62 :
Polynomial.coeff recurrence2Scalar4Shift 62 = -(36264821904544926445444022930707346283098176441863 * 10 ^ 70 + 9708227565854735564677308591812978827878658947232317395776831623171)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_63 :
Polynomial.coeff recurrence2Scalar4Shift 63 = 1275449695891102683654543696401573249003781063866238 * 10 ^ 70 + 5844641257429072484146101761224586564574285554497328053496141557780389
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_64 :
Polynomial.coeff recurrence2Scalar4Shift 64 = -(25837383561160767682892781909917554480795364595300301 * 10 ^ 70 + 8921144900501314709134066774020246848898786704946743639906708993271823)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_65 :
Polynomial.coeff recurrence2Scalar4Shift 65 = 424215958502251176944037710743909968121031584458748896 * 10 ^ 70 + 4571118180695013678412756154324644727044050226672332720332199997386776
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_66 :
Polynomial.coeff recurrence2Scalar4Shift 66 = -(6127711475247397840378733249411441084844598795900504569 * 10 ^ 70 + 9269082916463770264393774934300861774689222670277871871158503771094138)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_67 :
Polynomial.coeff recurrence2Scalar4Shift 67 = 80510190575719300374775687424710202516599350365568885145 * 10 ^ 70 + 759692084570338313271664017302993322135124852623688791517655560942603
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_68 :
Polynomial.coeff recurrence2Scalar4Shift 68 = -(978771239315441250007425743278439813257644964447506977172 * 10 ^ 70 + 2342439884458902082826106941380748491091845976628856614660770270705848)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_69 :
Polynomial.coeff recurrence2Scalar4Shift 69 = 11122934544334162511516490636569061214509380253358407946567 * 10 ^ 70 + 2476369784349294294452505141165043675363217368232992997989591248756613
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_70 :
Polynomial.coeff recurrence2Scalar4Shift 70 = -(118960440448081582370155465817892658564381358452756981982771 * 10 ^ 70 + 7918653986534356504591617984198804360961702737655701863579647589134582)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_71 :
Polynomial.coeff recurrence2Scalar4Shift 71 = 1203193737429954970808689400346999518022266169910630762549908 * 10 ^ 70 + 8418584995871027443619074423435694210192320849395370603869009482811409
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_72 :
Polynomial.coeff recurrence2Scalar4Shift 72 = -(11550585363941072001839548284481679790600017984705366570318163 * 10 ^ 70 + 76508448410760010382663895097269206564734382137962501797529520233576)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_73 :
Polynomial.coeff recurrence2Scalar4Shift 73 = 105544003646416965649103726657281951867122124291397614496979547 * 10 ^ 70 + 1996609819659576514197927013632661858190069378890496889013611708419271
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_74 :
Polynomial.coeff recurrence2Scalar4Shift 74 = -(919987511993084008768084339561999722534905150026963415719191955 * 10 ^ 70 + 5167417064843915055102599948341207823495862336762518867280400596271365)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_75 :
Polynomial.coeff recurrence2Scalar4Shift 75 = 7663082704302959409313043669199758802394082225043026618072226788 * 10 ^ 70 + 2999693118541915868869663596719472119343174726464954214599280313411617
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_76 :
Polynomial.coeff recurrence2Scalar4Shift 76 = -(61080630221015856101723347594560757849740002581612114466862032204 * 10 ^ 70 + 1093967617117578188359257780170631722602709172820045817361505242921605)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_77 :
Polynomial.coeff recurrence2Scalar4Shift 77 = 466427294745392322168474266046735252168512719782952742783223786666 * 10 ^ 70 + 8860271519020044367266917333290412566109650811068381006073179600178634
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_78 :
Polynomial.coeff recurrence2Scalar4Shift 78 = -(3415689194700677369841439416965423646195536695616904578660942928102 * 10 ^ 70 + 597495402948383852944071442954649512630653959620427468539428951048761)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_79 :
Polynomial.coeff recurrence2Scalar4Shift 79 = 24008822641411806066159747725636710717429575455044946755254548936229 * 10 ^ 70 + 678917666699834241285439235134513426030327148674839173230471626252697
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_80 :
Polynomial.coeff recurrence2Scalar4Shift 80 = -(162106198337681446668507998902215377268100159134216117996621786235887 * 10 ^ 70 + 6107766424933930581575658041219500565895981474007864210433453264621836)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_81 :
Polynomial.coeff recurrence2Scalar4Shift 81 = 1052078565584501930139616964683102298058414793317931568106140523498612 * 10 ^ 70 + 6586809990880484404492937594709887660277582925999876108506456916143888
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_82 :
Polynomial.coeff recurrence2Scalar4Shift 82 = -(6566495839810461840156483892279737165574756909686580919686689503022851 * 10 ^ 70 + 4768296346432610099908743198003324514945115765704871741165578279032500)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_83 :
Polynomial.coeff recurrence2Scalar4Shift 83 = (3 * 10 ^ 70 + 9427664566338116476848059568516026073191042484167656754116616029108601) * 10 ^ 70 + 6918295225310720518805007169467179200822757832633431456516897714184678
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_84 :
Polynomial.coeff recurrence2Scalar4Shift 84 = -((22 * 10 ^ 70 + 7787260741093260199316117820242277592881363429685379760070507936667962) * 10 ^ 70 + 7557908092817143039542031727477484758729016191746111542174016141262572)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_85 :
Polynomial.coeff recurrence2Scalar4Shift 85 = (126 * 10 ^ 70 + 6339546704566372659112137904710737401919035696222146532356842226845049) * 10 ^ 70 + 3430029873440316777835417392646020438200387252427202793066713941846383
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_86 :
Polynomial.coeff recurrence2Scalar4Shift 86 = -((677 * 10 ^ 70 + 4350467777540509230349782567591682844625486956307348852701923674266790) * 10 ^ 70 + 2088358867893640472467049121852192908553717294149034984475772481220999)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_87 :
Polynomial.coeff recurrence2Scalar4Shift 87 = (3487 * 10 ^ 70 + 1269394038891769120436471241729617115557003134003193269590255728064305) * 10 ^ 70 + 6079194888452834767893562544657408478340836101400557263298102736816367
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_88 :
Polynomial.coeff recurrence2Scalar4Shift 88 = -((17270 * 10 ^ 70 + 2325283440812849970014692551783425488824867843782205809907171520181960) * 10 ^ 70 + 9914415022799093088934038113261352196911385119582643137922035872245001)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_89 :
Polynomial.coeff recurrence2Scalar4Shift 89 = (82264 * 10 ^ 70 + 6424710458043490918212733475246435006896966381434011641974938689636747) * 10 ^ 70 + 1207106013288676064559146342900242651114265464276791314743181465642720
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_90 :
Polynomial.coeff recurrence2Scalar4Shift 90 = -((376609 * 10 ^ 70 + 1651052255027344796121992613631859451848223454243723851684802326760409) * 10 ^ 70 + 5602180148090457041998961876639751663642128439860957560316051840971424)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_91 :
Polynomial.coeff recurrence2Scalar4Shift 91 = (1654816 * 10 ^ 70 + 8890006027401721179217198903331669325822110756121780466075609973708580) * 10 ^ 70 + 4475340428224048817037035678342674029223940045628173844647875888402595