Recurrence 2 lookup certificate: Scalar2Shift coefficient convolution

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

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_267 : Polynomial.coeff recurrence2Scalar2Shift 267 = -((12830409958372056761191967383443123580807413530696797696974570545777 * 10 ^ 70 + 5404080132971994843664661136377874584234488163637172208627381999105666) * 10 ^ 70 + 6092673117634037446672713813393041602369757044173733061596645120813107)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_268 : Polynomial.coeff recurrence2Scalar2Shift 268 = (4467265312436043746002885869480827786537808428563770938911573631806 * 10 ^ 70 + 2719293989369163298282844590657378626413185421997949869287045930715570) * 10 ^ 70 + 1079860660926905123863786978996573324848816514027543147177937096809645

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_269 : Polynomial.coeff recurrence2Scalar2Shift 269 = -((1203479375274657055289267183182563427642579086575001355381679730473 * 10 ^ 70 + 6462254616119439622312153402482463777226386251556572824238399313072041) * 10 ^ 70 + 1749223463434334336267061011381465059098530526482636315303531742535810)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_270 : Polynomial.coeff recurrence2Scalar2Shift 270 = (121061429829506239845213466482725873126934532452909499079044683830 * 10 ^ 70 + 9943780168106947855197028742090272651935137075094446671248009728640714) * 10 ^ 70 + 7087198776527659916178923021463024773814199682086666954764530879272921

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_271 : Polynomial.coeff recurrence2Scalar2Shift 271 = (136447268273609378952565838790899711138987923622979187303105363956 * 10 ^ 70 + 6187567675269018781684277915956080928623144225195018802007016097826782) * 10 ^ 70 + 1643530469776696591201539484615283198556770779687179834179310352286739

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_272 : Polynomial.coeff recurrence2Scalar2Shift 272 = -((136692103957674260766955318055045477476979960331381952331932487099 * 10 ^ 70 + 8835717429248434138340262156251317499372825250046766505148597278354818) * 10 ^ 70 + 2073886823382376535651186871998136493735926298210598814893450622678065)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_273 : Polynomial.coeff recurrence2Scalar2Shift 273 = (86278162971422170754309043267651668728131907132887655738497600570 * 10 ^ 70 + 3575339058942497803349205047805066663648994574888523403847848127238780) * 10 ^ 70 + 8648705463675450746844817259980724204697062503533947373556342347592647

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_274 : Polynomial.coeff recurrence2Scalar2Shift 274 = -((44667983946692880239030397728351590438751669051557647770409190873 * 10 ^ 70 + 6504914380971383181707980884766933029919429764493066474722306215166438) * 10 ^ 70 + 524019926947105574769160201228875049655339541999397200252145073884013)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_275 : Polynomial.coeff recurrence2Scalar2Shift 275 = (20238405382895585452412703717783741503221326716096687523036596029 * 10 ^ 70 + 7705060796653513016870456179282082940361784738615895202366683815464094) * 10 ^ 70 + 5260839924944995915572008830966724061583705266229790360168749306392583

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_276 : Polynomial.coeff recurrence2Scalar2Shift 276 = -((8193772790726924955349766474125609786974905452209596907920057838 * 10 ^ 70 + 5349931444603792257965818851500911144711636861361356279316209265560635) * 10 ^ 70 + 9915312400115999340398431788729205461366917372495106175861288296770314)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_277 : Polynomial.coeff recurrence2Scalar2Shift 277 = (2968413801362859009150152677795644358107001267942265271061227731 * 10 ^ 70 + 4129849218772029327601789875681991763106961661797370267816200066130297) * 10 ^ 70 + 7682679666520112741000886188759924247363240252430057908188119544786346

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_278 : Polynomial.coeff recurrence2Scalar2Shift 278 = -((947089763352013695381244865909725440752269597902289289358212228 * 10 ^ 70 + 3568562710420271151667232627411099008580412899084517654058410127517176) * 10 ^ 70 + 3133156536328754442077765691383169167716342113252034548947925051347903)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_279 : Polynomial.coeff recurrence2Scalar2Shift 279 = (253665504201147603807725474404269497743327095660191298092514436 * 10 ^ 70 + 660248443993538669072322953445294013003376967430791334581844904268056) * 10 ^ 70 + 4284022152760979328893950167328870994100145017722005412385044479223132

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_280 : Polynomial.coeff recurrence2Scalar2Shift 280 = -((48562162441140780324700127285147913164609128059807418309992523 * 10 ^ 70 + 2110652818739285135638502401917443386847898510786162933026403200374530) * 10 ^ 70 + 9166352817173652487903236651739540275316318608139444200872781842216431)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_281 : Polynomial.coeff recurrence2Scalar2Shift 281 = (525433296574843902275555657726520289404396906368748768019115 * 10 ^ 70 + 7084284897645315149854403534728932435838775198468620325307745638447886) * 10 ^ 70 + 1752231070370673966951560223898837362698650387499585393889833064555051

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_282 : Polynomial.coeff recurrence2Scalar2Shift 282 = (5429901153611952300959760981010144828046311785192474136986457 * 10 ^ 70 + 9338857453996735111049787497239022077428307329652879678114483254845673) * 10 ^ 70 + 5568204219730577917673879050188538578937063379889252458221388475528617

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_283 : Polynomial.coeff recurrence2Scalar2Shift 283 = -((3464894190870487358557965569082695986809887198846807398758333 * 10 ^ 70 + 8698515436132428744044669080874262848342993686310981333240604368657205) * 10 ^ 70 + 1807333185707522034263319715354562055887850402483028069226016816383953)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_284 : Polynomial.coeff recurrence2Scalar2Shift 284 = (1528591349494439856204600559164719135354950610588628225886382 * 10 ^ 70 + 6546171320108478386241342388939331813413304087458880464781535651337708) * 10 ^ 70 + 6347184606881013113253936137999739879653152739628483866101306368648596

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_285 : Polynomial.coeff recurrence2Scalar2Shift 285 = -((551026473495782837516117679917596802880797368874796430366849 * 10 ^ 70 + 4291410267577492273684523998333696777003350334042871063057029628853589) * 10 ^ 70 + 9086959557666324637480729029756569643348810520438746253902724092435993)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_286 : Polynomial.coeff recurrence2Scalar2Shift 286 = (168142943748715401308358358424614574454191259506948651619579 * 10 ^ 70 + 7780388160619303430735529204473696665368640459943079363288101546553917) * 10 ^ 70 + 5537637412945497191957061302520442354005197321496062424265972763419095

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_287 : Polynomial.coeff recurrence2Scalar2Shift 287 = -((42756480222530860649345186297827821060076442897094567900269 * 10 ^ 70 + 9537256030622366379529160269511727076326355091491871245211294788310085) * 10 ^ 70 + 3176709650501777587656160023698034606394466563537506726671094439848463)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_288 : Polynomial.coeff recurrence2Scalar2Shift 288 = (8254060128515612340602177706734701732823701276698275767371 * 10 ^ 70 + 2876555883731262085472088219972041188385820704683279623276539173325864) * 10 ^ 70 + 1495927512420373886261470108688035940413757810469953612583046602985478

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_289 : Polynomial.coeff recurrence2Scalar2Shift 289 = -((690367696313948815877618184017168937590339752029980199231 * 10 ^ 70 + 6906890151189638082747376102178723287128981071617434016568424429534966) * 10 ^ 70 + 3755309709877465686025620762957722476446160184218828465354903434783176)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_290 : Polynomial.coeff recurrence2Scalar2Shift 290 = -((339182002236006524029978111828257937123143190892132846878 * 10 ^ 70 + 5169145229440759940893831850306648918068346770063557517347648346377733) * 10 ^ 70 + 9202127754625710573557341697667886346994800082782144171265416474407176)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_291 : Polynomial.coeff recurrence2Scalar2Shift 291 = (234070587960755050412152252841200379019986280619531854590 * 10 ^ 70 + 3767357644271380392949369349773605397958189514239799262969279287835581) * 10 ^ 70 + 1724720993947189799629360660278758161108885290732871414446424734911551

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_292 : Polynomial.coeff recurrence2Scalar2Shift 292 = -((92820369671971294090691578337936774116902777396789856335 * 10 ^ 70 + 2433659738167036178851760826596435248509184278513844115405390244312879) * 10 ^ 70 + 2290550093550435850763717263767552090322776733974318602422390607580135)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_293 : Polynomial.coeff recurrence2Scalar2Shift 293 = (28665506374262170563717902182871733089921030203381595473 * 10 ^ 70 + 8934061086717027389813781110965897235058232091344389081735471253991948) * 10 ^ 70 + 3862259346186415061478543011087558883962606438381945161086528925858261

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_294 : Polynomial.coeff recurrence2Scalar2Shift 294 = -((7281364781744811320894888437826495908951131275395621998 * 10 ^ 70 + 7181445106028205970337325419657530875499126679121562176926982217272284) * 10 ^ 70 + 3024436774200736200225135356180504182421125163965451951116594603417913)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_295 : Polynomial.coeff recurrence2Scalar2Shift 295 = (1493795809075001434190071456489441092252450803602883865 * 10 ^ 70 + 1547782166956496858582556063022951436129575957452907245286402453935811) * 10 ^ 70 + 9696762023645577475685973835859138116602126244931400874598702546627065

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_296 : Polynomial.coeff recurrence2Scalar2Shift 296 = -((217165507425195798722801188377005935370268532617130327 * 10 ^ 70 + 7276575492775654753793422826743926011960326956149041389934687439895308) * 10 ^ 70 + 9607789970045014608227933632831514414833662865968448673467594101364554)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_297 : Polynomial.coeff recurrence2Scalar2Shift 297 = (5702462625085868787804276865735180638135996602029187 * 10 ^ 70 + 8052102335682960113596734057434764498446600600112086682475051821472211) * 10 ^ 70 + 5104256837409248185659251890332235998174213001815952158443882428294662

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_298 : Polynomial.coeff recurrence2Scalar2Shift 298 = (10102127990504837050937526522508646487186322725440209 * 10 ^ 70 + 1952605197899198642441295938384785729825054057286243533856342919827409) * 10 ^ 70 + 6674172954094825983041921855749437312136331246848389852805660082070871

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_299 : Polynomial.coeff recurrence2Scalar2Shift 299 = -((4568904120008293905792115646582877759414873138658628 * 10 ^ 70 + 4424618453604155123036329079875604107515719492458786117872612738419659) * 10 ^ 70 + 2557776001240169878063771199593669132762352191324668071459680935405766)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_300 : Polynomial.coeff recurrence2Scalar2Shift 300 = (1344061608988275739421175627475843445442114387392985 * 10 ^ 70 + 8075301338095348540238315516052150097467097276570510834602692807637444) * 10 ^ 70 + 5232260313016604823319350313603727632909712806064231449670192648965551