Recurrence 4 lookup certificate: Scalar2Exceptional 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.recurrence4Scalar2Exceptional_coeff_250 : Polynomial.coeff recurrence4Scalar2Exceptional 250 = (((394763908340588738800164739 * 10 ^ 70 + 1711993788578182450411671667548583389831366843413009263075183845516353) * 10 ^ 70 + 1066655661142364976240157181783286952883106588654233087071637076090769) * 10 ^ 70 + 7760915803829541504343792893482130723461556389609691785825787855981992) * 10 ^ 70 + 27327560968595623689934507102140233631452018226550225864308409863402

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_251 : Polynomial.coeff recurrence4Scalar2Exceptional 251 = -((((423846233210788953136904877 * 10 ^ 70 + 9713772190779101537927806670210962056734549642253026955783121068275552) * 10 ^ 70 + 8037862315209024469851923032754770738175946537935447475667512764136666) * 10 ^ 70 + 7911279366855820695071450359836257433254477214633901102178612450912507) * 10 ^ 70 + 5325824948734886821771314833513900201337747198607258763408420159312622)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_252 : Polynomial.coeff recurrence4Scalar2Exceptional 252 = (((449105796353325438692926464 * 10 ^ 70 + 6957833559452221778956020074486109934788308429288419157201372708451502) * 10 ^ 70 + 5817578189642359524285951242436598096200844171955306803348552435919013) * 10 ^ 70 + 5224717224466839157727964217890141055477729360006000712778905748525746) * 10 ^ 70 + 291275668581520676907083106409712195560207932728505842931317411320099

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_253 : Polynomial.coeff recurrence4Scalar2Exceptional 253 = -((((469632871894879271767680029 * 10 ^ 70 + 1476451980358587050704355344391369923456110788577669183654457166955211) * 10 ^ 70 + 4873525480674402951129206939940138841962889304245640840897354528611958) * 10 ^ 70 + 5953673858429858900912634007936827263839667306451399674239330440195562) * 10 ^ 70 + 9448240006145651448361788675489928450537414534218000057592294857762772)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_254 : Polynomial.coeff recurrence4Scalar2Exceptional 254 = (((484660130505135699598332853 * 10 ^ 70 + 7670930887783143638789111430225113138908763560183803663928840062421640) * 10 ^ 70 + 4418436178611530332863573554150486080645119265528500861825209117930979) * 10 ^ 70 + 7836523831163155618936595293779715221131086786545593791284330382100899) * 10 ^ 70 + 2826351119376214609103748530126038076696339542763176624628914842733949

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_255 : Polynomial.coeff recurrence4Scalar2Exceptional 255 = -((((493610017439169838876313812 * 10 ^ 70 + 6491310553281965919360058100810914081803967004657815214411873724883075) * 10 ^ 70 + 4801186834976557855578393945141872971471167990997546239535822141961882) * 10 ^ 70 + 2399232808608326283565973976408707158278976434830590502104864016710046) * 10 ^ 70 + 4933538495643000414755609159824874175798515235321008040162353286692850)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_256 : Polynomial.coeff recurrence4Scalar2Exceptional 256 = (((496131424545306301640827354 * 10 ^ 70 + 947329730636294789712490747130606227405866978937211201134883734077537) * 10 ^ 70 + 408021180557565693302367781353424542149405208421299022422044941580230) * 10 ^ 70 + 6287366181160981202875689452151147876888210848093186510964659258429681) * 10 ^ 70 + 2304145565061079781262625732862929391025218936531983334322894678206903

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_257 : Polynomial.coeff recurrence4Scalar2Exceptional 257 = -((((492122422132073171829934586 * 10 ^ 70 + 7311136033317074072115704496491827508392688988595341370289918310527442) * 10 ^ 70 + 9511695162387466045958740079588906729289268631222475419866092539098794) * 10 ^ 70 + 6970062095125000619185302798897333145400896163385328169561272360099278) * 10 ^ 70 + 9570423263588409064055256174624180635641474183352391962833187903291289)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_258 : Polynomial.coeff recurrence4Scalar2Exceptional 258 = (((481737008390248269546727181 * 10 ^ 70 + 5814116055270069829531273904880869332421365449201031774742415153317900) * 10 ^ 70 + 5974583636060706577843146463721647382524181454416512592057215849853447) * 10 ^ 70 + 5630363368472115928819710431370584637312257807836238494778342062874059) * 10 ^ 70 + 8336789044179424045993680916019415228253900528851730105620734660010487

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_259 : Polynomial.coeff recurrence4Scalar2Exceptional 259 = -((((465375259935570201952748577 * 10 ^ 70 + 866680741230062106170003561615253839317794145458148234231096833022275) * 10 ^ 70 + 2162500869386409824774126588945990071386829393072745683378910315309066) * 10 ^ 70 + 1446306827584462065199771357428091007103114483574782293378919359974612) * 10 ^ 70 + 694452076582129547873420697666102954897635403122278219968387410059155)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_260 : Polynomial.coeff recurrence4Scalar2Exceptional 260 = (((443657764390996784407039279 * 10 ^ 70 + 895267023184150947313786353347922697508402223402331632250549296594327) * 10 ^ 70 + 8294000611444571635421501435524866513927778902895970716150919430062950) * 10 ^ 70 + 7294855823491270625453920746123919361914159571050522758755580559631296) * 10 ^ 70 + 1121903679756029667858406395392634035358537819845696996395082047196884

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_261 : Polynomial.coeff recurrence4Scalar2Exceptional 261 = -((((417386612154047017388407031 * 10 ^ 70 + 1736747552211761488276949768409427044893671808312993991246869569238571) * 10 ^ 70 + 9737681939601216002504768733081206778083662692400655834900009464807026) * 10 ^ 70 + 5064068889566753888937498783753643173879116909429819181746771714911) * 10 ^ 70 + 7760946096768048372557360460775050340357574464507630451926252038024965)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_262 : Polynomial.coeff recurrence4Scalar2Exceptional 262 = (((387496361138326423823488401 * 10 ^ 70 + 6165250536610636739814961258764052340988306299027172137248093132357463) * 10 ^ 70 + 362461586839407724052813256895230792782774917869543721931907782501834) * 10 ^ 70 + 7119624747124270550068630874809155846293880654107519699527610572663075) * 10 ^ 70 + 7699324905640113808255513147039169378510059549521843523107430481266786

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_263 : Polynomial.coeff recurrence4Scalar2Exceptional 263 = -((((354999142883696201161283622 * 10 ^ 70 + 4892262132190669739092709156975551055797021154202018691343143330089619) * 10 ^ 70 + 384595303704470032534825273859528371685951427015368899025866867072542) * 10 ^ 70 + 1047689671677708269733134817786493036685394129049145306156759707145553) * 10 ^ 70 + 8030870655722692201039487516423535779939585560027781579902888508349855)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_264 : Polynomial.coeff recurrence4Scalar2Exceptional 264 = (((320928380517225327259707632 * 10 ^ 70 + 1995907921722362899462500913589336086610097282123046849063199405828927) * 10 ^ 70 + 6584583584015362703977197045769453201295953844328620262630432519744791) * 10 ^ 70 + 5737827623493162778371772632995014473065020023537788579144296697339000) * 10 ^ 70 + 3680733579988688758817090654692110422406839803466562030244759373104796

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_265 : Polynomial.coeff recurrence4Scalar2Exceptional 265 = -((((286285427775088040367578170 * 10 ^ 70 + 1885002566909337318781296148974176754628904206273596336735856071641490) * 10 ^ 70 + 9510959612975715676835285305810984889352816178606336584636935629834501) * 10 ^ 70 + 5721689255120812449680583739952780654250086295303542064205831163723311) * 10 ^ 70 + 4749961262206740640066015141884343707968532702903231066453945535278653)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_266 : Polynomial.coeff recurrence4Scalar2Exceptional 266 = (((251992860895282542226455731 * 10 ^ 70 + 7537546485807382190099034327934219426532648029810262816881836418300529) * 10 ^ 70 + 1621110804377863740786691163578920207106283037487141970915291295334140) * 10 ^ 70 + 2393747674561354787698889801899876355803280080761601376030672575548893) * 10 ^ 70 + 4680464234578174904880620941725758729184815152286051545083162385988770

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_267 : Polynomial.coeff recurrence4Scalar2Exceptional 267 = -((((218857256898969861576888979 * 10 ^ 70 + 1306676871525344621439110504367213844000689613124286531199519281930826) * 10 ^ 70 + 5085392989921687009379860610392461422424379576650180585480488274925521) * 10 ^ 70 + 1187622832684015122046790927943010875831266990939917121975488159949991) * 10 ^ 70 + 4705751695547125538949136222838496967412595566109434487076556821056045)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_268 : Polynomial.coeff recurrence4Scalar2Exceptional 268 = (((187543199405287443526123988 * 10 ^ 70 + 4180164117004992710276122969568579039194877672677904765225367768509522) * 10 ^ 70 + 3369564581827395909929510066515075001815014793614426717393433371899335) * 10 ^ 70 + 9197263039193431687572209616234426307282847566179722922335921742208652) * 10 ^ 70 + 4771264253659364912681866795975033668412119936636257397188504964102805

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_269 : Polynomial.coeff recurrence4Scalar2Exceptional 269 = -((((158559105341861245242563558 * 10 ^ 70 + 292297709024903974078670984576573385105925534115570213301930743819579) * 10 ^ 70 + 2027446527015836634583794403974150771564039034745703891422037753358939) * 10 ^ 70 + 6122854757562160528998386384121741828051306579053869839453812784238011) * 10 ^ 70 + 7806165984229618344557682206821266803515905560846793097119830563909653)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_270 : Polynomial.coeff recurrence4Scalar2Exceptional 270 = (((132254393641857938247049281 * 10 ^ 70 + 523980196159034455349258807177557414658507916634239243757883757201889) * 10 ^ 70 + 365071563544325608864296618954587363497546078015448265566247665302931) * 10 ^ 70 + 5391792873001082510706756850852009582136748819697776347697723678093654) * 10 ^ 70 + 2459951019771588501733549515816947669364656861696609427314836089086161

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_271 : Polynomial.coeff recurrence4Scalar2Exceptional 271 = -((((108826626978262168356525736 * 10 ^ 70 + 2683574961002739414590917416963352400128443475515534901885267789894573) * 10 ^ 70 + 8014136056799526085334986213835250454782187716436175161658869684515498) * 10 ^ 70 + 5665993485326263952498625954915880472934653420487304155030942347651044) * 10 ^ 70 + 9737754724687910494677424790695991114031887251980655837494014025569688)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_272 : Polynomial.coeff recurrence4Scalar2Exceptional 272 = (((88336621214306093336536410 * 10 ^ 70 + 7551118984354246063716381709972324796317744220098778862798378742989560) * 10 ^ 70 + 1911328899375779513167736399825019613077321255383556922575673354722375) * 10 ^ 70 + 9798795129097760095248060171275887541853365472770006047430516985505395) * 10 ^ 70 + 1723496808784292697095599918114927587738366080490042144771351708680458

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_273 : Polynomial.coeff recurrence4Scalar2Exceptional 273 = -((((70729166047772119026580784 * 10 ^ 70 + 7469236413880561096310533761684067718681946403777257333498415396263446) * 10 ^ 70 + 8557674342607323831145971228581373515114250597520075816691144649716849) * 10 ^ 70 + 6285010667567045475039042215931880076501060533746407804387667809354592) * 10 ^ 70 + 5402173147300059800268435668775338284687279964700291926499230857413944)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_274 : Polynomial.coeff recurrence4Scalar2Exceptional 274 = (((55856927504074519019113467 * 10 ^ 70 + 3933137691440523410793954221287242377874789587637857064471233099014065) * 10 ^ 70 + 5719648086430167590070095171758909260313719966951361305363165326403641) * 10 ^ 70 + 6914513837813457243822357160959960392960106566331114353889090299060838) * 10 ^ 70 + 3277835272479012723038576166630614732057999846896505002773351725986298

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_275 : Polynomial.coeff recurrence4Scalar2Exceptional 275 = -((((43505270183923502003579291 * 10 ^ 70 + 7621957522163996979869391122653035846033036999788222297905224374100182) * 10 ^ 70 + 5186190481059838692682643849652324204587452676737003955465346197887387) * 10 ^ 70 + 4920624849762203740880954051329678949861257110791555061149390415588036) * 10 ^ 70 + 7361551397803776505722376767824170057424600501942518634706422743281840)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_276 : Polynomial.coeff recurrence4Scalar2Exceptional 276 = (((33416084781724029164470674 * 10 ^ 70 + 7836972923892988486510514123534661040314276078679995556757075755965282) * 10 ^ 70 + 5481873325223881924843234476925324999974502627297639845395642497020345) * 10 ^ 70 + 2126256051414267273258852878527217446516015552126056269272510184977946) * 10 ^ 70 + 7406969922891049379426240570666662980250079614573618049265944131923270

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_277 : Polynomial.coeff recurrence4Scalar2Exceptional 277 = -((((25309164592429824664660854 * 10 ^ 70 + 4273420751895883268101457889297284939665617530369323941333075056809392) * 10 ^ 70 + 5628412245765775873840928185142680290665935009146825630230605025510622) * 10 ^ 70 + 5491317241303040354640968987614710061110868370805053059203393041676879) * 10 ^ 70 + 7264982994088096559602276880404893467814167303283778736178948563054971)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_278 : Polynomial.coeff recurrence4Scalar2Exceptional 278 = (((18900174385107635408901847 * 10 ^ 70 + 7527872438784745438700992454583027376174229389059871089141623078364254) * 10 ^ 70 + 2498647660065612431094693163859093917109713793101565662877484321057475) * 10 ^ 70 + 9574425959671491304058706859554086685254150774698026100405399659654903) * 10 ^ 70 + 6582592831312975947672634810043996802645432923451755167943957336587096

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_279 : Polynomial.coeff recurrence4Scalar2Exceptional 279 = -((((13914736204008382473396516 * 10 ^ 70 + 5797470439656875900157759467275742447541208526982402005264382929114020) * 10 ^ 70 + 2049897129893540096322925852836051291312290749321125193683618937996003) * 10 ^ 70 + 5863790332828181403421730000289165572068120246636088801445411545825707) * 10 ^ 70 + 1751282077912458413375697526346433735456883072694406769397023455861259)