Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence5LookupScalar0MainPart1.Coefficients313To337

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_313 :
Polynomial.coeff recurrence5Scalar0Main 313 = -((((4811806701061781899662313539299400681881885333328625632683833 * 10 ^ 70 + 6972815340581109519805237755986281794690750510395810880614932714490717) * 10 ^ 70 + 8046175094241859152355120640413701946629854846262225364007030443102966) * 10 ^ 70 + 4161547904408670526575469940311464249185537048564993483159220873604424) * 10 ^ 70 + 3465709675562800112397715670784898071358498149779789042804407220260492)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_314 :
Polynomial.coeff recurrence5Scalar0Main 314 = (((2153437456443736930285733806939079909860687703395123590730612 * 10 ^ 70 + 1589210559260373848242491045859897610290730270445547683420365536934471) * 10 ^ 70 + 2669620167046337355341892022593267718375672866245144640521066474414900) * 10 ^ 70 + 7533846760143487588825112893450769419321170361604876242019896194523797) * 10 ^ 70 + 3368239405705056554602861129464259438486793997464121076656148267466180
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_315 :
Polynomial.coeff recurrence5Scalar0Main 315 = -((((928582864853115210159674757155774421584676714410465498418913 * 10 ^ 70 + 564332297123049702515893863190817988263213512534207593254950670200259) * 10 ^ 70 + 365515843089006215074625442234593503680473114172058985913365633304518) * 10 ^ 70 + 5707968434807116435612663520619645856878195078039177267399268184180148) * 10 ^ 70 + 6031578091374684383281719027715197139311816865331020260504273517514856)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_316 :
Polynomial.coeff recurrence5Scalar0Main 316 = (((384797867696057151076035612091858133195874323077600596344069 * 10 ^ 70 + 7520025811849449612915273427221242187571822927221723528476018928074623) * 10 ^ 70 + 7742996577489683987521833785058075409741315968218869906114950800747961) * 10 ^ 70 + 3657933534456543227140447448078609325675657454628476253620057219802789) * 10 ^ 70 + 5125310752430377929284212450251075582602433544974640781920194057189144
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_317 :
Polynomial.coeff recurrence5Scalar0Main 317 = -((((152350468213636843511231182331566068113014119419452860836469 * 10 ^ 70 + 5866147524110481322337694781264247553282800371847930821706669146871441) * 10 ^ 70 + 186041698851551862060070166722009830376518497379343684028323716221424) * 10 ^ 70 + 356459173502443091639666122841471300979062418317106679782314587840391) * 10 ^ 70 + 9464022449405855794695211716855954083352498183767287008980784091912185)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_318 :
Polynomial.coeff recurrence5Scalar0Main 318 = (((56977259457970865552892837852708793831729513110524423701342 * 10 ^ 70 + 591812891880041751534105551901418575141366197349252198096738466597667) * 10 ^ 70 + 9281179256045394829088064124615261529230067038311301344225410812948426) * 10 ^ 70 + 5169589834166679997453037305635954416838852906656170727202167111344453) * 10 ^ 70 + 661987448230725271917621519137943847229682031017250280377920435484750
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_319 :
Polynomial.coeff recurrence5Scalar0Main 319 = -((((19668453122037812714546617447269658197878225824797970435907 * 10 ^ 70 + 6639463451897055200077367170062776314421422590751334102321362320241698) * 10 ^ 70 + 8489489239508177349078112039629593346188358912631810148511362403277422) * 10 ^ 70 + 7225579693327186710941977093447290203927363869798756830399198869442347) * 10 ^ 70 + 9603406601997393233598738511520028540540779810210537046090839581151787)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_320 :
Polynomial.coeff recurrence5Scalar0Main 320 = (((5937006318297357578453869663502148560690131498262824720549 * 10 ^ 70 + 2102409177750205524254228291557863697690062136453115268594154179184976) * 10 ^ 70 + 1939600943867172313265032218408967274589053629570381796555523401183286) * 10 ^ 70 + 4254583368726688845257416496670596078288951452284787965738133008794720) * 10 ^ 70 + 1474011050192607889620533184827419141083646313364961929208254713347610
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_321 :
Polynomial.coeff recurrence5Scalar0Main 321 = -((((1311352307905924916786306195773026528063988173936148581660 * 10 ^ 70 + 1063973040237676458313022998459882304095286360546820103655083859749534) * 10 ^ 70 + 1986349481471412925286404997328958094644750580840156691022311935632933) * 10 ^ 70 + 1928878370901690122800158178610615964620198631318251876200566084857359) * 10 ^ 70 + 514489083921046411050883430741192457282901395321866406773759995897574)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_322 :
Polynomial.coeff recurrence5Scalar0Main 322 = -((((21029889313775075506548710040655110081409655825394927163 * 10 ^ 70 + 4994632559242933706296553599240330918273282589915138821967723146416806) * 10 ^ 70 + 2598521321275669169273236162338820510314516860626779122035718023240315) * 10 ^ 70 + 3721890242614846966716032168284236168390937687768527174657322014859347) * 10 ^ 70 + 3988394167656769101294342017269131647947221459500616847714928818727905)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_323 :
Polynomial.coeff recurrence5Scalar0Main 323 = (((274472756461046009456167087321017270610251930504173972227 * 10 ^ 70 + 8858500905629877587990938714516856594377315253559677484761119676741898) * 10 ^ 70 + 3127540028712140204660096017517127573670861076660284284983107994933749) * 10 ^ 70 + 2259957272830779912564270894033055159184722908002646427612625257201457) * 10 ^ 70 + 9036486762030961575313807938725613213047732320617443787700485538827706
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_324 :
Polynomial.coeff recurrence5Scalar0Main 324 = -((((234551065821283221582252412606989007142550958840118790336 * 10 ^ 70 + 4102317118348927073360334656817155709648935384038064789468713575176782) * 10 ^ 70 + 5351348552451042803517780228031834741644126297114260140494319385205922) * 10 ^ 70 + 5088274442305753591831931976317860811648546235280083104744116604890366) * 10 ^ 70 + 9018903627354053817524193665346347827647310909664475845181075960261004)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_325 :
Polynomial.coeff recurrence5Scalar0Main 325 = (((150486888119031806501531117923273634175101360389524805313 * 10 ^ 70 + 4603864967058780765038771352807892629705172317064205488125742759124745) * 10 ^ 70 + 4840710619246802413241629676434771892911328476415372752847818375470838) * 10 ^ 70 + 58327829637136159447356111909913191710093799240637863206326690292820) * 10 ^ 70 + 1345932851859115638072507024584341603994280035823496315873106854306243
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_326 :
Polynomial.coeff recurrence5Scalar0Main 326 = -((((85254880273976771391364856619000029849974890755106648015 * 10 ^ 70 + 6813857503215766928746233816462228835712683750696462424740692917970925) * 10 ^ 70 + 2584091336884760213561015077292356065811569454507666535239299145250273) * 10 ^ 70 + 1921684646316812504965289422818447703725412129455712490416614932414624) * 10 ^ 70 + 9782490600318311931994245649827448421918145741245558275600704946846331)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_327 :
Polynomial.coeff recurrence5Scalar0Main 327 = (((44936867936440134751464998372148490709635246029414722733 * 10 ^ 70 + 9576079497726444180519906757007149721691415855555654939417036289422275) * 10 ^ 70 + 7494537228081768589138836681286785830627864468951983186806157078821834) * 10 ^ 70 + 9950767934206852595318767260507140279905924459718555158831795657097370) * 10 ^ 70 + 9377209450453055215711535123623199434543683492315101118591021360860037
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_328 :
Polynomial.coeff recurrence5Scalar0Main 328 = -((((22569613063797856147225773421635581805311786883281022027 * 10 ^ 70 + 528711301127182834642304581680851083234526439080464880892204836854871) * 10 ^ 70 + 5629923941867694901318216791344407464511141034578970327504375459299451) * 10 ^ 70 + 2886732250996893984047595719151550989626930251807294154754709919476821) * 10 ^ 70 + 1974869449554413024175981122254160733044907192148479863264591519044353)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_329 :
Polynomial.coeff recurrence5Scalar0Main 329 = (((10943788571475073731680528780743448914171404571756963582 * 10 ^ 70 + 8636197805159324378285277611813912760541195040905779955761557496384441) * 10 ^ 70 + 5863715197521464045941490875124766669508297514273286855446947551022641) * 10 ^ 70 + 6566530041691486506370045742999243484143817742290370369251759600046575) * 10 ^ 70 + 5193406727438087940941339188189096152912937766777668644332441412442468
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_330 :
Polynomial.coeff recurrence5Scalar0Main 330 = -((((5164086127416312815720030219587330540424699273514992035 * 10 ^ 70 + 7847947880597813124128966724950397445952803207971562706979001269574324) * 10 ^ 70 + 5276008116843209802910078125531224725073980302307902821076887917923762) * 10 ^ 70 + 3137561972870933797941461257653161375852037889734701883636182904872883) * 10 ^ 70 + 7147877039399639826296882814734883740404356987962968305921946010386666)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_331 :
Polynomial.coeff recurrence5Scalar0Main 331 = (((2383524241346315948989825413288082228440776750219310036 * 10 ^ 70 + 3970645345032149237276283514262174136475867038847422755140242659035284) * 10 ^ 70 + 3089044596942851620184841951765760197726720047738821670550087582818302) * 10 ^ 70 + 115524435097170428606660994814376829743167470582436811713435691578621) * 10 ^ 70 + 438408004176761964812469367666371068779910098052354639046057623357109
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_332 :
Polynomial.coeff recurrence5Scalar0Main 332 = -((((1079622631154934092998016436501371082841432582572070165 * 10 ^ 70 + 3447166818616785541818843548042703305228272769558471576526978942473254) * 10 ^ 70 + 212226446332426989974833585632961154069767436709266671825860532351888) * 10 ^ 70 + 6985752780514303755915388520864917073529283828985409032069176786224792) * 10 ^ 70 + 518310548432879559019665135361109319192553895872841068419592857810724)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_333 :
Polynomial.coeff recurrence5Scalar0Main 333 = (((480859367652750027562602034827376265715357058646265933 * 10 ^ 70 + 9324805478919996786204567842229959747344544567478693602864509610025416) * 10 ^ 70 + 549135054226914975664308565862078344288131547014391532721803701924441) * 10 ^ 70 + 6708530350023714837813235459233375865115575730677222980776218359759639) * 10 ^ 70 + 4488437158641365323110878432130611361497179183027569065240583829324281
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_334 :
Polynomial.coeff recurrence5Scalar0Main 334 = -((((210818300234365191597517970764510321814051112135913949 * 10 ^ 70 + 5953574171155671826028527155924456479581237436193787535469498650939054) * 10 ^ 70 + 9700074516440042984485596734928896121934105863448530450848989154482579) * 10 ^ 70 + 5275196733578758742331268906802575569233085798545503336083459861722426) * 10 ^ 70 + 3959658799455164496935921550662924553761304272664864607393814711515922)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_335 :
Polynomial.coeff recurrence5Scalar0Main 335 = (((91007756232421752604517083401853590969907117714799761 * 10 ^ 70 + 5985946808770234461141716132133051211390954161416594077303595412839158) * 10 ^ 70 + 1733674731586978786192039217899434191275590429267461424551848203743671) * 10 ^ 70 + 4485725760297985707569922517872043870416592078839463824484295175060502) * 10 ^ 70 + 2838060914124764977795267166798129584629116282792211949495346635082050
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_336 :
Polynomial.coeff recurrence5Scalar0Main 336 = -((((38675269872823705631814210172705325432606102827228227 * 10 ^ 70 + 9384410720944267067004934029977939174549733825627195713413650410222966) * 10 ^ 70 + 1102952019984015186079402018547498656825249668918906982630379073030834) * 10 ^ 70 + 2509091022402928297225270677933652225668621658238065134592596997122914) * 10 ^ 70 + 8592296437579538546684744588913866267242713880660224228865781374984761)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_337 :
Polynomial.coeff recurrence5Scalar0Main 337 = (((16170344529088840707035991471588711450694595702331299 * 10 ^ 70 + 3785280277420442086426880735070635677812772771725079558627307369840421) * 10 ^ 70 + 4387988711183503780324773629052692177348249195924275162695212491284915) * 10 ^ 70 + 7715019526665964652101984207327869033386572085966681087516011066053806) * 10 ^ 70 + 6722027435464634422246645457515553005999925168803365945187896781303665