Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence5LookupExceptionalProductPart0.Coefficients74To122

Recurrence 5 lookup certificate: ExceptionalProduct coefficient convolution #

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

source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_74 :
Polynomial.coeff recurrence5ExceptionalProduct 74 = -(61058061802981623029376606806443202366894773710420183549367077429708 * 10 ^ 70 + 7834852662939162117904246127173471259667675610847221789132433459542517) / 738070452448895892793300
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_75 :
Polynomial.coeff recurrence5ExceptionalProduct 75 = (1778708839938916102908032048117745991890808972182893258924457206495056 * 10 ^ 70 + 2041878902067948824433241936223947153647542221990520457521491726956337) / 2730860674060914803335210
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_76 :
Polynomial.coeff recurrence5ExceptionalProduct 76 = -((1 * 10 ^ 70 + 9837180590798157475279001311109115849265341973362915958537680678591076) * 10 ^ 70 + 4878356355618900429834707097978680394633967648012920470951119886599374) / 6827151685152287008338025
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_77 :
Polynomial.coeff recurrence5ExceptionalProduct 77 = -((6 * 10 ^ 70 + 5193802811782163788090483663463793449505202138940830704956427715819689) * 10 ^ 70 + 9758846121239654386206048828084053124681637673237648901857302016852647) / 13654303370304574016676050
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_78 :
Polynomial.coeff recurrence5ExceptionalProduct 78 = ((644 * 10 ^ 70 + 5099057097564484374282158178602067979570377982438354264178025609008049) * 10 ^ 70 + 2719587010204688785863953611968404396869462710732262481445337190185517) / 27308606740609148033352100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_79 :
Polynomial.coeff recurrence5ExceptionalProduct 79 = -((7005 * 10 ^ 70 + 6376908543753043975363537759224337549132769127395601501261309589286079) * 10 ^ 70 + 6946617225435735341926834373463447147538926667794048284431250915733619) / 27308606740609148033352100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_80 :
Polynomial.coeff recurrence5ExceptionalProduct 80 = ((46284 * 10 ^ 70 + 3490105745422554948159890967789743272550460840557426141078582071448968) * 10 ^ 70 + 4163233575266387065216490618722237055604413976728729158097424568322071) / 27308606740609148033352100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_81 :
Polynomial.coeff recurrence5ExceptionalProduct 81 = -((7654 * 10 ^ 70 + 3692752452407220459424048088083333136899117546851607689964791940653614) * 10 ^ 70 + 9750386254254958721245635185486135909300227673253077493491538147243689) / 1365430337030457401667605
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_82 :
Polynomial.coeff recurrence5ExceptionalProduct 82 = -((178085 * 10 ^ 70 + 9051382360284165193755616043423068051525156418685257486097695719862999) * 10 ^ 70 + 4205803297139688834889439582818191011898200755153621219641451451210643) / 6827151685152287008338025
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_83 :
Polynomial.coeff recurrence5ExceptionalProduct 83 = ((3975951 * 10 ^ 70 + 8590870198073581983619371736998167468836634366648150516762632031016955) * 10 ^ 70 + 6515193944283061941254697638008196646474407392295804676263198301131648) / 6827151685152287008338025
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_84 :
Polynomial.coeff recurrence5ExceptionalProduct 84 = -((28122830 * 10 ^ 70 + 1489812627627179315233347101555577832167588953700574236929691511828507) * 10 ^ 70 + 7532815426146296943822105341667984832972027087886110982850127402201043) / 5461721348121829606670420
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_85 :
Polynomial.coeff recurrence5ExceptionalProduct 85 = ((764823238 * 10 ^ 70 + 6804381021887996823426247651921951270121213684184374730229050658407924) * 10 ^ 70 + 1344111137183728699668947490170924894632747890613065488533781077701007) / 27308606740609148033352100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_86 :
Polynomial.coeff recurrence5ExceptionalProduct 86 = -((1627845985 * 10 ^ 70 + 1173710268770304824726060826989640801622609950563761302649818997968007) * 10 ^ 70 + 1401252930620238539738601393956566985655385966000146680345137053699531) / 27308606740609148033352100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_87 :
Polynomial.coeff recurrence5ExceptionalProduct 87 = -((8768178196 * 10 ^ 70 + 7722557031065684878362461051053064713297271643037024941892277294272641) * 10 ^ 70 + 3138844380416990478610924830953883056595351804095628664555314997665739) / 13654303370304574016676050
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_88 :
Polynomial.coeff recurrence5ExceptionalProduct 88 = ((25509936193 * 10 ^ 70 + 1073168369784778220075430514062115329683837552962499211236433826264805) * 10 ^ 70 + 546774438948154430396133769796679053854072194676023462633462405112759) / 2730860674060914803335210
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_89 :
Polynomial.coeff recurrence5ExceptionalProduct 89 = -((939302486547 * 10 ^ 70 + 2862585113892399016955282960585239761217878336297790784258890069813968) * 10 ^ 70 + 1184328404349971041475978849984762074234472812619782838360558620075189) / 13654303370304574016676050
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_90 :
Polynomial.coeff recurrence5ExceptionalProduct 90 = ((2124659060123 * 10 ^ 70 + 1182760516847907168868020534295746359727599411339634584564876287279751) * 10 ^ 70 + 240952626263668569204369536072684305576241796283393364860836124279084) / 6827151685152287008338025
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_91 :
Polynomial.coeff recurrence5ExceptionalProduct 91 = -((2350089329382 * 10 ^ 70 + 8565067276031574718597778459261647584176407316394164985322266616278324) * 10 ^ 70 + 4385115062203979196456743164209821088717898696219588409776505338824684) / 6827151685152287008338025
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_92 :
Polynomial.coeff recurrence5ExceptionalProduct 92 = -((241026563679622 * 10 ^ 70 + 5958726634412038025091525216101667531254059430270385615919767994701620) * 10 ^ 70 + 3285500841855303399344242859641080945966747101607957893194119955484813) / 27308606740609148033352100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_93 :
Polynomial.coeff recurrence5ExceptionalProduct 93 = ((2724934101612359 * 10 ^ 70 + 3790004334958734435193212856052689647736305596646411230137205944859861) * 10 ^ 70 + 3812962680931326945769958711246349473295723863059785675373118597610569) / 27308606740609148033352100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_94 :
Polynomial.coeff recurrence5ExceptionalProduct 94 = -((1746076519884076 * 10 ^ 70 + 113255214818700153674737708757783233660839903890751031771608516136439) * 10 ^ 70 + 7723456652032406063884262211716483200353084362654222500788046268075943) / 2730860674060914803335210
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_95 :
Polynomial.coeff recurrence5ExceptionalProduct 95 = ((68755196794785988 * 10 ^ 70 + 3465864266623056512001851928330808700494405435376880712464105095024833) * 10 ^ 70 + 8188973613552450456346038725820463548355775485342427550828149736122327) / 27308606740609148033352100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_96 :
Polynomial.coeff recurrence5ExceptionalProduct 96 = -((7258393959950877 * 10 ^ 70 + 7683303680221360734243095871053861203913146602440110303582370399066474) * 10 ^ 70 + 2948780153584346125082727853129290093371311355911545217285082543567883) / 5461721348121829606670420
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_97 :
Polynomial.coeff recurrence5ExceptionalProduct 97 = -((1011636514831839080 * 10 ^ 70 + 4495965747969727352169601978963626387769347081465232737440801061128052) * 10 ^ 70 + 1101969070571869656873865556745685559453481913599993346813557383143429) / 13654303370304574016676050
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_98 :
Polynomial.coeff recurrence5ExceptionalProduct 98 = ((20030488164978365597 * 10 ^ 70 + 8872876037861068734488274769834184277663628527186227900381569147337975) * 10 ^ 70 + 7123129868227861367381005554088694551887277934398128788290052235276111) / 27308606740609148033352100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_99 :
Polynomial.coeff recurrence5ExceptionalProduct 99 = -((118355760192962991688 * 10 ^ 70 + 5950216187306881779285411726079925125265277286296090253218464129821425) * 10 ^ 70 + 3743916387862324677485615473656459184219985814179501152776868354198013) / 27308606740609148033352100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_100 :
Polynomial.coeff recurrence5ExceptionalProduct 100 = ((441510381007962393947 * 10 ^ 70 + 8993232852193886167442333806259756975240600738105764119500538413625522) * 10 ^ 70 + 1752813006978764806184857398955295215843042568977011280425923308674939) / 27308606740609148033352100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_101 :
Polynomial.coeff recurrence5ExceptionalProduct 101 = -((78216028095205055251 * 10 ^ 70 + 1351996493142303342887549687242996722042529303493754020801899356827073) * 10 ^ 70 + 1463189579059450328239410158338826248759119610430937470707262944911801) / 6827151685152287008338025
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_102 :
Polynomial.coeff recurrence5ExceptionalProduct 102 = -((10579791269985137790404 * 10 ^ 70 + 2287932797678695517496756475068909190600962003546581237610791794101552) * 10 ^ 70 + 7401600494174566644467757952903393219808418628808504112163780634387869) / 27308606740609148033352100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_103 :
Polynomial.coeff recurrence5ExceptionalProduct 103 = ((103164420494194124178234 * 10 ^ 70 + 7986132897983130276199638621483861370920922959905639081026252540325749) * 10 ^ 70 + 8747587338372123037442974378225508930691246583020421054685352891221313) / 27308606740609148033352100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_104 :
Polynomial.coeff recurrence5ExceptionalProduct 104 = -((602436672643220616364549 * 10 ^ 70 + 2036089570589375327947097615191083224207195076708458430309591390048071) * 10 ^ 70 + 2583972417979766454526514299613113970515053015001354296725098371922767) / 27308606740609148033352100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_105 :
Polynomial.coeff recurrence5ExceptionalProduct 105 = ((1174618963194422695524479 * 10 ^ 70 + 4277028161636843056107902187602110575025376849557848330627456697697352) * 10 ^ 70 + 7858269648537143040955516106035640572037534389384512483158295674648769) / 13654303370304574016676050
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_106 :
Polynomial.coeff recurrence5ExceptionalProduct 106 = -((3748433146775850138570644 * 10 ^ 70 + 1529938053360823755072520203452046112530464219415998500525421338315468) * 10 ^ 70 + 1081889004403142689223698613186958734274901480511230743263340698782771) / 27308606740609148033352100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_107 :
Polynomial.coeff recurrence5ExceptionalProduct 107 = -((31002333763990925093458302 * 10 ^ 70 + 2984738683389113864455524492889712681671828745007913437457041390523676) * 10 ^ 70 + 8514215402641863669153623703830149838462231730348185340203269021310407) / 27308606740609148033352100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_108 :
Polynomial.coeff recurrence5ExceptionalProduct 108 = ((181381614439481968809755884 * 10 ^ 70 + 7468842117133497990601178120361827653214323173999180834846023364506684) * 10 ^ 70 + 5892270565399507780105583183380532229997958481259283621328543474015489) / 13654303370304574016676050
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_109 :
Polynomial.coeff recurrence5ExceptionalProduct 109 = -((454435353822923714050332420 * 10 ^ 70 + 5341593948547138040825801111064382915946425839689633258958687437533422) * 10 ^ 70 + 4615304869212445082118636136461198478238338592314731811102278812635189) / 5461721348121829606670420
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_110 :
Polynomial.coeff recurrence5ExceptionalProduct 110 = ((1993927799133381581979132791 * 10 ^ 70 + 7835001750868585540514915510409212650536055042544201026570828418747923) * 10 ^ 70 + 2896851019568251130447848055686725328628606204098732790317152657527187) / 5461721348121829606670420
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_111 :
Polynomial.coeff recurrence5ExceptionalProduct 111 = -((6831771612962526212707374511 * 10 ^ 70 + 1876467585455529832804620032095610002160126935590712084231989193097115) * 10 ^ 70 + 9485507035275147742932198423530344148296434074562536809654703097565311) / 6827151685152287008338025
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_112 :
Polynomial.coeff recurrence5ExceptionalProduct 112 = -((13151539395374226813519856796 * 10 ^ 70 + 5188936442831033208244369171500089045105994108708574862797818770733923) * 10 ^ 70 + 7370916959969225476042992214460653275259524264800840210844271318957447) / 27308606740609148033352100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_113 :
Polynomial.coeff recurrence5ExceptionalProduct 113 = ((749962343399969674482040969032 * 10 ^ 70 + 2718186247755655702816471587691554356705455097849119962370009989981099) * 10 ^ 70 + 1321481668385642168099519195888904376768478563220805425299230244159341) / 27308606740609148033352100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_114 :
Polynomial.coeff recurrence5ExceptionalProduct 114 = -((1455880046652144405829588360011 * 10 ^ 70 + 1784609401338548304107185420262340576489713656370622030275888624943037) * 10 ^ 70 + 8227409952298395397635287670824933266313799040657154715841216273992443) / 6827151685152287008338025
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_115 :
Polynomial.coeff recurrence5ExceptionalProduct 115 = ((30397425965435677964621296877866 * 10 ^ 70 + 3741307842904521191182045767496126210883077961162578402005185924243585) * 10 ^ 70 + 5845614951379117332805105708504389992093095459704487522531933505815789) / 27308606740609148033352100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_116 :
Polynomial.coeff recurrence5ExceptionalProduct 116 = -((29247300461468840510450361019630 * 10 ^ 70 + 1829368779062152481200807469244596475395503068710705894354359064028043) * 10 ^ 70 + 9115337106561164404980244924247794583732972542223260911726823387290221) / 6827151685152287008338025
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_117 :
Polynomial.coeff recurrence5ExceptionalProduct 117 = ((56590283438826424757581796679692 * 10 ^ 70 + 9994547242442366014222924822243802466431551110703623013745293719301897) * 10 ^ 70 + 6121098693795178190216329266075298031450815108939468430872575920557669) / 5461721348121829606670420
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_118 :
Polynomial.coeff recurrence5ExceptionalProduct 118 = ((106073662999367427537026835908540 * 10 ^ 70 + 5713487284436307612552257155990015848448341440050133608985092412365897) * 10 ^ 70 + 2466392027187346874304777179386098353878652854675955783004044664884119) / 13654303370304574016676050
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_119 :
Polynomial.coeff recurrence5ExceptionalProduct 119 = -((7517507360565647176062753307838224 * 10 ^ 70 + 3638189701876969028189597628883486581514500692622745433264640223402231) * 10 ^ 70 + 1993605221807666731943968238792076305809152652933204202698412763173509) / 27308606740609148033352100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_120 :
Polynomial.coeff recurrence5ExceptionalProduct 120 = ((10975872586147674391686930623664955 * 10 ^ 70 + 6075859377152708436105135840968626505770575784180323896485475202189072) * 10 ^ 70 + 7810101042304110016030924380793141363384332465017338793512366693974307) / 5461721348121829606670420
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_121 :
Polynomial.coeff recurrence5ExceptionalProduct 121 = -((140366715736810695826383752792861516 * 10 ^ 70 + 8311119172882754285204974966387025526163408498396836403297869538855794) * 10 ^ 70 + 9982857445602756806407054251433098779769393137080059098157071253303497) / 13654303370304574016676050
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_122 :
Polynomial.coeff recurrence5ExceptionalProduct 122 = ((280323465116698575709917872760448180 * 10 ^ 70 + 185798442353901071441113148038249465509280721499600426513473160715961) * 10 ^ 70 + 662936886291632516595739123739121753722327288419768465176390386679048) / 6827151685152287008338025