Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence4LookupScalar2FirstPart2.Coefficients329To354

Recurrence 4 lookup certificate: Scalar2First 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.recurrence4Scalar2First_coeff_329 :

Polynomial.coeff recurrence4Scalar2First 329 = (((3955798375900 * 10 ^ 70 + 8626464551702442571772659495537879292328209654484622801453672047483044) * 10 ^ 70 + 7733478192864362536066641347604026303785833990923870137358400518133306) * 10 ^ 70 + 9170014078491229460435869894393585349192708093240899267193273661224479) * 10 ^ 70 + 3222063661971594901413873214168470719161815395239616390155681440343690

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_330 :

Polynomial.coeff recurrence4Scalar2First 330 = (((6819191256019 * 10 ^ 70 + 3415079448887084505802595244983502317446385988656974157803413361304795) * 10 ^ 70 + 4309783831831415725033735742157786489058336734023253463774850604917867) * 10 ^ 70 + 5258163893911022905825622275076459445517849817517116491700744714700381) * 10 ^ 70 + 1674471647558065863404584758094696032067521668983682244268776535585021

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_331 :

Polynomial.coeff recurrence4Scalar2First 331 = -((((7180214045773 * 10 ^ 70 + 6469905255128991079674242599916321030676305219134168549089360095275210) * 10 ^ 70 + 4743440347047991125464253119679711518023300502055287659784558825496173) * 10 ^ 70 + 3403605022625336164722851352081541960097408859117875326365408026387782) * 10 ^ 70 + 3530262621268105836945718666805767555629897581619053677549456549221423)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_332 :

Polynomial.coeff recurrence4Scalar2First 332 = (((5106960905947 * 10 ^ 70 + 8038914781404936882365158931170357922380355563042531740364355743866575) * 10 ^ 70 + 2433555920891902208357409711447724757646087023423628297149415979229536) * 10 ^ 70 + 9992376430519160906826254754537541085973058140400223964961418229698524) * 10 ^ 70 + 972951817424841673288955516067485649339773092797106679775954659279337

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_333 :

Polynomial.coeff recurrence4Scalar2First 333 = -((((3113558776874 * 10 ^ 70 + 9476788402615279745281746153551643769465283437501581428818297296645710) * 10 ^ 70 + 7301952556052617216325596214798990130002103448769186045748798044467698) * 10 ^ 70 + 697406956473641131511202821387277775400979798224084458069862862452352) * 10 ^ 70 + 3633216505804935244054473363588892651368851459376250951547976141394995)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_334 :

Polynomial.coeff recurrence4Scalar2First 334 = (((1737048334340 * 10 ^ 70 + 7901169640405947785689735458357924369075570619659661935776284842301018) * 10 ^ 70 + 3378643697122758347168936357247098598492467272153185619833173367403188) * 10 ^ 70 + 999571595075349724065456491977312718346482459521931804550457196577313) * 10 ^ 70 + 3919539352262519383670174912789028817655231785085696349933526257691519

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_335 :

Polynomial.coeff recurrence4Scalar2First 335 = -((((911400922432 * 10 ^ 70 + 3780746183571920353031222201238690060508677315433440564047913977988390) * 10 ^ 70 + 313893819670309343570977614917247897848113694630565528776807464035959) * 10 ^ 70 + 8966940714706194878070866048598251860738341204591322142760044404224784) * 10 ^ 70 + 1969710227523377225202589671483458715305829873341673881311196456879488)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_336 :

Polynomial.coeff recurrence4Scalar2First 336 = (((456029114087 * 10 ^ 70 + 2561504190004561051757328928247635886935569970243480949582215826433651) * 10 ^ 70 + 4490414157956695278554291420221140258509140239991810093388432781063176) * 10 ^ 70 + 7218129837167478571412872995519064824980952945982667000787877236686813) * 10 ^ 70 + 5310962876017509298298422794638278051108553900987606063644295092394504

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_337 :

Polynomial.coeff recurrence4Scalar2First 337 = -((((219322758856 * 10 ^ 70 + 5821221414081687747880996245136027257112043250242764716126512547328606) * 10 ^ 70 + 7072104768138587200860541119648538972375608194433381236116168877128059) * 10 ^ 70 + 735303928047269230224576737101120124997827439244015706214910667950923) * 10 ^ 70 + 2546230941835347084707100164050246413666351200049287350078591453749934)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_338 :

Polynomial.coeff recurrence4Scalar2First 338 = (((101866625773 * 10 ^ 70 + 5438113144348095773763219920049485757226062244495267348139197871469459) * 10 ^ 70 + 1008888705906506922812297767294803569943411936822431495519381434562319) * 10 ^ 70 + 7406757009082850070037238521666280252818948469696002095051767535256613) * 10 ^ 70 + 8792302282201390775659676957048921774554658053701683253763337152730706

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_339 :

Polynomial.coeff recurrence4Scalar2First 339 = -((((45821836211 * 10 ^ 70 + 2644982841869330820378883809108816671346481029445917707377458615306018) * 10 ^ 70 + 5419125276005828918552014508958118159647290615832325321685623878215483) * 10 ^ 70 + 5578150640482929703924106500986762732272135412018376433559052376949272) * 10 ^ 70 + 8016513052915934019103338647711387625568835636296762149686132194966064)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_340 :

Polynomial.coeff recurrence4Scalar2First 340 = (((19993921057 * 10 ^ 70 + 4620260964140872366280149552802330998786271186151988912608775308459923) * 10 ^ 70 + 3753141587212623124672065619378103387394479237927643386765612169094163) * 10 ^ 70 + 3303889520886840361767571278894895353186764146323696011205682233137401) * 10 ^ 70 + 2808329882121152135099820657552557543116127253472916376147418224057199

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_341 :

Polynomial.coeff recurrence4Scalar2First 341 = -((((8468115905 * 10 ^ 70 + 7143575632558719986117882049960669938008196932431770255520757516925692) * 10 ^ 70 + 1306392140233117356578851366733677213520823431065455225662321494131644) * 10 ^ 70 + 4126205909782931342702041782598110485988181483951836897448657003484951) * 10 ^ 70 + 7891698102487028914309780553673482538453344087255127660815324059823713)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_342 :

Polynomial.coeff recurrence4Scalar2First 342 = (((3480530075 * 10 ^ 70 + 3859034482022337167681380743747342871564819970099370325974588290014554) * 10 ^ 70 + 3356580797375394941867084553074602254979366034791518745931359671931644) * 10 ^ 70 + 1899964889413460142049912701693445663365327340377854296455073913017836) * 10 ^ 70 + 9882382689438478007935301704626236603748334641730589472418540287898631

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_343 :

Polynomial.coeff recurrence4Scalar2First 343 = -((((1386690664 * 10 ^ 70 + 2089697438102877958906683266521609250973611011784850669398063614723509) * 10 ^ 70 + 8963058516249759290194891066175799928261452181828654096358143298381628) * 10 ^ 70 + 9740853110878690278484139861409756168515407559684456235115411244290363) * 10 ^ 70 + 9758227171691197030955119786523100939820656130275960535330795285564629)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_344 :

Polynomial.coeff recurrence4Scalar2First 344 = (((534296033 * 10 ^ 70 + 7972591813341252098680661270004637076747885397981222412755213981807035) * 10 ^ 70 + 4490115552673161266730237370334382155245875785897825896274408213876026) * 10 ^ 70 + 9704065455777915854261720821206352254560957627182075482351577171924369) * 10 ^ 70 + 2560118253732972892385650533760741701671900697455990923786947641159407

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_345 :

Polynomial.coeff recurrence4Scalar2First 345 = -((((198281986 * 10 ^ 70 + 7577515081193100958506774746869124744358485375160859564981876260837425) * 10 ^ 70 + 8139953396868368504051868153806761706688252946216222130851230410286036) * 10 ^ 70 + 5999694099360468817916893497530345144750658251520055695206156871292385) * 10 ^ 70 + 1268847082059231743556045166824125813541481078323169630733076380471475)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_346 :

Polynomial.coeff recurrence4Scalar2First 346 = (((70377501 * 10 ^ 70 + 811609209902136025049173923095335191061067364323341783205228161566089) * 10 ^ 70 + 6759340687949015468292919424138803290813286869482466108957688813782799) * 10 ^ 70 + 7693355041352027810962898329835258660097866768998715339184296796791414) * 10 ^ 70 + 8358046087921685537823756405976098129406442273422653839259054449931276

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_347 :

Polynomial.coeff recurrence4Scalar2First 347 = -((((23591291 * 10 ^ 70 + 7710060965016480058057430798348361427044957119136377055924931799457820) * 10 ^ 70 + 3558918485073431606765470080911472170100166588472109158714661909323326) * 10 ^ 70 + 579882828197262485571053889703201122373269302615349632917481809630638) * 10 ^ 70 + 995143446864770629266494114942240475760803527080076594627359671004354)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_348 :

Polynomial.coeff recurrence4Scalar2First 348 = (((7284371 * 10 ^ 70 + 4290018026451784054241624966788458055101279217533810534219206186797619) * 10 ^ 70 + 3553242437400141723078023533823796956386571895272437518993034075853094) * 10 ^ 70 + 7378885713362743071810259281680897730206553970884387748237708138744737) * 10 ^ 70 + 4081966013311754782069215054382556340437414404493624974792686811074070

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_349 :

Polynomial.coeff recurrence4Scalar2First 349 = -((((1953047 * 10 ^ 70 + 7793996968756188099228658622235032935010779398260229514624830805950977) * 10 ^ 70 + 3022744515809566713368807319542504896334172373717631374207531730710411) * 10 ^ 70 + 3342949913164337042169293535306457754750750310356452521255815418165408) * 10 ^ 70 + 4683489435224660354191094918198853532660395260594458271503865492828631)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_350 :

Polynomial.coeff recurrence4Scalar2First 350 = (((370619 * 10 ^ 70 + 2844453445411448679489619280881323168788650476996066341842127852358494) * 10 ^ 70 + 3335889088722758052290952125707903241096649669071953262356396079361114) * 10 ^ 70 + 1649395593419588304027464809810449649227222949535185038393386820883842) * 10 ^ 70 + 3898014307592677625591322849540024067110003870661091814961506069479236

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_351 :

Polynomial.coeff recurrence4Scalar2First 351 = (((21024 * 10 ^ 70 + 2292409815949978564251680950054596924440430153716012077157681160457039) * 10 ^ 70 + 9312698567853861230503112303733071963639394633415937289955156163817426) * 10 ^ 70 + 2098196739725551506635945307503425891333263839702869175643662619422845) * 10 ^ 70 + 9163214653608786614465581291704115572092320428678773836347419063734786

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_352 :

Polynomial.coeff recurrence4Scalar2First 352 = -((((76024 * 10 ^ 70 + 8404827832322985609679003890882473491510392317779005163718962277114506) * 10 ^ 70 + 9602993644889875992649948995615050545481897387581121165550806318563419) * 10 ^ 70 + 8973201508876006075236594419857753307800653265795352299571374201445381) * 10 ^ 70 + 7704769766865689931672152892370573290269870500019223951513165169624248)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_353 :

Polynomial.coeff recurrence4Scalar2First 353 = (((56638 * 10 ^ 70 + 3101929113768879121876696448194079940857318321546902117275752484846272) * 10 ^ 70 + 8688132940603689683931976058078508267648497647058033633007902743363595) * 10 ^ 70 + 9617064640272223536469790337217639720583563617295917499900140733106942) * 10 ^ 70 + 7046341438434237900426358539216401624032732111868779494492425290746685

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_354 :

Polynomial.coeff recurrence4Scalar2First 354 = -((((32534 * 10 ^ 70 + 6690549050363454682373009795967482359023732992523373125208262534156908) * 10 ^ 70 + 3751944622998474587834215573015499298680923181106323530354871076787852) * 10 ^ 70 + 6047652768658851443628917558344770734128752378379097138864704967513250) * 10 ^ 70 + 8202511575224380496846971155005724244040279335487486372412697045853415)