Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupScalar1ShiftPart0.Coefficients155To195

Recurrence 2 lookup certificate: Scalar1Shift 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.recurrence2Scalar1Shift_coeff_155 :
Polynomial.coeff recurrence2Scalar1Shift 155 = (886990317553417365340326079102889722403428 * 10 ^ 70 + 3485513170805482829383718500811227782583837647602068159557611407961313) * 10 ^ 70 + 9746948229228646903379519017499391097463814372271744651759034996648256
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_156 :
Polynomial.coeff recurrence2Scalar1Shift 156 = -((15589233748526093483384983207191922098328156 * 10 ^ 70 + 5708571628820793838816359674699388235869143283408155421914178470654048) * 10 ^ 70 + 7150921329751549208758476748056447720093267160829452762878677154122916)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_157 :
Polynomial.coeff recurrence2Scalar1Shift 157 = (46035707375859882669916432932738522719530436 * 10 ^ 70 + 637967144010813619688789538574251069856774376904761682387096166265195) * 10 ^ 70 + 4168912328324689267755949356246875490830012531705787540191060161981510
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_158 :
Polynomial.coeff recurrence2Scalar1Shift 158 = (22142169091010871485334738454193585926296238 * 10 ^ 70 + 2219688386379161470278184870833406279253271398417126564030872076589017) * 10 ^ 70 + 8421163027996693527948456285724873017089903141807235234861574292409715
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_159 :
Polynomial.coeff recurrence2Scalar1Shift 159 = -((643971369409455896330066124950108607547529957 * 10 ^ 70 + 894768667670536250354892665249617330848416627395238399105742607021685) * 10 ^ 70 + 3065743290741230023606071315851630599260570087779889016085783601122585)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_160 :
Polynomial.coeff recurrence2Scalar1Shift 160 = (2165128139851453263258489515387902443626227674 * 10 ^ 70 + 8226606513746886640158950077652087356685053935819247288336468132734645) * 10 ^ 70 + 3694212365322063615513111711717695609740862707724196901959461706539643
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_161 :
Polynomial.coeff recurrence2Scalar1Shift 161 = -((650679071797269329048492666663346648169868271 * 10 ^ 70 + 5022273739802654957140349008538401138870643215876576054950678657575686) * 10 ^ 70 + 2160092452312739890276676765372447293689579135156959648889139774428334)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_162 :
Polynomial.coeff recurrence2Scalar1Shift 162 = -((22443834002416588365733528769099420790632531145 * 10 ^ 70 + 8650331387975975921256988342030588138863835674345251885987705369679168) * 10 ^ 70 + 3408447547350557155642381683221493769736025968624605473433280173499464)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_163 :
Polynomial.coeff recurrence2Scalar1Shift 163 = (92966824065307781179311106749323414578710709034 * 10 ^ 70 + 1361342290698882740817668388773051990831221314780292975027582414957842) * 10 ^ 70 + 389637717920891936754818888465104653393357847231393261608484244992826
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_164 :
Polynomial.coeff recurrence2Scalar1Shift 164 = -((107265744927887245643085483391415581528376730975 * 10 ^ 70 + 5776559872929034693267768841346809556359478575515905349456207064771812) * 10 ^ 70 + 2552242541112383168874399057251587976743586025385111497252973149425373)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_165 :
Polynomial.coeff recurrence2Scalar1Shift 165 = -((595390139376457092622470288088090112606515832448 * 10 ^ 70 + 3700422056781712566571822460780346403107054975034754679617793318744000) * 10 ^ 70 + 3040437469053315151807872720261734542224659567954618281780466238255289)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_166 :
Polynomial.coeff recurrence2Scalar1Shift 166 = (3408538964072156855035266622309015045699736104321 * 10 ^ 70 + 7422604290556580941672506932892931845457534030951683595437264469293846) * 10 ^ 70 + 792951726801970509422991721749105936064950190299262749625455830675790
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_167 :
Polynomial.coeff recurrence2Scalar1Shift 167 = -((6818367262245516794490646341963396705315205707592 * 10 ^ 70 + 2328765185461233969237544821236960809644855695188247797727256334614229) * 10 ^ 70 + 3051415112596258469219564419315752127152036220392312220392025159336483)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_168 :
Polynomial.coeff recurrence2Scalar1Shift 168 = -((8721694667701095384220789250434751279410308153540 * 10 ^ 70 + 9103626826504303600050621763148309236020291543107810877106461623640959) * 10 ^ 70 + 584685756606733100626037783267702170301615537979152827084876403579107)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_169 :
Polynomial.coeff recurrence2Scalar1Shift 169 = (101302537739292624382549817470854261424589063728256 * 10 ^ 70 + 3026280211785199165039709850688360249977022156227983805148693765384003) * 10 ^ 70 + 2665117994370880927014836478895190637833152780835067842334037376407289
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_170 :
Polynomial.coeff recurrence2Scalar1Shift 170 = -((299663067914350216652652164772621190020576859293972 * 10 ^ 70 + 5915012580357120376026767934454604342964136094788774005900943545129370) * 10 ^ 70 + 2951802167853971985771761642950059265397862578738251426072916122886023)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_171 :
Polynomial.coeff recurrence2Scalar1Shift 171 = (162450252686980207943927544314498158687340659294593 * 10 ^ 70 + 2042390058601247454184189966776767204803592706619068713980715464276266) * 10 ^ 70 + 6326614696784288194990264012983758008744881499301102243796765016897333
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_172 :
Polynomial.coeff recurrence2Scalar1Shift 172 = (2222911371892065603072569784132997867103495564678483 * 10 ^ 70 + 8649287343806419534137023856411804462867859823890967058836965713425336) * 10 ^ 70 + 8726826765568955743940913827088057878207358745920887614684855888903775
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_173 :
Polynomial.coeff recurrence2Scalar1Shift 173 = -((9966025575126411306127249015743202195334459432331672 * 10 ^ 70 + 6659996040044604391058256506180242544271289192257101456831088143535012) * 10 ^ 70 + 4765990002343919153334918227472719495351565181159354650593522679807506)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_174 :
Polynomial.coeff recurrence2Scalar1Shift 174 = (17522568292879007538200552479607370064976768901887472 * 10 ^ 70 + 9703037494043086982087682134652513204889457810641266467462972221109338) * 10 ^ 70 + 1277926594706573743367595540178258945209189901738397774556649630613578
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_175 :
Polynomial.coeff recurrence2Scalar1Shift 175 = (23254174632860596998677397422312270023969201491066283 * 10 ^ 70 + 7232081913394119576415135254998810403405486327926016474260991094163774) * 10 ^ 70 + 147734555375448601917591422684886648106348589272390420835881810990180
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_176 :
Polynomial.coeff recurrence2Scalar1Shift 176 = -((244417521471003856794668660391864250623052224745442118 * 10 ^ 70 + 6433613145686400300965183653529668750974003624299918494579889575587005) * 10 ^ 70 + 4704478405535367333089205187627604922273835742682783310853511734736507)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_177 :
Polynomial.coeff recurrence2Scalar1Shift 177 = (730096202504125109500039931198630331738715154809541574 * 10 ^ 70 + 981293343686701860489605759970066679157588728706842957962635144398937) * 10 ^ 70 + 6934763067661306000745934901245217796035177665544783512666743199148866
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_178 :
Polynomial.coeff recurrence2Scalar1Shift 178 = -((689047925274101235986807919681218976984317505616616929 * 10 ^ 70 + 2736136317679568064823389884762013033764408410398805709367134693642241) * 10 ^ 70 + 4869911018199551728931062552206446777677619462295430432245256947644880)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_179 :
Polynomial.coeff recurrence2Scalar1Shift 179 = -((3542015753836774697872379745616527055894824561699532524 * 10 ^ 70 + 6095624584582239732701047820507081861989314217108365661255988565802267) * 10 ^ 70 + 9881975241911630091103888945652844986100214361727620813863658874571772)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_180 :
Polynomial.coeff recurrence2Scalar1Shift 180 = (19325463630617371959333399248976476920740068489848893431 * 10 ^ 70 + 7950283123339859186490031261273683055200452213757260501217172823997829) * 10 ^ 70 + 6266246425443289373696608452873683235013426594388144189242420749613362
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_181 :
Polynomial.coeff recurrence2Scalar1Shift 181 = -((45228107552762663801464364949041145771895846327899268599 * 10 ^ 70 + 3404242711265237345910440217271020079079184963701097825386407121403688) * 10 ^ 70 + 876887129545566477267623389627992871165807554388944287472649393439795)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_182 :
Polynomial.coeff recurrence2Scalar1Shift 182 = (18369247115629740771448706357053355300507692609690198483 * 10 ^ 70 + 2362322293220202338000585317763331478778393262823970562828296322538481) * 10 ^ 70 + 6205796117623520960641510615047796623945532745411494245621662709518791
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_183 :
Polynomial.coeff recurrence2Scalar1Shift 183 = (287070405650256075524028624462515387071640866001167456095 * 10 ^ 70 + 1031875006655385405987313140698559875265762167883998257789250859568252) * 10 ^ 70 + 3641302611556971292687877168782970367421879128372665732269814985536062
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_184 :
Polynomial.coeff recurrence2Scalar1Shift 184 = -((1248535514815045415873730304655401378247579246719579887476 * 10 ^ 70 + 4402331141029558345248413486971598988108871021261638448479151828118510) * 10 ^ 70 + 9283261462112197257364686968226890712452953998451951958078313050342988)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_185 :
Polynomial.coeff recurrence2Scalar1Shift 185 = (2619658967681088626413067703807365021715565823520796596586 * 10 ^ 70 + 6640019964646903054591005689908965481765974539977122610302915602048155) * 10 ^ 70 + 8248040871302298419259777965460179893035594514816865736761039189785275
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_186 :
Polynomial.coeff recurrence2Scalar1Shift 186 = -((733088739895802789571914975576636029993789130110767093722 * 10 ^ 70 + 7214407055246195757507090732586113640775643720045854479843180784888860) * 10 ^ 70 + 7085118892945211924081806379656431372957647949748528241487417521134851)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_187 :
Polynomial.coeff recurrence2Scalar1Shift 187 = -((16486739110796690907529953639944623675363714388008670313250 * 10 ^ 70 + 6476168228901685633304805389820606059500424339235074365556884942819799) * 10 ^ 70 + 3966514110117851218800970432705412594611933830317449434877478524916265)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_188 :
Polynomial.coeff recurrence2Scalar1Shift 188 = (68953939978707725027454586553831417213123980218509373452113 * 10 ^ 70 + 6908156328905351408455517156691353027127625470655388155364772152501043) * 10 ^ 70 + 8724802090137977457755557579202500029026718542830170979742669800674183
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_189 :
Polynomial.coeff recurrence2Scalar1Shift 189 = -((148967641967146029332960418902349729952487550714191899400371 * 10 ^ 70 + 268936681769637640699078007065769941638534074786201218947726364189983) * 10 ^ 70 + 1599498440873521210377373982681674431027804994683460578722828861247302)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_190 :
Polynomial.coeff recurrence2Scalar1Shift 190 = (93481402046024998103014500112789593557513043560734649027125 * 10 ^ 70 + 8797867870554273055640041181256373783582301806103995513252953749580576) * 10 ^ 70 + 5028296307112103500513097542193962342300868408314767430196116640807129
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_191 :
Polynomial.coeff recurrence2Scalar1Shift 191 = (661639847450109389544831642019700294110262714922003050769282 * 10 ^ 70 + 2006986271952568010784547146418615134343518035917365500321095576434492) * 10 ^ 70 + 7847538875675949803859509146056172332222835537847801165773799589165066
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_192 :
Polynomial.coeff recurrence2Scalar1Shift 192 = -((3188266108726376662244641539538236906147243699915858577715991 * 10 ^ 70 + 7618948272065439064720063515370086525152180547726494962637725647528657) * 10 ^ 70 + 2906431859299969800387468369040903333314249835707711302769896054661075)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_193 :
Polynomial.coeff recurrence2Scalar1Shift 193 = (7946277162688838449529748463371949961076455189598252934615987 * 10 ^ 70 + 7168102218395368048408965482550138026689193428942584583946559810876415) * 10 ^ 70 + 6620024374018259930045380896727562891255581622282027080354271133753578
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_194 :
Polynomial.coeff recurrence2Scalar1Shift 194 = -((9998117862484109462476750552147970420107245541204721805411101 * 10 ^ 70 + 4975212136300351255517878150017757126426572540801205726242469801092002) * 10 ^ 70 + 1292085703952831462358667178912302218413590719148506557163391952452003)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_195 :
Polynomial.coeff recurrence2Scalar1Shift 195 = -((12061401358978954363838035692857829789395576355263491896111596 * 10 ^ 70 + 4357647084840694932063347118023681299809807279945780927700413907969594) * 10 ^ 70 + 2234170319067185187724590897478274400884320090305918402609298643980762)