Recurrence 4 lookup certificate: Scalar2Left coefficient convolution #
This is a checked coefficient-lookup shard for the fourth pseudo-division recurrence in the order-seven certificate.
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_194 :
Polynomial.coeff recurrence4Scalar2Left 194 = (((1543441625258243593 * 10 ^ 70 + 8015368828489678763701354029784068732112837896471068829155899082771544) * 10 ^ 70 + 5517561538422550714884814709400990637106806009252737235707617669870451) * 10 ^ 70 + 8378345012370274646954732647939573197801843241109878142756343513059443) * 10 ^ 70 + 9727470303791088834372999403003530848679348003471784543390637048514308
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_195 :
Polynomial.coeff recurrence4Scalar2Left 195 = -((((3362688745125887768 * 10 ^ 70 + 2519930330990588597761652550453543594919187374024003099765211844205799) * 10 ^ 70 + 9690956328021668876794561079266042935724035861870355480053933808406030) * 10 ^ 70 + 5074499425576431755415322283506588906379093398658590072420322752001602) * 10 ^ 70 + 5552623372951947125559964757562206832307119531500749822663955329615668)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_196 :
Polynomial.coeff recurrence4Scalar2Left 196 = (((7222198643011971138 * 10 ^ 70 + 2571417563724442550141762778549766927755609023690453194110160522071161) * 10 ^ 70 + 3341585498895573378654623605256225271817270266412958872808826750869645) * 10 ^ 70 + 2586399731472222058944665056838288083623675818425391918979790864059228) * 10 ^ 70 + 6128809931603311714720214005561404123110006902836102477867976461925246
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_197 :
Polynomial.coeff recurrence4Scalar2Left 197 = -((((15291366944605894216 * 10 ^ 70 + 9210293589775570473909932522591983464245826832236447703512408998000883) * 10 ^ 70 + 2721586470752729521079925377678491120728699574551241795865325215217280) * 10 ^ 70 + 4493985545673113756979679514922038511164887278319976839861086786116534) * 10 ^ 70 + 4267457585812561301129834448388921499517348189684987008324621996490491)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_198 :
Polynomial.coeff recurrence4Scalar2Left 198 = (((31917174514393117839 * 10 ^ 70 + 9600944958377307834216176768701135988767587950013521005099266133038070) * 10 ^ 70 + 9774699497918937568196450118683672311917178741658384340408246944085086) * 10 ^ 70 + 2996358036267516285098870301753802450583898318298243610565986980171785) * 10 ^ 70 + 6280437021647228042118048523869365785133532342055345021320864348841295
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_199 :
Polynomial.coeff recurrence4Scalar2Left 199 = -((((65676534384883816194 * 10 ^ 70 + 3501817607527739483383261267022364126374005290685550962300059858818633) * 10 ^ 70 + 8117155247692798777513655413886622955434277817634114770736485170062999) * 10 ^ 70 + 5822755060691407240176872666754725178542118223133273164371338529961504) * 10 ^ 70 + 758693474366028830051235178510300768058445403073504989540316739174743)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_200 :
Polynomial.coeff recurrence4Scalar2Left 200 = (((133232251866107762411 * 10 ^ 70 + 8351955190591435852397481903026682331072515714111374211428163126573264) * 10 ^ 70 + 6190484801563346591694936058024309195556870022322810650222264683106577) * 10 ^ 70 + 4119623696598669009574931060509909242007892907777025858843269877186122) * 10 ^ 70 + 3610299574573791985323665781045644848884755356405721862757779743087672
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_201 :
Polynomial.coeff recurrence4Scalar2Left 201 = -((((266456799638813311269 * 10 ^ 70 + 293347069941054555561755590448795418388455304769954378235624161311028) * 10 ^ 70 + 5076845831426045864613274991666225457639102042060580558057867492105693) * 10 ^ 70 + 789674538703977870136750230104269962901248746938624441471137099966964) * 10 ^ 70 + 7836378511219475383782499298670112356601639971307053854594430863976962)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_202 :
Polynomial.coeff recurrence4Scalar2Left 202 = (((525371770191442326870 * 10 ^ 70 + 2017269461715106607006827557054054426708740544912297935867967166247054) * 10 ^ 70 + 5169942552134592403371383504398489406197767965876482337391421842895664) * 10 ^ 70 + 8323435849986544192832682380081706413117794040609595196208151941056637) * 10 ^ 70 + 6533191980611348523581251368178512982696064730073898770906904329375207
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_203 :
Polynomial.coeff recurrence4Scalar2Left 203 = -((((1021251136765573429480 * 10 ^ 70 + 6840729894796334058280883640549626098707154060391969224563766388082110) * 10 ^ 70 + 5487993575623988871379813296317349857953876888206282258109449038168085) * 10 ^ 70 + 3908343443566787016447399007104858566626261995098997970308444530199489) * 10 ^ 70 + 4441649120141235413561576860378668072626975240894837358006189315113795)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_204 :
Polynomial.coeff recurrence4Scalar2Left 204 = (((1957162426924418915784 * 10 ^ 70 + 6347506670587511284046881903604314325672977084939196529179860104598910) * 10 ^ 70 + 6110688544095326421947837217650011102215860481519571078206421289173959) * 10 ^ 70 + 1775771976083678772589094224370482015769435839859096563955949246769720) * 10 ^ 70 + 3471247872052128298428031513910647571149430728045504982808293010605776
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_205 :
Polynomial.coeff recurrence4Scalar2Left 205 = -((((3697868429711283940374 * 10 ^ 70 + 2456267064609342831572552977104961870564085577667929582800250513407539) * 10 ^ 70 + 9430746430918007192952487673893872370467014377031903012007818417334469) * 10 ^ 70 + 7020502015078900503934832684662420736830955700561971421877389357073540) * 10 ^ 70 + 576355993545131233301807809355954244818955622110496541647031823591306)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_206 :
Polynomial.coeff recurrence4Scalar2Left 206 = (((6888223317773582821223 * 10 ^ 70 + 7555864636444457153671985500142090532179998378403887903189055021218101) * 10 ^ 70 + 2353157828261523673381623779806221435665275487723133400887466781635485) * 10 ^ 70 + 282832946075289449759709617124130923528595767896348337236442410887302) * 10 ^ 70 + 8218436128823193431255991456957492723005889794810016858639073639025691
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_207 :
Polynomial.coeff recurrence4Scalar2Left 207 = -((((12650106319834758164389 * 10 ^ 70 + 5020129499803051622015829745891103478786703442538376138173924731006737) * 10 ^ 70 + 4214178935150752903981975607233252100785980969962251702585537940931789) * 10 ^ 70 + 8448376601392162031838211569788023203295415608847449480382371794726929) * 10 ^ 70 + 9735687308007239354009029073705284064971031496865643946754610082301708)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_208 :
Polynomial.coeff recurrence4Scalar2Left 208 = (((22904003820542290947070 * 10 ^ 70 + 4252043709483417545167421684671637291012335862898687836143391626921396) * 10 ^ 70 + 4686940325951464244997544038977805772997547734291188451849854513498917) * 10 ^ 70 + 3785061423705111316634803044004421206645205716289042048142598669155537) * 10 ^ 70 + 8981997159896224122679545654976188760609736989560958116590420128120951
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_209 :
Polynomial.coeff recurrence4Scalar2Left 209 = -((((40884342679984804845390 * 10 ^ 70 + 5126950420867638659100122232338025437396755318135570249289300275062836) * 10 ^ 70 + 9062086373055067058923224742987887811219686365393196829464868336473506) * 10 ^ 70 + 5059845090218008272866348748786821417388646382269986775719170823511887) * 10 ^ 70 + 1810202352531287483820827855761645149773223259721789062246798729444034)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_210 :
Polynomial.coeff recurrence4Scalar2Left 210 = (((71949552087118721235762 * 10 ^ 70 + 1142223055440623136113838446644536079396359714265374552272560093101280) * 10 ^ 70 + 3057238272131854500073690389167155178810767705887639026427700908575833) * 10 ^ 70 + 66359601046144625964025233647743449869736326766375680584241823209414) * 10 ^ 70 + 4206159529160964932670175348775737762869298994829767231800217667231895
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_211 :
Polynomial.coeff recurrence4Scalar2Left 211 = -((((124830479071582926584922 * 10 ^ 70 + 6677705122540710508939866069714083680536831483404802208912393157158844) * 10 ^ 70 + 7934518036073321699128713291966948343333934989071399617516971706904155) * 10 ^ 70 + 7774132783152434933882358133146222703646052219484366064614397484060449) * 10 ^ 70 + 4216955446432799962493877640014754880726674921065109068680830848816632)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_212 :
Polynomial.coeff recurrence4Scalar2Left 212 = (((213515553102202429493131 * 10 ^ 70 + 6808578771851564671587793086023264662490735736382874302575114136852213) * 10 ^ 70 + 4624890134103045773234163238374647605044563725260110906288302092750209) * 10 ^ 70 + 6675732749508025745260141357755923482925976191488842564435011412997042) * 10 ^ 70 + 7769763033775763514334478235140110717789934290901294568224221145541957
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_213 :
Polynomial.coeff recurrence4Scalar2Left 213 = -((((360038044651331041688748 * 10 ^ 70 + 3576618582684189557276431501112653334193966684450635104468460623872113) * 10 ^ 70 + 3778313593337850075790727818328432041737231157160145792605009628895924) * 10 ^ 70 + 306672484480448150772443692145809173886443713674700293879433538191601) * 10 ^ 70 + 4296412737757535441832534575710947116071252592157430268684645554333416)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_214 :
Polynomial.coeff recurrence4Scalar2Left 214 = (((598507583292484760759001 * 10 ^ 70 + 810574286000177992153159998162866546603470381348600064045573539121531) * 10 ^ 70 + 2491317119919572786786244360529051458119329209122662634373057728401475) * 10 ^ 70 + 1394928504646126184205690719552705097867952038317691136627077653969650) * 10 ^ 70 + 475897787478196456958805064924135826060007643421902437877506135133664
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_215 :
Polynomial.coeff recurrence4Scalar2Left 215 = -((((980808734173009228714100 * 10 ^ 70 + 1244310734067934883951991066977152038967435353247297066672800128382409) * 10 ^ 70 + 7944761755156529063585650415969246512003546026182957361228619069603286) * 10 ^ 70 + 8749479735227821353453961693113490674351700088949670025209130028855338) * 10 ^ 70 + 418238817085921061908788332932743407864374811600948848289774058087837)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_216 :
Polynomial.coeff recurrence4Scalar2Left 216 = (((1584462464147224873363107 * 10 ^ 70 + 5809371828101830725080321159519351485332099703943378333399432930367216) * 10 ^ 70 + 6222264696307430211266642813719251070035954603825801126400843589693049) * 10 ^ 70 + 5307485208218400357093939332246170190971789565058657416929657157549031) * 10 ^ 70 + 1092483377247335473902325338830984240715492860592402046669384917299272
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_217 :
Polynomial.coeff recurrence4Scalar2Left 217 = -((((2523193400019450058073365 * 10 ^ 70 + 7081499619657452023198777323326332122654169260268234808929601148730716) * 10 ^ 70 + 3081120174526963802239387356151322862726385354554458256413863603297639) * 10 ^ 70 + 2291943193053523651723026057280738276218059932995593460012410334996691) * 10 ^ 70 + 6544228143361682094887049623750376622263965804078026291234224563900461)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_218 :
Polynomial.coeff recurrence4Scalar2Left 218 = (((3960740404063766048446010 * 10 ^ 70 + 1474745191564937727658364500220017910053524699921215258609031382937757) * 10 ^ 70 + 6907003469782198207115178942918397100385048225867760672988234333956471) * 10 ^ 70 + 5237045548432195067625685684319661713168253295833407809437444231408410) * 10 ^ 70 + 9642099202952675382776661516727150346730559446876230994760454390004141
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_219 :
Polynomial.coeff recurrence4Scalar2Left 219 = -((((6128355373115508369633805 * 10 ^ 70 + 9297028593672219591880921616903340842944175792757597670154364276500184) * 10 ^ 70 + 9867272944301920817018603789162587658326869993781054532333947140597846) * 10 ^ 70 + 7547426279768899106296050525958899327164424175545676829433877967660156) * 10 ^ 70 + 7539494113271329427850475990116344627526590353126223753522453788423091)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_220 :
Polynomial.coeff recurrence4Scalar2Left 220 = (((9346213776150305779465312 * 10 ^ 70 + 7531609384744737685805777686298846652363509385730111045508340820625045) * 10 ^ 70 + 6047226515600139118766918198673331320598201755455509779264663196843638) * 10 ^ 70 + 7176485058142457510830718579487964706342685451092543362306828891282120) * 10 ^ 70 + 9678711114484802301490510064749941316932383512512970384615805917709401
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_221 :
Polynomial.coeff recurrence4Scalar2Left 221 = -((((14048566140220743025274664 * 10 ^ 70 + 8817191899767434919674887777190807406431939771178851624720319483606453) * 10 ^ 70 + 7412603228198348676066040954525616538921437924411178636897901995095997) * 10 ^ 70 + 553104451409501967708483553841425557327655723922599953140841637707883) * 10 ^ 70 + 4900756003018303047747469368242639130710156063138183542260826700743779)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_222 :
Polynomial.coeff recurrence4Scalar2Left 222 = (((20811853109689536044461476 * 10 ^ 70 + 5698767483260898984556030632964373332971582150742682731166289150093790) * 10 ^ 70 + 293688629606655393665163388700491626743141021876624405330692302793202) * 10 ^ 70 + 744235073161658761721456555177028904412164708292082733524845124335766) * 10 ^ 70 + 5757195072593008042514727906254453887833204659166426590194059217122250
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_223 :
Polynomial.coeff recurrence4Scalar2Left 223 = -((((30384164210308966712866578 * 10 ^ 70 + 3612497719086240818950200391102334432837256660368032952314560124805571) * 10 ^ 70 + 5818903268003948144067947972317812155744901911289875252339028763576943) * 10 ^ 70 + 9725884558126811052367741985074590195429355454871364051386776987647611) * 10 ^ 70 + 5328476137295921689918627612621035132644756834512730888374120251271457)