Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence4LookupScalar0ExceptionalPart2.Coefficients360To382

Recurrence 4 lookup certificate: Scalar0Exceptional 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.recurrence4Scalar0Exceptional_coeff_360 :

Polynomial.coeff recurrence4Scalar0Exceptional 360 = (((421305 * 10 ^ 70 + 4408520093390920301126807926666965659029262380138563213461782936999367) * 10 ^ 70 + 8082871895779773634515128864794289307333653827296501725668472374433036) * 10 ^ 70 + 8762206052473161891593088460541804044195263181621722808832867577800670) * 10 ^ 70 + 243454873638903351509758770082087287014204171278194210989001573289339

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

Polynomial.coeff recurrence4Scalar0Exceptional 361 = -((((142311 * 10 ^ 70 + 7177682740904539433627671669031838953911423877466876405167946060529939) * 10 ^ 70 + 3169740920171351951483586473474263415889387567655297025462717952200469) * 10 ^ 70 + 4119207191410306068659894949356753674111647083048549281151240365608703) * 10 ^ 70 + 8720334609839838213945240861140092790199021136909331375457613981570074)

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

Polynomial.coeff recurrence4Scalar0Exceptional 362 = (((44855 * 10 ^ 70 + 5992296316580714798685637260966096094683086225526717395906719982383756) * 10 ^ 70 + 967213043264909595148135389532160468380929029846535021087974334626737) * 10 ^ 70 + 986666633799138034425953323503338394960589966468505086870186579631231) * 10 ^ 70 + 5486249256938385934255720599622599215024248649375221472358803421902522

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

Polynomial.coeff recurrence4Scalar0Exceptional 363 = -((((12582 * 10 ^ 70 + 910420897491518603501410670093393946510521406111397255770257454560019) * 10 ^ 70 + 3233666695390322529968688052229568967280341887457507555580749170746974) * 10 ^ 70 + 4019669657481356535953729781586616571981189052562111979484570685340514) * 10 ^ 70 + 4110898226014406612526979266589243525041672215042225181729193738657512)

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

Polynomial.coeff recurrence4Scalar0Exceptional 364 = (((2719 * 10 ^ 70 + 5463817420524711315363130980348911129951799423331760800178663458021083) * 10 ^ 70 + 7151899880448585094442919394882044853808708849957474775694594364604973) * 10 ^ 70 + 4151137357323468951532174895860319702112640810476217035695474894051429) * 10 ^ 70 + 4378786235015172984979994913741243524547231309549852063645384749023602

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

Polynomial.coeff recurrence4Scalar0Exceptional 365 = -((((112 * 10 ^ 70 + 7613767190100324308764258250798174349890705598384149564198776779828790) * 10 ^ 70 + 8552612547810043847152629182923781966474218832775550715518338215588898) * 10 ^ 70 + 9953274377686970699198997830555882323772651828782871449369329010551079) * 10 ^ 70 + 2206911612886009564584868307546753807835413377287709891051872220676855)

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

Polynomial.coeff recurrence4Scalar0Exceptional 366 = -((((357 * 10 ^ 70 + 6238578242218612101273983803021494552710510688613864332172115053338478) * 10 ^ 70 + 9945503626855611327383373728478595550639657098088257355028139324668311) * 10 ^ 70 + 8619128081150976317659917949520592641364048183940315511883996729452012) * 10 ^ 70 + 4930026026670792512065085363953946084119309904432152653116782846034574)

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

Polynomial.coeff recurrence4Scalar0Exceptional 367 = (((306 * 10 ^ 70 + 3319750820162289107594211805037093867647973485262368420084269837254755) * 10 ^ 70 + 4010941537746092103470998211408407952733317757854056306315499550879606) * 10 ^ 70 + 4529443456311182009521423982556109061156636864443427868573780660246103) * 10 ^ 70 + 3057567576965598657594000710896261001121335501218868952539633687248808

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

Polynomial.coeff recurrence4Scalar0Exceptional 368 = -((((187 * 10 ^ 70 + 5289940369560003341569762533257175437115997052017710411485077919472215) * 10 ^ 70 + 7840754781615232445064315345738421240334320125844064368310228850708402) * 10 ^ 70 + 6715501305233387131670002907563384402978633039403751851075280216602603) * 10 ^ 70 + 29676339871571286791588747623182435197243250209899594077782033570904)

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

Polynomial.coeff recurrence4Scalar0Exceptional 369 = (((100 * 10 ^ 70 + 3731805501221164332423419159676835311879063148698254610791664245022766) * 10 ^ 70 + 1174476547095371047604871642441134826686589284103888768910828322566099) * 10 ^ 70 + 412169257721044843838204799603280901210173934941273956832006051962541) * 10 ^ 70 + 2522314618943546984359147108865800451230835744920901492626429502475348

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

Polynomial.coeff recurrence4Scalar0Exceptional 370 = -((((49 * 10 ^ 70 + 8150521521819266412150889196966656012110467312279326954153207358626958) * 10 ^ 70 + 6708998687680356244542712896327029113970080931307163877448232983076841) * 10 ^ 70 + 9398292535687770210113498119753794421492776920206974946268667990718580) * 10 ^ 70 + 7645894501444807693935310444393024512210550621075730240704221213232894)

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

Polynomial.coeff recurrence4Scalar0Exceptional 371 = (((23 * 10 ^ 70 + 5018159344600153985450566403333206646947876462658448366284937339596858) * 10 ^ 70 + 7232118061037689424636518131300481416338905148923601309011707435193164) * 10 ^ 70 + 8324784731084816511176816790855986737474044229611017576398937077628483) * 10 ^ 70 + 2782412184534495859516103831433392805650626017458165431991349531873007

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

Polynomial.coeff recurrence4Scalar0Exceptional 372 = -((((10 * 10 ^ 70 + 6719712289286032192203502272050285325009470802591481140503444362945834) * 10 ^ 70 + 6104594811679963948163815334197374989406830389948266428833959271752962) * 10 ^ 70 + 852597730256502309107891730702917756861151858545180031876817229706662) * 10 ^ 70 + 2369201519362292228444095649124264785172993628103233118423288841893214)

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

Polynomial.coeff recurrence4Scalar0Exceptional 373 = (((4 * 10 ^ 70 + 6958808409728860779753567386487502552310669401938134387071276895325315) * 10 ^ 70 + 3788346107429629753954298828321941355001251917943924249036343850663872) * 10 ^ 70 + 6545604997262338646531439690862464012300011039988884240546682450265246) * 10 ^ 70 + 382943648519725516750219129979935721055595895082517951913185866689227

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

Polynomial.coeff recurrence4Scalar0Exceptional 374 = -((((2 * 10 ^ 70 + 97350106612655916580831683969691179987241479916588811647016875268091) * 10 ^ 70 + 4986932414589038602421873691920994622892302301639307817105206482051383) * 10 ^ 70 + 1989687571503025340712126793882901450069233906861546517050291255013750) * 10 ^ 70 + 1478540210712977773372941129684806266251560306269143286556859320001545)

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

Polynomial.coeff recurrence4Scalar0Exceptional 375 = ((8382448698130158356502059716168094119414742398856798865075946013841489 * 10 ^ 70 + 4629265336360791370046526367633129414688557032380827851937647659271263) * 10 ^ 70 + 5305176649865728581717448627240115097767821937874318456308216216932010) * 10 ^ 70 + 5050152048604338825684897015524486936004190768254595666253384583137724

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

Polynomial.coeff recurrence4Scalar0Exceptional 376 = -(((3410337108986014535993425180716678977244101758245846178546321033712531 * 10 ^ 70 + 7272466813817007069646172310427480526755128934089142900204673710975959) * 10 ^ 70 + 3922913880644704621719256086254508957459316766153868483762865260412167) * 10 ^ 70 + 1167456209803427711072876490941622528882533423682243340668406432208678)

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

Polynomial.coeff recurrence4Scalar0Exceptional 377 = ((1353551639955695095609154452974357933476289830395190402921681649253099 * 10 ^ 70 + 2441954418531851680178959948680179971219422835317022136972208781106368) * 10 ^ 70 + 3325782918321236908264646052394385780136685224363826823883178843593670) * 10 ^ 70 + 5009673972964582384526902896899591131479448604397758542910996219570028

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

Polynomial.coeff recurrence4Scalar0Exceptional 378 = -(((523849021027259782842871004377478228675295244637713213900523237961171 * 10 ^ 70 + 1832418449412368529768585147577421550417333583010366796330968413966865) * 10 ^ 70 + 3276476469115443868824482063266104692750337655573363190329833117716914) * 10 ^ 70 + 9496258028133045714380072330701128095758051356484528871496041822251321)

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

Polynomial.coeff recurrence4Scalar0Exceptional 379 = ((197495176999037531749626441038569683657639608278283208035508564038395 * 10 ^ 70 + 2590694824484230367686674529595187737442186363780904490739613432696425) * 10 ^ 70 + 2876733586590592529152739590252842954672482318128992736240940549231019) * 10 ^ 70 + 9679277584696681366571100456837651537115121382328543503997722832881811

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

Polynomial.coeff recurrence4Scalar0Exceptional 380 = -(((72412698707393043387531922805736628069808820253312283707126484404258 * 10 ^ 70 + 9058266835117659852149171117370302650433805720129483998353254656748477) * 10 ^ 70 + 7989383674093592716042256405279363702011909791273381067513841577635028) * 10 ^ 70 + 1858318309499715169068627160289410067763895290794437856556656289979634)

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

Polynomial.coeff recurrence4Scalar0Exceptional 381 = ((25756000332550194748705836114153813731521101445821289767937864835131 * 10 ^ 70 + 6501279654325240830868962046134380238595031308659715735497846375316683) * 10 ^ 70 + 4071538797497197327262927696012087308825888228145398065750540887641151) * 10 ^ 70 + 4450729124837472951651842368612515652915064578741952967742365552016155

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

Polynomial.coeff recurrence4Scalar0Exceptional 382 = -(((8851326189393614876817776839550490436579582374721687177208945860123 * 10 ^ 70 + 8867239010020598098325474518177062108530554415659386729002433152162862) * 10 ^ 70 + 493562682336161986515704721058784449938927167234845238369524702859512) * 10 ^ 70 + 3833086409748287730982323033240564388278194943202246129292419847537932)