Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence4LookupScalar0LeftPart3.Coefficients371To393

Recurrence 4 lookup certificate: Scalar0Left 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.recurrence4Scalar0Left_coeff_371 :

Polynomial.coeff recurrence4Scalar0Left 371 = -((((122 * 10 ^ 70 + 118824204385462454323303045314574394284362355770711329188408541932742) * 10 ^ 70 + 3792785004859641550747940278107981165725797731009452517912227500344454) * 10 ^ 70 + 110628549406951012800219409566674438105760898557754549858224222356764) * 10 ^ 70 + 5096463827104715770436943680070390886342860097226038687760915177687382)

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

Polynomial.coeff recurrence4Scalar0Left 372 = (((48 * 10 ^ 70 + 5126123407714167374042720378484902235396005684779152597395742983828752) * 10 ^ 70 + 2067713920547931346971356120665297437459997828724168867895774706792238) * 10 ^ 70 + 9063994915124001273217583340882233135186498740818160641410844089595358) * 10 ^ 70 + 406741003313996576547860698662961939352204717620585575628772164308258

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

Polynomial.coeff recurrence4Scalar0Left 373 = -((((18 * 10 ^ 70 + 6787756963247983858121527122948666265807317369976834096809060911759573) * 10 ^ 70 + 3302573153762494085079208444926294318386874058857184276326706361280836) * 10 ^ 70 + 3241984274280414460837524257520353788534410285909730262131952173335944) * 10 ^ 70 + 4660079791910318930183464688403136329886105307641076491391622483816594)

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

Polynomial.coeff recurrence4Scalar0Left 374 = (((6 * 10 ^ 70 + 9429314539554788326875262111749756932902727702055785604599891554458081) * 10 ^ 70 + 322297789904322061879863394571288994360616274152898775565800717826042) * 10 ^ 70 + 5113252636448823376955757874469074886233367531208718609748940213048217) * 10 ^ 70 + 5279971673322581409447614925714552254355916111775412569825341215697746

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

Polynomial.coeff recurrence4Scalar0Left 375 = -((((2 * 10 ^ 70 + 4815951965071962432928311218383081925525113413390935928806863500203245) * 10 ^ 70 + 7705720345695958864232285404797416080339443591871608568027837265933954) * 10 ^ 70 + 1234903155308952234173532204836830471137726681030477614492286362850481) * 10 ^ 70 + 9904890812861804156324211209761019710441087302137813697955894146540514)

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

Polynomial.coeff recurrence4Scalar0Left 376 = ((8482052563145206837427464394419752886627822726305469917937549033546969 * 10 ^ 70 + 5573237571283508981091159761902947941085902894798771325924852205861180) * 10 ^ 70 + 1491757454694109820746892849367914194504580370931209721119147422214652) * 10 ^ 70 + 6267319468441159644537581422953603822568540435429962453308546530403712

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

Polynomial.coeff recurrence4Scalar0Left 377 = -(((2748843892165293502178818882915317910671010890518427401668382723296379 * 10 ^ 70 + 9909031710922119812824712821927538519509918935966041913295582672631869) * 10 ^ 70 + 295954699462009221494646284581829170373039775370135739769630358664465) * 10 ^ 70 + 6122175157261922736628966209287326213896070133522883441561053651189106)

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

Polynomial.coeff recurrence4Scalar0Left 378 = ((832649828209127436800992679030595372241683021458358714283152207843221 * 10 ^ 70 + 9738187652418044174471047658119893082196040830969099335632727416453902) * 10 ^ 70 + 9007456246913411921772950484672961500931680839668050933443270071921294) * 10 ^ 70 + 5694662582141280078476041987725845530279239152458886831129815991220053

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

Polynomial.coeff recurrence4Scalar0Left 379 = -(((229431302412950839586087537325795471679259301335809454265111855867864 * 10 ^ 70 + 7669522399527606502636298986134148157382998655787968564338733277164806) * 10 ^ 70 + 3775552670899327913315940563242089486096751369480003544219955085797031) * 10 ^ 70 + 5558549586830394938642636409056615864363678876670216426253317889344375)

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

Polynomial.coeff recurrence4Scalar0Left 380 = ((54013140557207636161758865843627521375217118180041748639649300590769 * 10 ^ 70 + 4527286537501885004524365808029150057317758020022697407261685617319826) * 10 ^ 70 + 4690195604728168089285900934461500308248207143783048998661610055549332) * 10 ^ 70 + 4218314289032358115196409483212135021419433422797466059812069423463190

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

Polynomial.coeff recurrence4Scalar0Left 381 = -(((8744374782623523506741775305105730141232137367283210389200102984840 * 10 ^ 70 + 7657920915574227361187807421787907179237381117535234870555159881580620) * 10 ^ 70 + 1425671735414826410312114268068950069423971849157894459446973807742966) * 10 ^ 70 + 9100514397421941353777436041130720926646666028605163205180876565573710)

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

Polynomial.coeff recurrence4Scalar0Left 382 = -(((551160866337916558319939119908384785032317325767727564815979971587 * 10 ^ 70 + 7750032027245259566282262038764606476360646037744599566433450862096530) * 10 ^ 70 + 7642182019431231961224408811518767667268345796392162758796758433616206) * 10 ^ 70 + 4555391736972568047864620145803969455148794058546366042655724216201895)

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

Polynomial.coeff recurrence4Scalar0Left 383 = ((1369283993103281129270831906280663148828498081979292732711694319413 * 10 ^ 70 + 7815408736888767991082700426175398466532619890999437237843338293999518) * 10 ^ 70 + 6647142552660305347807857072373679826492895147266490211834237764818513) * 10 ^ 70 + 5784481786200974567710862053888341905955137827356250704896591001829173

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

Polynomial.coeff recurrence4Scalar0Left 384 = -(((823618415700844231237052874904785952707566421929671288460183611734 * 10 ^ 70 + 105837533148777752222779844038088075152362837033409114852347006053084) * 10 ^ 70 + 186182411352934705229532201013559409407667412706292850535225152107021) * 10 ^ 70 + 1456385360347938259633729233060658254066369521296097049089043257401969)

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

Polynomial.coeff recurrence4Scalar0Left 385 = ((374110078091025236046412498332448165776935016142532591909386820502 * 10 ^ 70 + 9559746349317852142910715500136655749757193991504128671056556126889535) * 10 ^ 70 + 549286966784513523154616151572303541080340434136196102270117660669438) * 10 ^ 70 + 689859671533619563535333868406364403138694178086587824056338502815903

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

Polynomial.coeff recurrence4Scalar0Left 386 = -(((145987096140794536344188885315711947417048313582541945845573036414 * 10 ^ 70 + 7219960987613114524276708948542077650111456813943670497617272903606149) * 10 ^ 70 + 2803798557040134285821803022386343152950928591448899303158961753840892) * 10 ^ 70 + 577995604958588512565000069790393702110391733316805967418575549212810)

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

Polynomial.coeff recurrence4Scalar0Left 387 = ((50577001848206574153614216982292977130292385056011740866509864323 * 10 ^ 70 + 3673851980955268064377424044856021134510156854913066208454633470901659) * 10 ^ 70 + 296948071492189851335395452451480587526874892675385900749513166340216) * 10 ^ 70 + 9537833169267915111258860908204981609046448952289454538071453266290921

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

Polynomial.coeff recurrence4Scalar0Left 388 = -(((15484340094311253466751526834409767424328010384099522298702377073 * 10 ^ 70 + 8965595094835345433379282926309639099201755642737100204118264204560311) * 10 ^ 70 + 4081762601563768662251281315338252327326970481818812010312922007166304) * 10 ^ 70 + 5490631100080979870535111976130747475791971927746507919197938702854243)

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

Polynomial.coeff recurrence4Scalar0Left 389 = ((3985957966118727127405307211553739404703999716738695558841813298 * 10 ^ 70 + 4560467386006304863032531749383867110740226499413164467519862939944835) * 10 ^ 70 + 4424560283283184105591303363473971003241441353999903528202258103264145) * 10 ^ 70 + 3143247237601669002636107208909472896875010020551627228147975018060646

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

Polynomial.coeff recurrence4Scalar0Left 390 = -(((700112474485490022609470676227467384615482754450312960103087157 * 10 ^ 70 + 9760032966042803709383150029641678574879792299821599112500706903136845) * 10 ^ 70 + 8608030466390281378755756892407481055661259414198511519963053763312126) * 10 ^ 70 + 9747687844694601368264058522435875435066619474813921476204432201616952)

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

Polynomial.coeff recurrence4Scalar0Left 391 = -(((48426913984079391502517424743280912230359316356965307352723379 * 10 ^ 70 + 7694896403585542315270400492686749029196061617344003850593695159313377) * 10 ^ 70 + 8960963941772792377946290559985679443284923212154383539260265547895261) * 10 ^ 70 + 5545473436583930940996573681846416384547450927032243386241975203162647)

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

Polynomial.coeff recurrence4Scalar0Left 392 = ((130210966969827654556739938498901857258953404770173348959922631 * 10 ^ 70 + 7851996835753695416821005432108102493872451957356000501404729902528126) * 10 ^ 70 + 9945939354510565103784373881424082723810371381268929934507617008260658) * 10 ^ 70 + 7699292883758940835980160484933569943602314064620460715786837516327774

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

Polynomial.coeff recurrence4Scalar0Left 393 = -(((86326821978015692101790067102978554631104801630888706039957768 * 10 ^ 70 + 8933636042830235197131805030537600866887265286025549186111239058824354) * 10 ^ 70 + 4827087243613697503861542475982406922373163568187429420092200416953708) * 10 ^ 70 + 224527702022491891868135521742673280211432370991804714244977153612672)