Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence5LookupScalar1FirstPart0.Coefficients191To221

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.

source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_191 :
Polynomial.coeff recurrence5Scalar1First 191 = ((((738816312 * 10 ^ 70 + 1113593829260188473041699494848987669556371348024038821648446501449851) * 10 ^ 70 + 1957525928949198051183941270335472065103528290229217408598568557146955) * 10 ^ 70 + 1467970333792300720518159061543831147998110846403034103738661586632622) * 10 ^ 70 + 3494437431597950429923811899351891934059103274826716466595396993432929) * 10 ^ 70 + 7771530725685850024689794048628834469531447809532206369312360287340552
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_192 :
Polynomial.coeff recurrence5Scalar1First 192 = -(((((987254234 * 10 ^ 70 + 8169284415772988928698696872796492735831151498887044137935155161028020) * 10 ^ 70 + 3744407452596307353247354876458451554042404980947417224974886174395205) * 10 ^ 70 + 688371657859488232646872397432507043340366220531221332600224106801123) * 10 ^ 70 + 5024365962848050423340089318148996495701043995382732638807304580234429) * 10 ^ 70 + 9471566215126976571550495375029384781993776917567569333566827015293652)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_193 :
Polynomial.coeff recurrence5Scalar1First 193 = ((((1295761083 * 10 ^ 70 + 3851208858931904205543838793254927303271184508087703765746900566034495) * 10 ^ 70 + 8897059030666177663877785615222102492055462289938926097543468525204324) * 10 ^ 70 + 6677215854681933456430615114195438115563944502405364205235280932643587) * 10 ^ 70 + 1132168497073770699579513921157716668897868592231845079576622669779566) * 10 ^ 70 + 4256250412544910021662797975319170223591530629576444713347939597909854
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_194 :
Polynomial.coeff recurrence5Scalar1First 194 = -(((((1670268350 * 10 ^ 70 + 9457385006229256882400361342158932051907256385367529007732605777801621) * 10 ^ 70 + 9324064525037639174549691092154604116881961814006141516430133366106720) * 10 ^ 70 + 9128608686390570124319880642402557030311118243345069912476644238319457) * 10 ^ 70 + 6068386907285914072521128460083446380546788036460530468217151254721722) * 10 ^ 70 + 1375362735602915315098370973878125550227367805849796081063230953374488)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_195 :
Polynomial.coeff recurrence5Scalar1First 195 = ((((2114308552 * 10 ^ 70 + 6465418401520903317444677386378639278626675188049537616277181225250101) * 10 ^ 70 + 1846974091374205591605686564447082654692709570986702609591124696765392) * 10 ^ 70 + 7319784660726744195574188812372722642731875625462360262382413291163679) * 10 ^ 70 + 5919000793849875159055371388348034467251786669643325362674996956526173) * 10 ^ 70 + 6265695133834382262117793093979470719734433614202090268259796532560520
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_196 :
Polynomial.coeff recurrence5Scalar1First 196 = -(((((2627961735 * 10 ^ 70 + 3399372156077828654803298915859156766296786675947594397514351610773930) * 10 ^ 70 + 8011095984407595599501988700746068309574879691224336323027699938926482) * 10 ^ 70 + 4182774510480166431414517214932145842416501804567059406518667383744434) * 10 ^ 70 + 900576893066910343399228550227063929017277621567418186380458157247312) * 10 ^ 70 + 8903005273972384417306892709799161356559661276130853420738835950636535)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_197 :
Polynomial.coeff recurrence5Scalar1First 197 = ((((3206838578 * 10 ^ 70 + 173364728232425111673462697886272003598135096562465431218037325159270) * 10 ^ 70 + 1534574551747601512649713287452645846150434109497158180809771106982861) * 10 ^ 70 + 261119948236186346348518656831313182121532698177400900428329649653627) * 10 ^ 70 + 1070990821501638260450395651659337794626831808837989660150418855732890) * 10 ^ 70 + 5666824145284953697058242649986018677638119028935232007328488727103016
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_198 :
Polynomial.coeff recurrence5Scalar1First 198 = -(((((3841234956 * 10 ^ 70 + 2203480349625745018590134461235091250277750366512686405702796671996625) * 10 ^ 70 + 2442355470916074035605248451626867620272073396886173099633092144158600) * 10 ^ 70 + 658533300890481552618192616151569499531886172257920046076209495708979) * 10 ^ 70 + 9065959131594953137530320172281704874340489073696201604150172638370242) * 10 ^ 70 + 6256951318572850551031925700103268412060527572169087846097590337223691)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_199 :
Polynomial.coeff recurrence5Scalar1First 199 = ((((4515607386 * 10 ^ 70 + 8252349865594140020551552303661862185232848491216361781062920677813992) * 10 ^ 70 + 1888676742328486121270219954105039284547515475965928576037058594645225) * 10 ^ 70 + 520924965251348273282963610747051843776383391046860271066420091545720) * 10 ^ 70 + 6702390261930564379117199284509497954913956888771911956049671545324247) * 10 ^ 70 + 9271169593082534475634438809707523038096483178368803129023340366474303
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_200 :
Polynomial.coeff recurrence5Scalar1First 200 = -(((((5208513817 * 10 ^ 70 + 1751559145729882177724467285039951123970756505922277474693237826919993) * 10 ^ 70 + 220977678922377611482235811818166048743820282362747994107557254518941) * 10 ^ 70 + 416340165811939882467092807260260873352891092549923219795084585360441) * 10 ^ 70 + 4612167038508846245041890453499612108454655935957498154151769559532891) * 10 ^ 70 + 9653487709109433931447765220211984984312706297583844618807063056607044)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_201 :
Polynomial.coeff recurrence5Scalar1First 201 = ((((5893135461 * 10 ^ 70 + 1796262521442511608105289687386476181397049099388782534452251348668678) * 10 ^ 70 + 102403197995172437057542662755628522430687062791369258043305216577398) * 10 ^ 70 + 8075757282638080994627844826402665547270402972163362912596933624651229) * 10 ^ 70 + 7348093052527698944571046109843576333418780354331001770648850490479125) * 10 ^ 70 + 7049043268061827010469477883733414209752942240779886184112459857330522
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_202 :
Polynomial.coeff recurrence5Scalar1First 202 = -(((((6538441950 * 10 ^ 70 + 291300320198007005883918835234561488042068155985157545687228317826643) * 10 ^ 70 + 3414254963620943160723156071534150313754879575493796965368921967803668) * 10 ^ 70 + 2092634183267878644190057540255740934853515965080370799204900061860790) * 10 ^ 70 + 9031381993846141793041597575067254143877442859911186521331225796313534) * 10 ^ 70 + 9214805906340154270851518436420107387954599306815347531439443952377380)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_203 :
Polynomial.coeff recurrence5Scalar1First 203 = ((((7110987566 * 10 ^ 70 + 1913624227049615073528724273193381455197229497354697024989524280867458) * 10 ^ 70 + 7031804654797367663982917084334948055184538942319312257201027654814410) * 10 ^ 70 + 5589102250907948098692814650878376031223729140285406890172955133942662) * 10 ^ 70 + 2863923107946767903632153949320725319919806805901844405408362714976177) * 10 ^ 70 + 438338337010420395023120169693534279124118428833235947185315834299622
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_204 :
Polynomial.coeff recurrence5Scalar1First 204 = -(((((7577239116 * 10 ^ 70 + 5197291147157876451044808732803473865139284470634056935880581906312103) * 10 ^ 70 + 7903697595587733849854791763180781490755489546344579202135338312054276) * 10 ^ 70 + 9034646324068152156179376069807647519449298013378900894109930658533776) * 10 ^ 70 + 639003706077947210783609774451943958697189005881802539605337389949050) * 10 ^ 70 + 4466072084965543012841388484051096061229972463372343685662634640638109)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_205 :
Polynomial.coeff recurrence5Scalar1First 205 = ((((7906248436 * 10 ^ 70 + 3217119855203330097876793503296416794573664478627339519914774574814010) * 10 ^ 70 + 7870236262339957659508747795158532584699200851737935858030576009447859) * 10 ^ 70 + 5562006413642773362687917882980047725679083910171707486033333118802551) * 10 ^ 70 + 4460065794517861128078674377161530244445434415061376051751939953491873) * 10 ^ 70 + 884089015494777655280191134838921156558950479350230035326082087962345
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_206 :
Polynomial.coeff recurrence5Scalar1First 206 = -(((((8072409222 * 10 ^ 70 + 1901086579729513573688328304781893434893658652530698444349273171974533) * 10 ^ 70 + 8034412934349725305130795685206430740498048341162623472623355578056485) * 10 ^ 70 + 2862652164795050371183489395306320577650978589961872614917593602350573) * 10 ^ 70 + 7938312104381686048715904227581347114024495773532362693763115934951976) * 10 ^ 70 + 1755221568180402057781972410276461932665946077977645373379363538793512)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_207 :
Polynomial.coeff recurrence5Scalar1First 207 = ((((8057993187 * 10 ^ 70 + 8242523605345971190032706087716770663451211658118556090071300773064576) * 10 ^ 70 + 9975916804795895813904258435460080234211803758688718407682372927295944) * 10 ^ 70 + 2964627704808166327689738743662434132033996272594497828183886334263769) * 10 ^ 70 + 6286491510153814743263498920427617429212405126591925610893251363553555) * 10 ^ 70 + 2877642560211683667032798820626265242260706011448024198777627594655746
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_208 :
Polynomial.coeff recurrence5Scalar1First 208 = -(((((7855155542 * 10 ^ 70 + 9417214341889542476450589910659372086672566661817432728301650344442283) * 10 ^ 70 + 360063916423757968986381089092534571477246266866995096834639143656028) * 10 ^ 70 + 2086680380299382952581578131960772657891859633024570000395869974579196) * 10 ^ 70 + 5706292230834124105446109537700990635031578728761596352734443614219273) * 10 ^ 70 + 4588384163145128536615767015905008967851846706858044818971892402958243)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_209 :
Polynomial.coeff recurrence5Scalar1First 209 = ((((7467139806 * 10 ^ 70 + 5780174956118981641370887698419039802725262433215760611881234787807159) * 10 ^ 70 + 1663021281895325637192897311990977078928736239283868669221385567337237) * 10 ^ 70 + 5003917108272337020491199755393797440914462012126769330207970938431003) * 10 ^ 70 + 7695234095270866223886349592820433174919640658060074728155279122900685) * 10 ^ 70 + 3391485222482785750361750458008893276760330118164230751199750389398639
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_210 :
Polynomial.coeff recurrence5Scalar1First 210 = -(((((6908494753 * 10 ^ 70 + 3509291741487860635553214088098688658892389657499597102666286194580413) * 10 ^ 70 + 7424177155166796973971228322679020672011179790418317389638819116000352) * 10 ^ 70 + 7760907371624213978032895441020526643216220121444981471745048938967095) * 10 ^ 70 + 9068871479417476031917661337061498057095018135737692482844129496542041) * 10 ^ 70 + 3123477463204868996100530288818742068816728741047940018251974354145855)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_211 :
Polynomial.coeff recurrence5Scalar1First 211 = ((((6204231811 * 10 ^ 70 + 4000827400872709616964494355538786288584421011567051928739794029979597) * 10 ^ 70 + 4137454689236479778530806429163324738679536918084032574900061757971357) * 10 ^ 70 + 1590455374134709825952925803980150332481906637589273495816126490882943) * 10 ^ 70 + 4052263070888613416425548483468186945848115856571946513130975045676888) * 10 ^ 70 + 7082070289033444372202088633652398507429088239165500930955133038328110
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_212 :
Polynomial.coeff recurrence5Scalar1First 212 = -(((((5387982952 * 10 ^ 70 + 8486959036498659787530795245324502496158792883386790178685083050579638) * 10 ^ 70 + 2821268703646673904621024340313799405696360506621686765077862534979867) * 10 ^ 70 + 5039332313410794501934894814892819861056275791704755334563652687307897) * 10 ^ 70 + 4013886238864461925550754568588473098005291394966401820504634366392564) * 10 ^ 70 + 5949015246896409242734889651697664523505247405803532772559623919114586)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_213 :
Polynomial.coeff recurrence5Scalar1First 213 = ((((4499346795 * 10 ^ 70 + 1222226726058061380588864178632347144006563012588399185061188055190452) * 10 ^ 70 + 8737211799019432741744303172923613385073775671319922155512887744315054) * 10 ^ 70 + 2682378141099257888656350623855294981055276581669827605850430284773560) * 10 ^ 70 + 4925999937394022949053468996607696058701348152080899333999834011687820) * 10 ^ 70 + 9787329637272277389605840900228958869853945542194412191641072885923046
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_214 :
Polynomial.coeff recurrence5Scalar1First 214 = -(((((3580713991 * 10 ^ 70 + 1944763633669761528043395299286397455191362504853059581008087142613053) * 10 ^ 70 + 2639238270442539916550283066274359680456555538237418873027267438462599) * 10 ^ 70 + 2847568852832134403877431494042818731752485302980423704365193967458222) * 10 ^ 70 + 3015369905555403210690423246369987663614454261753294535246393925420565) * 10 ^ 70 + 9619506661034416038265349462400387001899250761652030522050170115061968)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_215 :
Polynomial.coeff recurrence5Scalar1First 215 = ((((2673925561 * 10 ^ 70 + 4196216206697819582203051929014366977372042464376502868797048790996736) * 10 ^ 70 + 3894676170742633998428964954626634912758348642206212091461260989079376) * 10 ^ 70 + 1665530188907545866312695314480126281588943612710523902626196402471760) * 10 ^ 70 + 8105756472662890290112101554048268072275337535187427833602530602236582) * 10 ^ 70 + 903163721131406717057437842857384149198982713680457226479342355292035
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_216 :
Polynomial.coeff recurrence5Scalar1First 216 = -(((((1817130084 * 10 ^ 70 + 4765070570878638598107520127187721560837110510780371529677552573778618) * 10 ^ 70 + 2442657081105526210848443873092492438543175431017732871345640002647431) * 10 ^ 70 + 391862905406200102552765540340369551948824379140593401842289584552545) * 10 ^ 70 + 5722024354759555928761084665789093214684522787959771038528626035200966) * 10 ^ 70 + 3141999191655551516866089880791053844731684478561428003347941249507323)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_217 :
Polynomial.coeff recurrence5Scalar1First 217 = ((((1042166786 * 10 ^ 70 + 9714083735609125131544764258812929077895572138211268023450892353316538) * 10 ^ 70 + 8211509472567083148755340809488054459281312062261043630644070638685783) * 10 ^ 70 + 958085894376163943381046724677963204767523896368314144451887591717765) * 10 ^ 70 + 4289128348650206389545389696164242303736106990664309131036442446136260) * 10 ^ 70 + 9505810660407140281719854989062649377312905864225857617684431205495326
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_218 :
Polynomial.coeff recurrence5Scalar1First 218 = -(((((372719393 * 10 ^ 70 + 8649882912349107463480323940820090973461973212654863585472471013731768) * 10 ^ 70 + 113570519725671526635669177614581229772269817889399874840622195927197) * 10 ^ 70 + 5029191081232869750175086653897571913755321148481776323831471987048878) * 10 ^ 70 + 7462118253019616885280207817702073617781976324892455422425401374905699) * 10 ^ 70 + 9423147806887945856294586878114850868565642912872785438751153051863912)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_219 :
Polynomial.coeff recurrence5Scalar1First 219 = -(((((176625097 * 10 ^ 70 + 9055082972459972200630153281327092263725593222715907645462060111025473) * 10 ^ 70 + 4807419048530039291170013787999435041802469969485180280853453412179871) * 10 ^ 70 + 4353118367208060353939242291028280711143413591561627179121853917851616) * 10 ^ 70 + 9634800287325989972416898116712409733320943186967277152590159314564836) * 10 ^ 70 + 180413710071007098052315724365965731035879891840126808187713092022207)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_220 :
Polynomial.coeff recurrence5Scalar1First 220 = ((((600399113 * 10 ^ 70 + 2295345586407675815478678279651300327255992209819305969268665924992468) * 10 ^ 70 + 274864063747804394937772294934242807923378240104999100251293985627565) * 10 ^ 70 + 6857543407890485184063102422753119931917612449710281327295646664272981) * 10 ^ 70 + 8006581985964861235746590249061721999522434429996281209049839240955731) * 10 ^ 70 + 3619503606161209397861077440902912861100696262649601846517375538389374
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_221 :
Polynomial.coeff recurrence5Scalar1First 221 = -(((((901456527 * 10 ^ 70 + 6143077338653172402302141111940489493320412335702340763021874806654128) * 10 ^ 70 + 4791580214442559705185053828645213382350372827247688731880136153738236) * 10 ^ 70 + 4051056298239769723420718570583090155576843499360863134555768235771318) * 10 ^ 70 + 6371788766000356327842768907050932178482277793214088293415290110106801) * 10 ^ 70 + 7737916257909830441965002876259760593924204456477441294449232848243020)