Recurrence 5 lookup certificate: Scalar1First coefficient convolution

This is a checked coefficient-lookup shard for the fifth pseudo-division recurrence in the order-seven certificate.

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_282 : Polynomial.coeff recurrence5Scalar1First 282 = -((((47327210445845912078551648481733670912785442818487796237570711905813 * 10 ^ 70 + 9365193524859557185955633493506574250147820132302704928739452734278910) * 10 ^ 70 + 8126497445964545690018509367515318178142266607265759642911204957552595) * 10 ^ 70 + 7765603026915257703578502808698040388826937468546888160003187715820760) * 10 ^ 70 + 7183892159487363306629642629077456040005959821855464856732203654055368)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_283 : Polynomial.coeff recurrence5Scalar1First 283 = -((((2773560940569786322601692631057550293922588407242048579323056721255 * 10 ^ 70 + 7568528424257644704052177556393479009215492383116428251064233002714059) * 10 ^ 70 + 3735335489922136859467730537055481674019741878155779082122078263957313) * 10 ^ 70 + 2805108137727905417306267566088473946171085602350569967234740836125661) * 10 ^ 70 + 9886454777875116892256166479028137401735303402013865930463134610698373)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_284 : Polynomial.coeff recurrence5Scalar1First 284 = (((17316385557218606163396613163872373266362971068775753282134585368840 * 10 ^ 70 + 4844979803938499510729091701088627810597154213835369167456753172672807) * 10 ^ 70 + 9243932807724439563607060527996545421261121951914364335451995451415522) * 10 ^ 70 + 7179979863530201360218906538680814446004037851482093691306737318412212) * 10 ^ 70 + 421485465651457638097868982583734480040466352047834475779744931550502

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_285 : Polynomial.coeff recurrence5Scalar1First 285 = -((((17657808318097295634171397548621630819138583069578295242190668175787 * 10 ^ 70 + 8474997346658218035843847130571362839878634060367775152837472213017220) * 10 ^ 70 + 689203106158459739035670856053727021230033971330917108499945789105149) * 10 ^ 70 + 8935904636211091402380691842247759865771883610294022552489581664954261) * 10 ^ 70 + 7021735401610005611533221028057482970936210134334900244921416690381669)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_286 : Polynomial.coeff recurrence5Scalar1First 286 = (((13625331094129830411683613769513111235571187347920861626232080624351 * 10 ^ 70 + 6100657806534076342680343309691430152401619012815282712703236225494018) * 10 ^ 70 + 4849087165436350970483070918994237191142548889042468579114525337135320) * 10 ^ 70 + 6651684397852626024682136358882808246728116204615565754433220742854425) * 10 ^ 70 + 6755420504768405235154021891381465357587585009899559228126556943826332

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_287 : Polynomial.coeff recurrence5Scalar1First 287 = -((((9225421046875785621022205865128623520762424462867693123055375996619 * 10 ^ 70 + 1481014933404517981347224799800507226610252535245481406476451342073313) * 10 ^ 70 + 561319768227606183773170774314375365304609914075088922442372150589609) * 10 ^ 70 + 449940218962945651308902561527079456988397427390990388222771660217308) * 10 ^ 70 + 5668181058323356116337400830755737699973129372914155557069525014950759)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_288 : Polynomial.coeff recurrence5Scalar1First 288 = (((5752694601979629088674216209731918775064105063576027276590152477903 * 10 ^ 70 + 1748053923153642376658338388480893337847958061107446147570011070917120) * 10 ^ 70 + 3989566637155306322320791442229063810864935213668618576631669618864821) * 10 ^ 70 + 9970937234294091239073288865803842798826790440070743044292348430659541) * 10 ^ 70 + 9013719846249810037751733325900903138618664565427114019614132532131802

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_289 : Polynomial.coeff recurrence5Scalar1First 289 = -((((3375923608488736617019541915048765954687131486076284008216301827440 * 10 ^ 70 + 1105429469212210124101168596668053689121153838113141827809273662027858) * 10 ^ 70 + 6129146818225645093330745463619667938073451758776481899889797368096194) * 10 ^ 70 + 742002748197574825035966511095694844688039836800776343554987503837344) * 10 ^ 70 + 1610827086398956667536129205960848418710573240862115671996776596369628)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_290 : Polynomial.coeff recurrence5Scalar1First 290 = (((1885390806691816614227439914426351897046219087644643302157532841977 * 10 ^ 70 + 3914092610210430412467098003948278808675499976748551230898028989737833) * 10 ^ 70 + 2522787446553874759040492302897086907424534126351220722417405288934453) * 10 ^ 70 + 127158515613820699001073032858114394784710387302848061382770836344662) * 10 ^ 70 + 3223389041331132579553883646815270314395982768079315990978251350586840

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_291 : Polynomial.coeff recurrence5Scalar1First 291 = -((((1008210386247360411946589492566502483002738379533837465764121901008 * 10 ^ 70 + 8087147149243678309603149629497081065050106898880029052831289726568550) * 10 ^ 70 + 2784275124834376229033397623767641980981404999614271702756585882869867) * 10 ^ 70 + 8513149547589718870665136024170537542978885545208439015839043913494560) * 10 ^ 70 + 9164008541258159917031471728846058041979774255537332428521842175495110)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_292 : Polynomial.coeff recurrence5Scalar1First 292 = (((517904150117437402835308280255740953683790298779142073642004025709 * 10 ^ 70 + 9526293157992852949939688236313870258961376563370051621727698934366397) * 10 ^ 70 + 7222923029398482678838164488708149829022701500252223700115565312345250) * 10 ^ 70 + 9741482357629043898559495957860675358873187428984086819649164447078316) * 10 ^ 70 + 9114466144899713841805112396309648223636009547335067854969892840203673

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_293 : Polynomial.coeff recurrence5Scalar1First 293 = -((((255914262982288498612873252913585251899534024403555042245638157733 * 10 ^ 70 + 5441825324523719480612779016534745936002658530828396788901096794918245) * 10 ^ 70 + 2207952542984290344879869367542324803805083593891656724038534963576563) * 10 ^ 70 + 3343389471249383364018658232406726717600592132159193905084106897248432) * 10 ^ 70 + 3318415235599427852703935821482931810944883711656339103997186954780430)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_294 : Polynomial.coeff recurrence5Scalar1First 294 = (((121643594184120117559536517919036024018922546500388853823820266093 * 10 ^ 70 + 3194007397804903105087726819800285618585879390084442588345037296198658) * 10 ^ 70 + 2126958396950286892144700449621065040253008683679400718817920243674064) * 10 ^ 70 + 8072752925736840456371766002986726527298876903374483458662589295759177) * 10 ^ 70 + 307955652762286204006577945554260642990746419941999975050538291576979

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_295 : Polynomial.coeff recurrence5Scalar1First 295 = -((((55557850700579332477029222853893855926318157284547533881434176205 * 10 ^ 70 + 661988953236835354884378381086399818922325003059770915612149127850146) * 10 ^ 70 + 2738258464126068881311019462804486772677219958190672739270958358887249) * 10 ^ 70 + 8198625451611487795512098333594492786127403160212659921891829340858715) * 10 ^ 70 + 9924350172881938052979562196908804089034919816449639349947633513228580)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_296 : Polynomial.coeff recurrence5Scalar1First 296 = (((24329663665663050952741040222240776217608766249873129374296419159 * 10 ^ 70 + 174414786672821170489724158811867421618547636832080324641652430492823) * 10 ^ 70 + 8705914457465713739681300449733245169040685759179733176479610118319332) * 10 ^ 70 + 7843076669436026574780276332587257732375404028315076583768437979234556) * 10 ^ 70 + 8729897220660141878365578780284018713843312224772708011804536797806031

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_297 : Polynomial.coeff recurrence5Scalar1First 297 = -((((10184515191334288848408604035155561733457921138994324518201029637 * 10 ^ 70 + 5087183963599583437414874685208839094300317645744429160223564047645144) * 10 ^ 70 + 394518399437101327324210339464803036427081624211401501889995670648228) * 10 ^ 70 + 5684797150031140831372545389330022510595280626055644861928113212467216) * 10 ^ 70 + 6905305180826072897746774742395527146867693359502962743289808518718770)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_298 : Polynomial.coeff recurrence5Scalar1First 298 = (((4060285394089823063698990116464904648590154750723686555168558509 * 10 ^ 70 + 2572430165536027004029815055248253232396577293770842103572351281580884) * 10 ^ 70 + 7041349932123249048361271928208518086097957606709541634758149723948333) * 10 ^ 70 + 3652577677207183389600469179026681889997044194941908573295196812366328) * 10 ^ 70 + 246440862295772422066836753092212145443845278697141874966890559486788

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_299 : Polynomial.coeff recurrence5Scalar1First 299 = -((((1536294040013735336608247972427037965861523590119877197371030173 * 10 ^ 70 + 30747926700752116087201228741972620704153359616455947143708950450938) * 10 ^ 70 + 5676884517546784809575134693861362024961083962814449382372166270276574) * 10 ^ 70 + 6728031122209412232693508573325523763313644004009546315728936986373379) * 10 ^ 70 + 9236473233992238192061013245517301681726248084101439316064997294102747)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_300 : Polynomial.coeff recurrence5Scalar1First 300 = (((551349517790870357514372255948973997106055157505717316846304885 * 10 ^ 70 + 5187839453090341293364580300032764688202583662290425244450397815734729) * 10 ^ 70 + 607285220655539358851255872317693221237834282945522092386199758908795) * 10 ^ 70 + 8767159120353605803283367457054542129118918733133616679586886085837253) * 10 ^ 70 + 8204190915395675584405169978507595606778383602846762537570759508331636

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_301 : Polynomial.coeff recurrence5Scalar1First 301 = -((((189524432749377838810470646540463588314496048865604202923369270 * 10 ^ 70 + 4207006759798201302018769165388314977737041852422547583230282586352373) * 10 ^ 70 + 5096955576506602673272311676633864182415009917988729551495429273260295) * 10 ^ 70 + 6723642429073865869895502897737924811416437482777566731483011424158849) * 10 ^ 70 + 770748697733111722650764912549210412463000088990121529279186243031558)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_302 : Polynomial.coeff recurrence5Scalar1First 302 = (((64829007181024848765609473500793407430169546034159349770023070 * 10 ^ 70 + 1155925580163055991373286958570109415767405159120689549065446146351941) * 10 ^ 70 + 8766430424022803966977865139857963305863597508762002967005232529827084) * 10 ^ 70 + 2092943034791374271461424401679414052293970070824351239131833126571951) * 10 ^ 70 + 5814266858868663862495603288198004840150518303961043685012063095897951

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_303 : Polynomial.coeff recurrence5Scalar1First 303 = -((((24150719301256381337547215550491197103534158446728263290930088 * 10 ^ 70 + 6936046321124664573509665804980243960586178240692880260405949614335332) * 10 ^ 70 + 581699656826678368724103976400507401012112333109466105382489490567402) * 10 ^ 70 + 3444782239981115343195531499002998133839382247905775556890603103883127) * 10 ^ 70 + 7450691783958914397480079586880924349072864971847077331920101637091751)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_304 : Polynomial.coeff recurrence5Scalar1First 304 = (((10941898409697845289188803047931837966030247803783435187908703 * 10 ^ 70 + 4871967696943177868055623127480779425663908134753549028056217819274004) * 10 ^ 70 + 2252205907930220512926687311199606674907086236413951608096047968803283) * 10 ^ 70 + 6891805918638493820051106646628335926740051147810848012783868192495709) * 10 ^ 70 + 2413478233277406140377343911086059133198198440414522301810375197329821

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_305 : Polynomial.coeff recurrence5Scalar1First 305 = -((((6058052333445661229622517345490001794241211443721592864150051 * 10 ^ 70 + 2430042598603115627635472949602705508814288248081603028979365085720746) * 10 ^ 70 + 7354884401600615172107866505484129432258693345338639815714351492682709) * 10 ^ 70 + 1087380256347217780646050690985332721736200247142090199236525628462770) * 10 ^ 70 + 2915471172015188395647676436106187118806110689215594306012890163096462)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_306 : Polynomial.coeff recurrence5Scalar1First 306 = (((3674394964539552161854665818387417817454640578934011646149567 * 10 ^ 70 + 2059419496170159774170291387257269339554691677337241040657593661962139) * 10 ^ 70 + 1967710866955255074063796519867960312087912172290877982060257757207839) * 10 ^ 70 + 698610325630933622052461403163967019522854143454385025348817799694238) * 10 ^ 70 + 8284192923829888104734322350022073586000430942216589413738409805064600

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_307 : Polynomial.coeff recurrence5Scalar1First 307 = -((((2216016342721492286148499938951880532623286611248570037412814 * 10 ^ 70 + 1916114288137712704748382654836283623203085055375085799181525084123435) * 10 ^ 70 + 8536018913065704519686494634855216281153866926409315680669596291198109) * 10 ^ 70 + 6412707810327060769701347030473525816900982537728520087690442890704463) * 10 ^ 70 + 1865486721394722766500288203362462429772076058083600034220219011998805)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_308 : Polynomial.coeff recurrence5Scalar1First 308 = (((1271246022074694327775412624947320516196419862139879265861559 * 10 ^ 70 + 1023572738138300152399145288074408243349901776690264084949769481693715) * 10 ^ 70 + 6447223596966020310266806993300668941507274672062420206023996598534421) * 10 ^ 70 + 9674390246110358006959049879077700375554318319565414503196685409351116) * 10 ^ 70 + 4858590307589760485046508870066407564553035259811805916718435802791801

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_309 : Polynomial.coeff recurrence5Scalar1First 309 = -((((683577905786614415730456995200797386255294869944214060447787 * 10 ^ 70 + 3029585434328325934561655334012919446244891475104609117837280270593820) * 10 ^ 70 + 1807614194762823129292809875209089419055305753840209642145248270054173) * 10 ^ 70 + 2392220261686917026862246795339742987375033279006602110620337666262082) * 10 ^ 70 + 4774209796418836949852898775910767157195660656893985236860509880231791)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_310 : Polynomial.coeff recurrence5Scalar1First 310 = (((343030583654507366751306336297551662122496273521592225336593 * 10 ^ 70 + 6524709995616175380199676879560235703931508633802544037855480834334227) * 10 ^ 70 + 6865990170550395851016247311547840743346583613739120124172332030986852) * 10 ^ 70 + 6329935968330042600365020340252152590533779912143165804784539231263663) * 10 ^ 70 + 8506958203188450775394194954759288327771122063927446050057058018890189

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_311 : Polynomial.coeff recurrence5Scalar1First 311 = -((((160134264002829378947997325308560260658379059117857128005438 * 10 ^ 70 + 4157426354335773597060305960705832086007316820024189845173886541299994) * 10 ^ 70 + 7695674400068079256220060262996964461102573164864221647079195054882124) * 10 ^ 70 + 9500422066091740882820887182416882704379478811695842533174194905747024) * 10 ^ 70 + 9430326255295711774207551825276717633429905689891007075646793692966703)