Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence5LookupScalar1LeftPart1.Coefficients251To279

Recurrence 5 lookup certificate: Scalar1Left 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.recurrence5Scalar1Left_coeff_251 :
Polynomial.coeff recurrence5Scalar1Left 251 = -(((((4156 * 10 ^ 70 + 3650990071803024719086942408998992953348969639833626207503607761612225) * 10 ^ 70 + 439810616401341252266771717461153682508797751864110971066347818013474) * 10 ^ 70 + 3832909625737823114988966557916088952817185662571416202713889752435474) * 10 ^ 70 + 6022704477346260468736410009059483069526601772770417638849260117457760) * 10 ^ 70 + 2921176082910365870359896671072778091292366271391137774497836367170421)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_252 :
Polynomial.coeff recurrence5Scalar1Left 252 = ((((14410 * 10 ^ 70 + 4362318050510494699854880567076091944704719533476536354892581992644891) * 10 ^ 70 + 2435137782895953045938963041406295781505026242251886329140040897095964) * 10 ^ 70 + 1889885141821902586325470895978748000488740395571917411179428180029159) * 10 ^ 70 + 8691154444197201909518505522176507951879180622681845380433437495147624) * 10 ^ 70 + 8753154825576208215741760712468406791449769772759609879163220514183792
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_253 :
Polynomial.coeff recurrence5Scalar1Left 253 = -(((((18859 * 10 ^ 70 + 700288199072014200517648538765771935773493353097284092976153764145397) * 10 ^ 70 + 7163927019705567878400554370615246848856188828494132248667657454354901) * 10 ^ 70 + 6072522845608516977000338038902078439374072993625508140222675405515926) * 10 ^ 70 + 9561261272775830112081126635429945254858750908575398752738563450458533) * 10 ^ 70 + 8781941517007865723792973127522960024294188593483028168014910708439518)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_254 :
Polynomial.coeff recurrence5Scalar1Left 254 = ((((19082 * 10 ^ 70 + 8779634042941004954006134823240141980535663947427526431416199181228285) * 10 ^ 70 + 7973165008021742878409001046321896841038844597469532335146235267764335) * 10 ^ 70 + 4732335270135327004507781678266578955655739204038366076134569232976009) * 10 ^ 70 + 136269870780161749277100337124476918827961545043482718136324059193979) * 10 ^ 70 + 2295908135008301247080735802710006627368526130211494949478987307409358
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_255 :
Polynomial.coeff recurrence5Scalar1Left 255 = -(((((16832 * 10 ^ 70 + 663249640578951870641593837387600171308181619337693530521804828082596) * 10 ^ 70 + 512541472979003107343844827470221913803289469637351615841574218936432) * 10 ^ 70 + 381956652063040893667853332349815155087650163005955837703630896145294) * 10 ^ 70 + 120043321980918205738273675768911930254759373235734136779049574487924) * 10 ^ 70 + 9711012247153413553637062576432042603949391986392053665596972724538178)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_256 :
Polynomial.coeff recurrence5Scalar1Left 256 = ((((13521 * 10 ^ 70 + 8978202697282720332239122407974057157340880012984914213655717251789382) * 10 ^ 70 + 3726984669721263071932919231184361192119135584020365498778621116993097) * 10 ^ 70 + 5196222901180687116385331468266730569049121553293034324438954841110300) * 10 ^ 70 + 4184718608169166587562533592509636343396435482029892298969750500699987) * 10 ^ 70 + 471985108387952444067369660662133936359813444552422325810481069125398
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_257 :
Polynomial.coeff recurrence5Scalar1Left 257 = -(((((10098 * 10 ^ 70 + 4497397281666817465853824793846604055332915247080729709263319012001806) * 10 ^ 70 + 8542029289363885398186306940986292126220149094859331754364079121977277) * 10 ^ 70 + 7081860276602073556750187470441683622669612058718863729402670636380924) * 10 ^ 70 + 5726784584542053722515473296223618219938018765121753931125410633008991) * 10 ^ 70 + 2468134548532005814521182430136637791357800702538713803160559774500205)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_258 :
Polynomial.coeff recurrence5Scalar1Left 258 = ((((7084 * 10 ^ 70 + 6188370185012701396148531168401292650817744736978951796713988223042968) * 10 ^ 70 + 7535356041077916668414318003963081399015524867650120861832661875043111) * 10 ^ 70 + 5103751807468132633469581053612786142735446798448350220239928682239096) * 10 ^ 70 + 6984204369749850053767013562640601804184145430232956451120598130642886) * 10 ^ 70 + 2340995480576240795968263114880289957395936421936866413369623284561771
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_259 :
Polynomial.coeff recurrence5Scalar1Left 259 = -(((((4691 * 10 ^ 70 + 7946675560556133913315810553817640843585360085186871558638320283054149) * 10 ^ 70 + 8428831297922783820181055889272920222348018109484802773992445394761794) * 10 ^ 70 + 7843455040075677308928791115865744516851958468878302963589371258279541) * 10 ^ 70 + 9297581229593525739096648745217323414305089702659193730702288683897813) * 10 ^ 70 + 7587274618139760088876463999976368037455512848109707319345461317580480)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_260 :
Polynomial.coeff recurrence5Scalar1Left 260 = ((((2935 * 10 ^ 70 + 9921999647933826354907794566972794715284158537833252416931475067972845) * 10 ^ 70 + 290918926792004491636705524065330159001245467976353651711547728324001) * 10 ^ 70 + 8505890039371399513660238685053282561975411092743867561739979738211137) * 10 ^ 70 + 7507509966658124844008481141278518018927430371734783764483303310430834) * 10 ^ 70 + 2349421350647132161083395616275587748105447904267197621791711105297796
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_261 :
Polynomial.coeff recurrence5Scalar1Left 261 = -(((((1731 * 10 ^ 70 + 6139123067061722030390744126195623523883104498077397486243581304002602) * 10 ^ 70 + 2743650957984466400463326637900892309177291212909085215292081717147920) * 10 ^ 70 + 7360177543779976329209421457080514370793000336904482451102060298338477) * 10 ^ 70 + 1742506517214926885755464425156366148956671738131239068656211835724497) * 10 ^ 70 + 1393586025949413346985081753480253913684119568039986174751225049282968)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_262 :
Polynomial.coeff recurrence5Scalar1Left 262 = ((((955 * 10 ^ 70 + 9053663913148230981393733580602988174287446584190825392373407180050061) * 10 ^ 70 + 2610661271362326772731655130384220280062992470772026964471317008739576) * 10 ^ 70 + 1024814407330634522438484307253706755010667421120107660604568913252966) * 10 ^ 70 + 5432413319286638193347944694152564787061093173962555561536362922314966) * 10 ^ 70 + 61832503585355181616467356673495807047762477806479167535602409557841
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_263 :
Polynomial.coeff recurrence5Scalar1Left 263 = -(((((487 * 10 ^ 70 + 729071828464204082241926474753183211669142212661439695192518515118651) * 10 ^ 70 + 1005169186198258623739066075458586301183191168066520033295565187285323) * 10 ^ 70 + 7269237155386840544950931723612776359680150766872538556540050379679419) * 10 ^ 70 + 2378632726041672459064896238462553922003013801195533712009572506718089) * 10 ^ 70 + 3102015680878733441293322721551598759899676973905420694824113488393482)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_264 :
Polynomial.coeff recurrence5Scalar1Left 264 = ((((222 * 10 ^ 70 + 7198310267056315121817761529844135418841399594479567675334598018162377) * 10 ^ 70 + 5316195395873105990254811109032183847896837699694944191598327832333926) * 10 ^ 70 + 2573828882975438745861240394372569628619368440327280894380245035652302) * 10 ^ 70 + 1757993583598083776046277847779872700031399403820071219289086441283013) * 10 ^ 70 + 6930086474790120095338220604955853361401683853922915013261015154660265
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_265 :
Polynomial.coeff recurrence5Scalar1Left 265 = -(((((85 * 10 ^ 70 + 5314375762144226069536060165964713550523288954255942399436560607961335) * 10 ^ 70 + 3854643135081202824841720829112320211912587898608430662675081075646646) * 10 ^ 70 + 6483583188665970705280448591226033267722040724017100051487461897006212) * 10 ^ 70 + 3217666600113879348714934117458423910731955036416964246248881453500472) * 10 ^ 70 + 7398084833962946599227699712587045671108256619321894609911801144372899)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_266 :
Polynomial.coeff recurrence5Scalar1Left 266 = ((((21 * 10 ^ 70 + 8724683466756015864577812331380156220794982442429175178532171979209909) * 10 ^ 70 + 7474124381055743886353189932541966876677186154010581265169088156900268) * 10 ^ 70 + 5784511502367336971465201660038517919083478437779129576357583404766770) * 10 ^ 70 + 7397225834218392647805171220331310022539527768968240511337069091920086) * 10 ^ 70 + 8941531185764439375587299835673088739633982393190083905322506737056443
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_267 :
Polynomial.coeff recurrence5Scalar1Left 267 = ((((2 * 10 ^ 70 + 7310914424668234902244140160964724289641387246921365976809927060998837) * 10 ^ 70 + 3210170628904984699643775292993160978879165357385548966860729211483902) * 10 ^ 70 + 1257558661790103879230924124161840183444354989284527274654021619604332) * 10 ^ 70 + 5936491545068689804539068804261499942076427535502035016047629866044424) * 10 ^ 70 + 7160685193435847897231667486088959138279743484789808799926296611625757
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_268 :
Polynomial.coeff recurrence5Scalar1Left 268 = -(((((8 * 10 ^ 70 + 7974828636579045216145074530004722734605792265489895783188678789245703) * 10 ^ 70 + 9951694088928782639729551941824086705325757178786965749462181332965357) * 10 ^ 70 + 4369410878785492528180461834668693523237075357552547505680915591808641) * 10 ^ 70 + 2155890415050240652435924279859625913847958052935635258644298795177690) * 10 ^ 70 + 154121822950413024452198352677707736572965271072565666439457629693414)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_269 :
Polynomial.coeff recurrence5Scalar1Left 269 = ((((7 * 10 ^ 70 + 5261024573964025042972770290856282768730986682786564381513385462687094) * 10 ^ 70 + 2647180685609299521999099382224295189488819066738609920176164967727120) * 10 ^ 70 + 4771938700034602398374833058476731144147860604953223432224922709748464) * 10 ^ 70 + 6488721412152468904678398435807364801593670056001311521856179885583151) * 10 ^ 70 + 5040081015519024335359687457593031125742354931836847050111144278063233
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_270 :
Polynomial.coeff recurrence5Scalar1Left 270 = -(((((4 * 10 ^ 70 + 3858563091147192607796362771466193174020445981663837694907351383983684) * 10 ^ 70 + 883546078756158373216742342925904527560157160700956119706215865144859) * 10 ^ 70 + 723298789797687939784967654774332927607990692748622264296506854817618) * 10 ^ 70 + 1073123337496371834943415453956173893017487415318741552534097449052963) * 10 ^ 70 + 6837392841683221484683294855993302287375511059701631398230662657813682)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_271 :
Polynomial.coeff recurrence5Scalar1Left 271 = ((((1 * 10 ^ 70 + 6205751627093899744478567015483179503845411965583827263286240736980826) * 10 ^ 70 + 1652940280019225414422452986897289294875852446486024949601670867189717) * 10 ^ 70 + 139945716118201959079656242582023269941595725755229229306385559535138) * 10 ^ 70 + 4067805647152502065916182695453795548191822112347500102297248996896347) * 10 ^ 70 + 8511200809213238581893222830356437523193323404462625727535158496212819
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_272 :
Polynomial.coeff recurrence5Scalar1Left 272 = (((1526836643284585809557228753570277671741678152864842873751849562175391 * 10 ^ 70 + 9220980791937692791891296994719779409676343933402692646897380588865298) * 10 ^ 70 + 178524733542236263446983738333758490994072871782789358259785536247670) * 10 ^ 70 + 8580513283913930480648502605921085684263261034975097334150635666743901) * 10 ^ 70 + 337130831278211479678344922709511195720899375418957519989885064410815
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_273 :
Polynomial.coeff recurrence5Scalar1Left 273 = -(((((1 * 10 ^ 70 + 133829170202144544085403197988359120655700001102871093494252589945432) * 10 ^ 70 + 1541642243455289574833007798480186754750344032853014112752521553402318) * 10 ^ 70 + 58927278987946739022507802686802092354856614261560453812077151087244) * 10 ^ 70 + 4020117057057984301090193676052760342142387149299984440057830901755550) * 10 ^ 70 + 4447776052517211095576515260831781552011909929676717107546446102595923)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_274 :
Polynomial.coeff recurrence5Scalar1Left 274 = ((((1 * 10 ^ 70 + 2515033032022918397879202503603238768590350893114002717736997688779486) * 10 ^ 70 + 9891430460343499692248643412079037260409617013733815620525514862079605) * 10 ^ 70 + 3615329029779202988188423149666236068511433887645223960806867651682431) * 10 ^ 70 + 4285259016860056625844960988073250119079214382772403591814622497627687) * 10 ^ 70 + 3557649100777277941860565756354067530184311012063093502314737464403028
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_275 :
Polynomial.coeff recurrence5Scalar1Left 275 = -(((((1 * 10 ^ 70 + 1497379270541129057963685785125597852375144312894918625518069181375440) * 10 ^ 70 + 2102575696433124796559871162921113117099663129585820068410371272480175) * 10 ^ 70 + 6814039304743861169111729615530344687946048306643443489612097929559681) * 10 ^ 70 + 2635225246815574809712538772130285550137133502405873827475906304497919) * 10 ^ 70 + 9694750575971424870417583898938316472385136900730417077761597544744701)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_276 :
Polynomial.coeff recurrence5Scalar1Left 276 = (((9110867619404027788079986706247611619243080901768894549914865755120664 * 10 ^ 70 + 5193982771090358457757643244594061407974163549947131692642277687107850) * 10 ^ 70 + 2890354073035759865753314086275238300882536483955505827806187949322490) * 10 ^ 70 + 430400933159987580546125271436743989104917217091719913340074905144644) * 10 ^ 70 + 5313321771845086535754881514940902522646428861606121006771059994874275
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_277 :
Polynomial.coeff recurrence5Scalar1Left 277 = -((((6547031682670759945959551198889679541806770957855636089999950322872950 * 10 ^ 70 + 1521875448410640721226569485008065221348732146186877525655739893607614) * 10 ^ 70 + 9045948831047155870003855469740571350098383415162422794100315506837519) * 10 ^ 70 + 3187061212470660171463963771849065485007415788098028931278700972328808) * 10 ^ 70 + 4357036557855202250700221614485843155053174795773963207669095339215602)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_278 :
Polynomial.coeff recurrence5Scalar1Left 278 = (((4365222078605022058749043402618498314486232108031235595003678761903658 * 10 ^ 70 + 7189265369639117834041242120846368402775301946543130112461353099560362) * 10 ^ 70 + 7672320361582236904452832192088967084756935311532674856406643241916720) * 10 ^ 70 + 1025144279021467644228712937536412054977073325994396545356637949932925) * 10 ^ 70 + 9364737154354479215077886843987651885606089080886283833121671712690100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_279 :
Polynomial.coeff recurrence5Scalar1Left 279 = -((((2733086857543662702172581324565991126566694867422391187662499047611097 * 10 ^ 70 + 9731579889797245113482476891801280357918033502822644000573824695665175) * 10 ^ 70 + 3860181562731561069518335115156230426535563042423317499112292898780230) * 10 ^ 70 + 3314924366024766347065738222283785842927648220792569202713351907699232) * 10 ^ 70 + 5660419198673521439965165488035918036975467728104997654697588342382611)