Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence4LookupScalar2FirstPart2.Coefficients355To382

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_355 :

Polynomial.coeff recurrence4Scalar2First 355 = (((16615 * 10 ^ 70 + 9448881222827856839309751813730840024388396955754883969870810952658299) * 10 ^ 70 + 7232027915419667344815925888953483873167063817098748214662727490786380) * 10 ^ 70 + 1951522647152266231644290371175899774657494107856646917626481723997985) * 10 ^ 70 + 5496682315436745703000622533078956988708783786037130925845234318384625

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

Polynomial.coeff recurrence4Scalar2First 356 = -((((7907 * 10 ^ 70 + 7666635271160424572186450278174248444964403291257375369400253859751503) * 10 ^ 70 + 2129063077689193850731862204254315873182096047082966066498665544367081) * 10 ^ 70 + 9648349382289714247118238883958759130206828780562086300190066299037941) * 10 ^ 70 + 7563723118944998273142883951011041353752364470207021607410832622503824)

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

Polynomial.coeff recurrence4Scalar2First 357 = (((3580 * 10 ^ 70 + 5129935116848842143584191247814256944789645984884771144148191213237844) * 10 ^ 70 + 9049827350256511750369714953636750648092334001125166874737595935665823) * 10 ^ 70 + 938181794421500869288648710718714362210840588542740951120548547899877) * 10 ^ 70 + 4562885420655531681997138179700200647961536050189555576749408385921709

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

Polynomial.coeff recurrence4Scalar2First 358 = -((((1558 * 10 ^ 70 + 2643507630308334802489653233998508362431422760718947829929828858118771) * 10 ^ 70 + 663590557783177286084015897755363917582358595139830041163968764945946) * 10 ^ 70 + 4353907664739787513702003039571740369811789710590155859020417079002255) * 10 ^ 70 + 7834238367444264414757052736730378334894327992024857591655019629804808)

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

Polynomial.coeff recurrence4Scalar2First 359 = (((655 * 10 ^ 70 + 426735417591091115490380661994423318200891108923866884387519109628487) * 10 ^ 70 + 9279436394164877912391749689633108498208155438727268566458944915412492) * 10 ^ 70 + 5329429299024993548697767063928205821919755236498949948851595012626053) * 10 ^ 70 + 7652921457965690724604296597843740884853032770523592541821395265870164

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

Polynomial.coeff recurrence4Scalar2First 360 = -((((266 * 10 ^ 70 + 4035468829613767150650755057360214216784009928203877220910993369265133) * 10 ^ 70 + 8063511331056203745060982736487902247654163534884221360642713965364136) * 10 ^ 70 + 1909704975991294799346476544575894230460515157351336736776430964798852) * 10 ^ 70 + 7828713651726611938757962475165638327265548971344296691010498962059944)

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

Polynomial.coeff recurrence4Scalar2First 361 = (((104 * 10 ^ 70 + 7367886806253447649542393508517861692629943450194045165491959039664485) * 10 ^ 70 + 9336042604052816412425671437076792625097778487556568802065997961392462) * 10 ^ 70 + 8269917275028641666284563541160760106575075688870675835334032307473957) * 10 ^ 70 + 7798706978193503212346185009749905934805342573446515945076961400460213

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

Polynomial.coeff recurrence4Scalar2First 362 = -((((39 * 10 ^ 70 + 6814814764698048713091032937688965243619954326314654224076678531362333) * 10 ^ 70 + 5881614081805996130934260989374656251128864554744835987702854023612022) * 10 ^ 70 + 5858403261069192414969762795689906819470608276496170545602862133013788) * 10 ^ 70 + 1881911142984351554415514285600031694310949254334325015995499025039859)

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

Polynomial.coeff recurrence4Scalar2First 363 = (((14 * 10 ^ 70 + 4017014516693052025750350416388251565360563287543506821309215334408529) * 10 ^ 70 + 2666235075192456178208583463025659768501687137108540272912759227477608) * 10 ^ 70 + 1552862748760004337699114648690838987461676077023985197462912727033719) * 10 ^ 70 + 6813227640365097686293357489379422990226174980650897857588775053258297

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

Polynomial.coeff recurrence4Scalar2First 364 = -((((4 * 10 ^ 70 + 9552796448004741978162894467890920256184511994165161142100983062382187) * 10 ^ 70 + 2486850975366320735147968160202608443682656731017130772513253139261609) * 10 ^ 70 + 5302417958306139799245688427936766204182406656596217146171931132247088) * 10 ^ 70 + 5337812150347290443474698270541979480931826952789042597567938258945679)

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

Polynomial.coeff recurrence4Scalar2First 365 = (((1 * 10 ^ 70 + 5862447138927228530002325100220948301014361762957916611946391485374073) * 10 ^ 70 + 1727333697300392438169553971580211370272816238487924708207530342234707) * 10 ^ 70 + 131418007106570143878011626690757622362068749286993294286532883290131) * 10 ^ 70 + 2084965041767019186442628336422060987860656532309385367049059076529286

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

Polynomial.coeff recurrence4Scalar2First 366 = -(((4543594034307845937095921993300058545761946488455553719582327157756807 * 10 ^ 70 + 5281883967293960440357876459861342540411580160988983434918846913381049) * 10 ^ 70 + 2653347653272239938482637588696975538057714276783060012218142660389304) * 10 ^ 70 + 4610973859144085550911644924999513635483756290008494675620477087787738)

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

Polynomial.coeff recurrence4Scalar2First 367 = ((1048753576605666811572679606039613877865937082837999037399037068666268 * 10 ^ 70 + 7056777777190415019194323383661167624192403785696681885062132849515306) * 10 ^ 70 + 4030132566901394076747126730310260620863698549628727480887596111444959) * 10 ^ 70 + 6352747566316993537076990760232120095903740505691048290307528061746383

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

Polynomial.coeff recurrence4Scalar2First 368 = -(((110576430145268469167238609588123085791880914774983608806680290780702 * 10 ^ 70 + 5862186087906973304090547496627816065010434091035224674413454078408301) * 10 ^ 70 + 887056260896600491821878274726641288504989484367441520475506214296359) * 10 ^ 70 + 8546395572947631890933045342076739543582496305535252821320701442919997)

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

Polynomial.coeff recurrence4Scalar2First 369 = -(((72536958049755527513870068928810325647460804335966727226409496414349 * 10 ^ 70 + 1489251068628180926342945208352691891341354729157744611091691668717407) * 10 ^ 70 + 8289011163590703266577049843221511581388083349312797568161394729047917) * 10 ^ 70 + 7866048431401819988557950373390570865717639506066020581609783003828015)

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

Polynomial.coeff recurrence4Scalar2First 370 = ((70221309328128595609945611946148285258419577925412837169273643913677 * 10 ^ 70 + 9343650151894878554796196617996156730435846301944291110127173719226378) * 10 ^ 70 + 3589344031256572588640748251880684630220469598571192053774066742842884) * 10 ^ 70 + 9012652181328595328992767830888336266625868821455886005055206439521926

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

Polynomial.coeff recurrence4Scalar2First 371 = -(((41438190229352366926631260918726071872638749013853075687908074958367 * 10 ^ 70 + 1206610815624837595886440323802626109607670543645373485784306490490106) * 10 ^ 70 + 3780061487984503748254689730729219754923691252426957538672533573151498) * 10 ^ 70 + 3668250587776089848161065790046198087168092006051131085459059514244432)

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

Polynomial.coeff recurrence4Scalar2First 372 = ((20397107379687218397104305656409755538771244207754938697448650932095 * 10 ^ 70 + 1701727970051868215715852230331879853131672539172902468591110858659615) * 10 ^ 70 + 6341007809024521879212593760564939528501335721996331292024422256365937) * 10 ^ 70 + 826522661205807120342761599337339451028061417001982313803911302864130

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

Polynomial.coeff recurrence4Scalar2First 373 = -(((9027332222992998465160093876955259602225643641862949082844367258797 * 10 ^ 70 + 7692924079007134507896574537717031183360772989533884678853185029940331) * 10 ^ 70 + 6440462702371041706862323161716909300847858379168488244214283526501383) * 10 ^ 70 + 8105059874237378995136386339569891097603489049746251211562823294988527)

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

Polynomial.coeff recurrence4Scalar2First 374 = ((3695489088456919715512143261316964143871181162782846229185121482508 * 10 ^ 70 + 3726194472380145919269158580654707156917226257009298785295167209512434) * 10 ^ 70 + 2736616699779278422820351259428314296770127772591388805558871607395136) * 10 ^ 70 + 964809481809466266942197930691550656555530170150255592158577671511046

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

Polynomial.coeff recurrence4Scalar2First 375 = -(((1415834616073323971822809241828577837010846656429121570741854825759 * 10 ^ 70 + 9282824404851455133647644282107557392751645862838260721376753415047962) * 10 ^ 70 + 7709205719103042492603941141979155798983415905874875846427939340597316) * 10 ^ 70 + 3507363613998556326538972838785558132330570203223207984588321330710538)

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

Polynomial.coeff recurrence4Scalar2First 376 = ((509288026247192895669255812565014487570221869363206697470520514175 * 10 ^ 70 + 4650998378572053670233488441999580074915389219779155115079468729408238) * 10 ^ 70 + 4615043851362014193054512970510673113782922681935619253794875781550158) * 10 ^ 70 + 5762477399062820518408719010616556839560997427268357489445548921933250

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

Polynomial.coeff recurrence4Scalar2First 377 = -(((171378877498012194157776756332609228293867200974106577845754237835 * 10 ^ 70 + 2108988931230888692015997863366940613756320784196279474870358645601782) * 10 ^ 70 + 1004117586887244302902969685709079667479461686649511631518238555584430) * 10 ^ 70 + 7373633874255848702831931431866839544555294374428833395425384194843824)

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

Polynomial.coeff recurrence4Scalar2First 378 = ((53290090409385014208321018903153222650351136490927876319512716014 * 10 ^ 70 + 3287355530017630387648150178816585746688402876985705916214727455165446) * 10 ^ 70 + 5425569421159316740651855423889739088952511168651264586328112090156356) * 10 ^ 70 + 7320857212913575899602903746696164336851991980482315201198572661961556

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

Polynomial.coeff recurrence4Scalar2First 379 = -(((14870396205980421851860769816278447304464053187303313306541894203 * 10 ^ 70 + 3596008178540840443750767622913567072197640035412770902915606548580925) * 10 ^ 70 + 7955861506461603707274003906504928782168702565100016190181818740771335) * 10 ^ 70 + 6735105566731640436932542023207889077124658813961444474595233668982940)

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

Polynomial.coeff recurrence4Scalar2First 380 = ((3446440543244035889545453204214247833255724805605579289550491284 * 10 ^ 70 + 3870398614632200796790339278842853532136424151407780989784889823081085) * 10 ^ 70 + 1003904211913016721424969724914922493713349331002282050771869516409961) * 10 ^ 70 + 194208193266655070584386409599393107766542890727311612580439880781745

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

Polynomial.coeff recurrence4Scalar2First 381 = -(((477851474248902326731234011870993210011912974686808989949611405 * 10 ^ 70 + 5434490845635971049214510582246645018964021901460550708106098973328751) * 10 ^ 70 + 1105593086746032810567004335537995238694918929427590478792686337745211) * 10 ^ 70 + 4651554345104340048124463691483419051596661573118551762153440040800393)

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

Polynomial.coeff recurrence4Scalar2First 382 = -(((109406951691816989711944340828812595762410916924578479489526936 * 10 ^ 70 + 6837352861861235315738048264644408912574205975930094001830910647727511) * 10 ^ 70 + 6571577334390745695157565706591702063216129502341794193962133311462537) * 10 ^ 70 + 3775380507971414771956526112040138707666575729332716552304419516047139)