Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence5LookupScalar0MainPart0.Coefficients160To190

Recurrence 5 lookup certificate: Scalar0Main 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.recurrence5Scalar0Main_coeff_160 :
Polynomial.coeff recurrence5Scalar0Main 160 = -(((((27 * 10 ^ 70 + 9256435911324353071291301928539825209647028183732403037184499549444031) * 10 ^ 70 + 591832502921189438980077767940063996028345095206299119147343319779936) * 10 ^ 70 + 7140319581742389218388106203960750301225553901112726747975297586603052) * 10 ^ 70 + 4866337115997685101610316720223284671811637051216615815559593683429564) * 10 ^ 70 + 6541368208001107552056387915159881006511720122359000282321751135970133)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_161 :
Polynomial.coeff recurrence5Scalar0Main 161 = ((((65 * 10 ^ 70 + 8490817656237927186792929420372644488671557867384626239491728025729146) * 10 ^ 70 + 1544344870967188433886718739419059741255399807846271387652036819255350) * 10 ^ 70 + 7364805817854284626897687912983810173319514550756961567817851554919079) * 10 ^ 70 + 162222816010982698603268501042205056770800081936513860249542978634623) * 10 ^ 70 + 3840268066807237951444692024503731039611389151966355408414937040867589
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_162 :
Polynomial.coeff recurrence5Scalar0Main 162 = -(((((152 * 10 ^ 70 + 4770207181429895544168545197895091977361085663764814303334119222786275) * 10 ^ 70 + 6036662617737822755724649656808122541328790745739183354516008881971961) * 10 ^ 70 + 399681331399877364772724288950180051128553723324022857590786934523319) * 10 ^ 70 + 8071072196100357657085722657779906953313332294483827843222453837869470) * 10 ^ 70 + 2417172606064228242539431495355763762239824900755615980663977039752769)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_163 :
Polynomial.coeff recurrence5Scalar0Main 163 = ((((346 * 10 ^ 70 + 7354136199671636150147310209686920018624343933536137944352913563579370) * 10 ^ 70 + 9876158818533488657287565250117671972402530134947736817537883821338094) * 10 ^ 70 + 7725591265091121640647402042903476028620121151341795473135650446562448) * 10 ^ 70 + 3670433889736585234553304494850764497909495210529347647449167592440350) * 10 ^ 70 + 545558947367008038085532369362491411805976399373287162444431443281767
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_164 :
Polynomial.coeff recurrence5Scalar0Main 164 = -(((((774 * 10 ^ 70 + 3928952885221816564709675305796265191945545353094441977845138264878789) * 10 ^ 70 + 3872020915304169187847625492439606254835728939156477408512419339918591) * 10 ^ 70 + 6813265136931973159375539127184849181158250030788049800308471810769169) * 10 ^ 70 + 6170962160596382936395480601816281193793524002728559693552089661109117) * 10 ^ 70 + 5527385385741648301821080827389955864167899278103575138092538408422614)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_165 :
Polynomial.coeff recurrence5Scalar0Main 165 = ((((1698 * 10 ^ 70 + 7261368150763537141479818678753949231307010353553219521228170365370732) * 10 ^ 70 + 9065443566487916355779196559167103926972864559558042473415480923507239) * 10 ^ 70 + 9111961162765749362622664982144330183502024169420351332840470237252234) * 10 ^ 70 + 7449713032009155181722673470661171121304067270072523766547481546418232) * 10 ^ 70 + 2506115056535583477086541006888885188770079785523458767452775679051003
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_166 :
Polynomial.coeff recurrence5Scalar0Main 166 = -(((((3660 * 10 ^ 70 + 2690284089908474027820939439414551999730380863104331650114334528187116) * 10 ^ 70 + 2160029654675149929890295819041857215919739066076221234826891791752411) * 10 ^ 70 + 7270966041898162882692302952328638799429385859233579815266120848686870) * 10 ^ 70 + 5541278392022769364931687865677600777462485607667825934879254751701479) * 10 ^ 70 + 730488573698655141900890007666005769905162893230754151277333656958503)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_167 :
Polynomial.coeff recurrence5Scalar0Main 167 = ((((7747 * 10 ^ 70 + 4425093265701723738176880476264299776063538041381540263681830797750761) * 10 ^ 70 + 2524365536124338366705536216366862053915411238987414409661533690160915) * 10 ^ 70 + 7772088082641753766469716797442900634305547884295100553614777042599635) * 10 ^ 70 + 6443239736271812569675182788008227053206093107375999550559982679181151) * 10 ^ 70 + 9795493024409582036197824748798184534498479551065774608560658260445062
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_168 :
Polynomial.coeff recurrence5Scalar0Main 168 = -(((((16109 * 10 ^ 70 + 6777317493121103767276182017940499238649560575369241494444801062862543) * 10 ^ 70 + 401481616719935841314823739599531435347455225950463543208449034536300) * 10 ^ 70 + 7414194569324465927200397816273654558397320558682621221837846647501190) * 10 ^ 70 + 9498230683013339357777781979044762916642673131378777333031970125215797) * 10 ^ 70 + 633722600436141639456021689163958347645195034159279020776734047042211)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_169 :
Polynomial.coeff recurrence5Scalar0Main 169 = ((((32909 * 10 ^ 70 + 8003780689381898251435128797710030670410762461199660669969719052772820) * 10 ^ 70 + 9818848356514099005023975930749189542409956603761276848754023715693224) * 10 ^ 70 + 4967374081330692471185696292344197650520600685307222533698455090933773) * 10 ^ 70 + 5747486336751911817745982334486848938774759730190766334556334304747389) * 10 ^ 70 + 6039130843133389205977460378406201515915488402855418373207074695757721
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_170 :
Polynomial.coeff recurrence5Scalar0Main 170 = -(((((66054 * 10 ^ 70 + 864775807390685318180736088096274717554580218048772579172626920774978) * 10 ^ 70 + 5094676413724226923024953565769682417234843316684411106061273464077983) * 10 ^ 70 + 2746646998525914099548967810227193249034493551858429025397132572668569) * 10 ^ 70 + 5336162365705026474118258608190798587654272031190647566744779567368145) * 10 ^ 70 + 763063851493460880108691087903623904337132563619651269273629217442453)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_171 :
Polynomial.coeff recurrence5Scalar0Main 171 = ((((130267 * 10 ^ 70 + 3913966256539621043437875800496066957548915769502625774804978390483892) * 10 ^ 70 + 2234489698838736458822733880126961765267266935137574944130998113326716) * 10 ^ 70 + 2481016465368143872051851017560765885810053011622821877954324732851620) * 10 ^ 70 + 6457782378186851465499363102184723888927972604445198578859892731348683) * 10 ^ 70 + 330909873903318339748042876964175799463454972321976560241431644627139
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_172 :
Polynomial.coeff recurrence5Scalar0Main 172 = -(((((252440 * 10 ^ 70 + 603940738145149443243754043870910185623804940577351209040268705434706) * 10 ^ 70 + 3277741411587011767663107184622322147361064756044762596187201381566368) * 10 ^ 70 + 8747022084191344890000488502375261067070526619188158172535659956689368) * 10 ^ 70 + 4411258311420139411760869822904553718245374253563558704660294748836715) * 10 ^ 70 + 9765980561177213392685705121460959000705045217586770876294104579831560)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_173 :
Polynomial.coeff recurrence5Scalar0Main 173 = ((((480719 * 10 ^ 70 + 5142577169503436934773781524434661675859478305328979547493228391079047) * 10 ^ 70 + 7047433996929225743281154111503660616742161193700422159943204024137869) * 10 ^ 70 + 7607124057020192143072759129023065706299491028623954990005094221555077) * 10 ^ 70 + 7227969962241540061043631984312178254356261658155995774415455423759348) * 10 ^ 70 + 2553296773234705846789830847356398192695122581645356459781262570289512
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_174 :
Polynomial.coeff recurrence5Scalar0Main 174 = -(((((899621 * 10 ^ 70 + 8328173875776864502580981623873370740160631488353606120352832570244465) * 10 ^ 70 + 2423683438230815749456045385761691804436577137582040137273384843429708) * 10 ^ 70 + 3429837375910932786639445168373895926219809079805857354762598912883346) * 10 ^ 70 + 1010980567824258478543671570373925490572143468987027589972009294760777) * 10 ^ 70 + 2276382217725118440039809378160668507013629932332261348534015374477641)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_175 :
Polynomial.coeff recurrence5Scalar0Main 175 = ((((1654574 * 10 ^ 70 + 3772670136735559528038363260596371532190639510136680384741489986044222) * 10 ^ 70 + 6712379149950326375201536363846563384845753706028262792430834011107196) * 10 ^ 70 + 5129466849496170098771578488027760616926060993897602514944006230485020) * 10 ^ 70 + 9912420708948892571795303530852802785912722433279998611028384721418219) * 10 ^ 70 + 5476893132656920371353884757578296508821512140551318142941965489054922
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_176 :
Polynomial.coeff recurrence5Scalar0Main 176 = -(((((2990842 * 10 ^ 70 + 1114477919727829420971290417682013710576363648683563992599600771217339) * 10 ^ 70 + 1311232830811056999411771352297126478828667777953335241706789473597083) * 10 ^ 70 + 3351906211484409159382941927092249675993308559003944302009210381549526) * 10 ^ 70 + 5124338232012783694572477291396783556783412505687842188742619771871207) * 10 ^ 70 + 2179568038041397144149614877691762407378860992482018292946702502132538)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_177 :
Polynomial.coeff recurrence5Scalar0Main 177 = ((((5313783 * 10 ^ 70 + 9313247921054226750534017391636810636801792396297082428123267939646790) * 10 ^ 70 + 4888172967344919413304801579849511375377468914967034365155170010525737) * 10 ^ 70 + 4234336007831389804770771066771265412940708089942206071397301031850465) * 10 ^ 70 + 554378617611726959336577169543872999967872350294923694180229682191841) * 10 ^ 70 + 3083139346252244839814160381599405406483543066209245858564831904954097
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_178 :
Polynomial.coeff recurrence5Scalar0Main 178 = -(((((9279816 * 10 ^ 70 + 1210117371154704311406919244507088146481258953297823718512654651952350) * 10 ^ 70 + 4358326132395284608290052605906340379162792512938372363523737191741232) * 10 ^ 70 + 1061614591791414058054300260094263003093568781957693552403274131083065) * 10 ^ 70 + 2625531152876176416697326683029192610479444531001791385964746663627113) * 10 ^ 70 + 1552933663366731171246044052908652823006463378615796458194989870667115)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_179 :
Polynomial.coeff recurrence5Scalar0Main 179 = ((((15930204 * 10 ^ 70 + 3000069577704491195638075685411818235617995568025694267625526511667640) * 10 ^ 70 + 1480079168567054423636234052251116534829237890778258059671091203150139) * 10 ^ 70 + 8484253910925118818791968237490043865105119744560733114773445638881523) * 10 ^ 70 + 3940522358652749469906527300386426332028664030332828196775783548003449) * 10 ^ 70 + 956200683314767719681006756291699992865174764069971230637494524248783
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_180 :
Polynomial.coeff recurrence5Scalar0Main 180 = -(((((26882571 * 10 ^ 70 + 6218863391050655589305982500437282966222335788155391536115036106199319) * 10 ^ 70 + 3834319382695107646155813913722164382082784103487054656952583729583845) * 10 ^ 70 + 1529436978161162537726350643855361563920793257895614197449190661512275) * 10 ^ 70 + 4231724159906606735790748999365274673543888613461033787802918314211671) * 10 ^ 70 + 4173360553558304648711059767272147033067282081907571004605657797210112)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_181 :
Polynomial.coeff recurrence5Scalar0Main 181 = ((((44597278 * 10 ^ 70 + 9191128750665671609594600361288277624648636141885818134533764390613992) * 10 ^ 70 + 9726776892464061662054980319133611318495628877803477618818942553932431) * 10 ^ 70 + 6697346038983528544500306367434738845153264240855624619468360860286050) * 10 ^ 70 + 2879169186005902495498657707378880348211574183575431256895953066225064) * 10 ^ 70 + 6335404515204745394161144403827497646427933961763922745493424078065262
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_182 :
Polynomial.coeff recurrence5Scalar0Main 182 = -(((((72736802 * 10 ^ 70 + 1026893808564056393505349287954389562623833957826619728530679435584612) * 10 ^ 70 + 9455540824117407717556096557119188957273026253569486237651496994228403) * 10 ^ 70 + 5042690054319447331817496878402055523418405238456026626010073694947114) * 10 ^ 70 + 4469100677551191214775017297226164323428456002053502815598277117026360) * 10 ^ 70 + 8487493466687483915208919373615558004679736188474563674064719492944474)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_183 :
Polynomial.coeff recurrence5Scalar0Main 183 = ((((116634808 * 10 ^ 70 + 8332007829050746694556317221386424392601606730999201659509403436683455) * 10 ^ 70 + 8547495759709833884480826536112838056706751606081983368853195341151532) * 10 ^ 70 + 4174279786586712583783555172408668968246093848993270095630370044186510) * 10 ^ 70 + 9389178382718845952616681559761124112405581412960513187454005294966476) * 10 ^ 70 + 9117893206047345709447672985555394799418619585887134045448116106819449
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_184 :
Polynomial.coeff recurrence5Scalar0Main 184 = -(((((183886478 * 10 ^ 70 + 8631513674498713386405722322867025574989473390925234531838097188992564) * 10 ^ 70 + 2211557688972659918204188093548398189532367628372293986782652367806657) * 10 ^ 70 + 3237885635438296100242630580259403267543392146002251807715847100857078) * 10 ^ 70 + 1740293150110881550526453095471784570060487884346731840026104210831890) * 10 ^ 70 + 9096140756645182159748212145052160785663051340947497222519493131454232)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_185 :
Polynomial.coeff recurrence5Scalar0Main 185 = ((((285061274 * 10 ^ 70 + 1798658407682352063706540230375258630198195979869413744975531374472370) * 10 ^ 70 + 5128509008375643037265369961385959922153661795125479177991604964021567) * 10 ^ 70 + 5512542163760076075719767642742956399686122674930506825455869980646863) * 10 ^ 70 + 3787000065018043726409082159822297933485655899794248676621610329162872) * 10 ^ 70 + 7847864519243492237784574100677099398141780336173360483548895587694671
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_186 :
Polynomial.coeff recurrence5Scalar0Main 186 = -(((((434522554 * 10 ^ 70 + 9206460507254485652572058209685015399102806695113995547296870731664923) * 10 ^ 70 + 4697022836649865894241830293648373922413915292643275133271479123644039) * 10 ^ 70 + 5797355343620714460482460311206173338009730097064624907808973623319387) * 10 ^ 70 + 1698765557043769089692479547872047774456939501758816440305992850295875) * 10 ^ 70 + 6164491984518248431587463818111561606779250619092734596879904618280185)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_187 :
Polynomial.coeff recurrence5Scalar0Main 187 = ((((651314402 * 10 ^ 70 + 7113126651999240876360626746595816881839666147528348976931956807627082) * 10 ^ 70 + 649694351583103576486753807236611465220350283723191930291341938771991) * 10 ^ 70 + 5683990271681692997862699134353867367906623160526286088438662099989052) * 10 ^ 70 + 2900271934897147865776696553812846525115515063458270487154360223887374) * 10 ^ 70 + 9234561680041995929070945594829330426911896292503747459571957240825511
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_188 :
Polynomial.coeff recurrence5Scalar0Main 188 = -(((((960045023 * 10 ^ 70 + 2320393054855685170690568342610231279410675418157070584046378329071095) * 10 ^ 70 + 638819205504431504759397838973516944216029240535061465771411693951827) * 10 ^ 70 + 4963297894821052969814014494842876430689172387098852959234987263785631) * 10 ^ 70 + 7830622398407946452418249475248125161905882097203645031627758640566048) * 10 ^ 70 + 4006628869693690726851831471189181772094613441165310140725690715956998)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_189 :
Polynomial.coeff recurrence5Scalar0Main 189 = ((((1391659955 * 10 ^ 70 + 5798457869299522346153945795551786539850045831907675473099260686553356) * 10 ^ 70 + 8872718841244190594122800400330478581459808502950742315567959800763937) * 10 ^ 70 + 9873239983462027085099209446039124402403524632085826623841508930216978) * 10 ^ 70 + 2932901866585460021597582571459446692578597613305323086469816796054856) * 10 ^ 70 + 851787828880033993784872137819751679064427269933172786974595138654478
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_190 :
Polynomial.coeff recurrence5Scalar0Main 190 = -(((((1983960776 * 10 ^ 70 + 9540785511416465078179514189601926899068097477413712400691870732818189) * 10 ^ 70 + 3405807560708880145940086088227321927888850021527890771174012635835453) * 10 ^ 70 + 1101896117788519390154839189510573078184748572929342332039027430838893) * 10 ^ 70 + 5978409246570663595110267267079354894642956785646582827218172125358146) * 10 ^ 70 + 5584387718160611644473561138773623263064657583622415054420225097850924)