Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence4LookupScalar1ExceptionalPart3.Coefficients485To513

Recurrence 4 lookup certificate: Scalar1Exceptional 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.recurrence4Scalar1Exceptional_coeff_485 :

Polynomial.coeff recurrence4Scalar1Exceptional 485 = (27187968953627444223152573569572420122568063980747766 * 10 ^ 70 + 5905136508453575757490819927496318015208155636388796174017787747161477) * 10 ^ 70 + 5225676051704165008285948876762313457716753854924554771617443502994044

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

Polynomial.coeff recurrence4Scalar1Exceptional 486 = (240755074531439446965310236854693306256644850626543 * 10 ^ 70 + 5608290531719289992432533024835455012706907437626573342317944435588614) * 10 ^ 70 + 6460736695831188149551570819552318599371015379198782848230547954378314

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

Polynomial.coeff recurrence4Scalar1Exceptional 487 = (1541351404048283121527118032443867301144779852343 * 10 ^ 70 + 8166142141385985732267928472384396206089829621700018170417274187387658) * 10 ^ 70 + 2467271307478840118530285207902734518002097769905287245651500313324309

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

Polynomial.coeff recurrence4Scalar1Exceptional 488 = (7052193786184947062440606805634473979258347742 * 10 ^ 70 + 4937028591276762527160408556683390616041131415393051508069417352623368) * 10 ^ 70 + 8821954031192548041518310112434569340001407881700490557577496040477408

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

Polynomial.coeff recurrence4Scalar1Exceptional 489 = (21527082623454426325753588628138865183415668 * 10 ^ 70 + 7628310142049445199890245756986300926794126813917114769721237130907947) * 10 ^ 70 + 812923752057928296591707806027666706101121958565647990259982478381643

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

Polynomial.coeff recurrence4Scalar1Exceptional 490 = (32216482565032211172939792304105410073034 * 10 ^ 70 + 1911619588559341222509442762896801468145970034055150388431410297218767) * 10 ^ 70 + 1958365694451720576576371297877992185384053964269398291758904109457610

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

Polynomial.coeff recurrence4Scalar1Exceptional 491 = -((50494670848919734936943857332063033211 * 10 ^ 70 + 3607165084757063449696303411523925357989688767054543019985655727820316) * 10 ^ 70 + 5828247915353020129584730414162885347276064742066268125536382650443862)

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

Polynomial.coeff recurrence4Scalar1Exceptional 492 = -((413086113675693471732150534407229610 * 10 ^ 70 + 7274155265708701865095359345872731826350294673549693338723255664727918) * 10 ^ 70 + 757450187287597138897000407073667519447686502426017557825885810593168)

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

Polynomial.coeff recurrence4Scalar1Exceptional 493 = -((1004977720854509949826324601814341 * 10 ^ 70 + 9326090735770029768943336668354191613781423880685607317855051342352533) * 10 ^ 70 + 7223504492271179404244209442784677859868904055830350768627935533077595)

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

Polynomial.coeff recurrence4Scalar1Exceptional 494 = -((777005247554678474934625686294 * 10 ^ 70 + 8302091229313092135295700943293423043379381454113005398976042265414048) * 10 ^ 70 + 4883172309658176261921001848450028087267883865326161482288750689620533)

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

Polynomial.coeff recurrence4Scalar1Exceptional 495 = (2077598761867885242197160992 * 10 ^ 70 + 1530073683414790412457504308106874271336443067374594463988139282770027) * 10 ^ 70 + 8744813183370935829032456866242316225992024191242220584228521984619298

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

Polynomial.coeff recurrence4Scalar1Exceptional 496 = (6990527602315234363812674 * 10 ^ 70 + 9495825261890558850168608190476978128786755951929665927231806847444251) * 10 ^ 70 + 6279901520097627933987810221753343164183654107639422242809311220835612

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

Polynomial.coeff recurrence4Scalar1Exceptional 497 = (8236069363469570462612 * 10 ^ 70 + 2496838704996183382493989033229184623313254181489035492834396145079479) * 10 ^ 70 + 498760473909041829273851348344545267350155457397169022476582145368250

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

Polynomial.coeff recurrence4Scalar1Exceptional 498 = (182295829531068640 * 10 ^ 70 + 1226613352072457971330335172722011220287528150662886758716073062417904) * 10 ^ 70 + 4237282099589638849767835489938385707336970986331900650928528856197426

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

Polynomial.coeff recurrence4Scalar1Exceptional 499 = -((13022683892161728 * 10 ^ 70 + 4221127560277218785709340217264950809575763065432801590926684640216559) * 10 ^ 70 + 5810300660910590937049010074168646708336144383815102749213107198283803)

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

Polynomial.coeff recurrence4Scalar1Exceptional 500 = -((20004262161907 * 10 ^ 70 + 2900499548199670581410852817094641975346312818985216875359486484379858) * 10 ^ 70 + 3763330316657124060609451897092832910287277496705520026202364855012637)

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

Polynomial.coeff recurrence4Scalar1Exceptional 501 = -((16361716441 * 10 ^ 70 + 4739234462527237199365301810525359155564791273510731011981589175604820) * 10 ^ 70 + 8197368743682355547778479588435586800825253619785567922346752297622793)

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

Polynomial.coeff recurrence4Scalar1Exceptional 502 = -((8388643 * 10 ^ 70 + 2581234468965957586400792723397635868812389400440769936594706799057583) * 10 ^ 70 + 843863464504985145140145499226460320049879299584920519915439170480554)

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

Polynomial.coeff recurrence4Scalar1Exceptional 503 = -((2799 * 10 ^ 70 + 6079143778576366052722778304249361322256942719530062313826294782017586) * 10 ^ 70 + 4468783802922050229408962859595161289218288401169693787775302570393003)

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

Polynomial.coeff recurrence4Scalar1Exceptional 504 = -(6109193959875492613217762191327105719816050549190561136871640373188092 * 10 ^ 70 + 6106556521441313543609267624560287155663760534341735567316053918198285)

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

Polynomial.coeff recurrence4Scalar1Exceptional 505 = -(863338868337357292475927918374825849054006949194948128604447748018 * 10 ^ 70 + 521070065923223262512031336587193787063404809310199835794619890340794)

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

Polynomial.coeff recurrence4Scalar1Exceptional 506 = -(77602786403100490945174840057444589387398187416328328022261666 * 10 ^ 70 + 7806704759803378703882722836285033022276501742672910874229310664333172)

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

Polynomial.coeff recurrence4Scalar1Exceptional 507 = -(4322518835459384159700204986761387825032459972649549810066 * 10 ^ 70 + 6981359555666194155545769348363771676414813663242397996029795128510784)

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

Polynomial.coeff recurrence4Scalar1Exceptional 508 = -(144503823728056919378650079468546482732575531222641160 * 10 ^ 70 + 4561032415874467445003105222849956155965997080022800352214250810875515)

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

Polynomial.coeff recurrence4Scalar1Exceptional 509 = -(2820709068956917334074195430984676809012815266731 * 10 ^ 70 + 1948456508759938494618995930089800432157543577425249331192981165325925)

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

Polynomial.coeff recurrence4Scalar1Exceptional 510 = -(30800353397030362031170255000043524407004655 * 10 ^ 70 + 2686827164956846414725643805630626682674296491979401404858709298222416)

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

Polynomial.coeff recurrence4Scalar1Exceptional 511 = -(175895633707345746905372989650870272753 * 10 ^ 70 + 8376086258387496535536079165034235073800945558094680878147946099306650)

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

Polynomial.coeff recurrence4Scalar1Exceptional 512 = -(502328471793129300987077794232758 * 10 ^ 70 + 7548221748685469362570094423716559747201199484216595596187644876685931)

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

Polynomial.coeff recurrence4Scalar1Exceptional 513 = -(662685707319367918171916930 * 10 ^ 70 + 119008155598713598057211780087610073542258076228772771250407486983938)