Recurrence 2 lookup certificate: Scalar0Main 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.recurrence2Scalar0Main_coeff_303 : Polynomial.coeff recurrence2Scalar0Main 303 = -((36427363813131744331224640438279500401535539318297506395 * 10 ^ 70 + 8380473836019611515788176715079812596436994449046639632578937714901492) * 10 ^ 70 + 9992057801730731695930030785711845387513554819000609957847518370497950)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_304 : Polynomial.coeff recurrence2Scalar0Main 304 = (8546289844532699770300440854474425424639256475572349079 * 10 ^ 70 + 1305043076838989460420266017559372286920663996172782795560881260931548) * 10 ^ 70 + 5002996591845387432725791240726707327200429811666381553768211820941532

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_305 : Polynomial.coeff recurrence2Scalar0Main 305 = -((1802065715256272371499037429109465471162450132589535768 * 10 ^ 70 + 3900016146568807256802601418122747338315789792274137510176697730282714) * 10 ^ 70 + 4088834683981002440931284579186692211172430301602660172366074540056788)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_306 : Polynomial.coeff recurrence2Scalar0Main 306 = (339576234181894496802033905765781042425722650299483274 * 10 ^ 70 + 1093309764502341415691537120388214621666325336035565604676948423037545) * 10 ^ 70 + 2568435777732797451667461373596607941850192391301696146889926943726873

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_307 : Polynomial.coeff recurrence2Scalar0Main 307 = -((55999465719470506701911457374548863966389193297514096 * 10 ^ 70 + 5275216476280036978146888771422876900943630947070781805925533655815110) * 10 ^ 70 + 3870404982810788492281165704300626298668716762140803133203334382956662)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_308 : Polynomial.coeff recurrence2Scalar0Main 308 = (7645668514833020499320402153590713464088963264915185 * 10 ^ 70 + 8086658433019387817356957198953297977827729362241075473901887869543057) * 10 ^ 70 + 6563577102720738994433195371918287968107411664323419639521447485777145

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_309 : Polynomial.coeff recurrence2Scalar0Main 309 = -((712962873099537548183620998001903116923774196012328 * 10 ^ 70 + 3339431874247543972238957661254412969724721336483936824695022957691419) * 10 ^ 70 + 8744048090596600210140382210003519916224899418632623111348706874892471)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_310 : Polynomial.coeff recurrence2Scalar0Main 310 = -((12264364436915592209569826791664051497231762147251 * 10 ^ 70 + 8198781438095178356190375729680409186587893249522080840915775866460834) * 10 ^ 70 + 5208456618925558239467761378341461785354211499867470207763575570698520)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_311 : Polynomial.coeff recurrence2Scalar0Main 311 = (26733877445043088951398960292466797618086177625189 * 10 ^ 70 + 1763625062473534610358910948880367129436322333452183905259460295842187) * 10 ^ 70 + 7256706444129076205958882398931235570957305985034774664520942311657634

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_312 : Polynomial.coeff recurrence2Scalar0Main 312 = -((8284550868544654871949469502019650584966976731277 * 10 ^ 70 + 1674868117520489633224683895884813819095305325672412929481404311914585) * 10 ^ 70 + 6488332620911450850731744802800111917225783469578465427493920423294735)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_313 : Polynomial.coeff recurrence2Scalar0Main 313 = (1847661331918508133933640470547491168667752415685 * 10 ^ 70 + 6485520268775233470777656044397590477079682557653430463489023786487889) * 10 ^ 70 + 1380512952370473383257122536258636003728996783990482402329170370781781

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_314 : Polynomial.coeff recurrence2Scalar0Main 314 = -((343175472794464527860869239887647693640044931928 * 10 ^ 70 + 4962160700816302654005903364219424256486667851870348585594968137726727) * 10 ^ 70 + 4040517273742157082823732730456168428662578381655097293637700581597518)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_315 : Polynomial.coeff recurrence2Scalar0Main 315 = (55379129825453297835046970733701261460619040517 * 10 ^ 70 + 8754906631373089700499019902297984975963991713987665634846620884221277) * 10 ^ 70 + 7936113192232564743675958089074259303432671403299202105442900996288727

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_316 : Polynomial.coeff recurrence2Scalar0Main 316 = -((7848291173427262120846160766148741342813677932 * 10 ^ 70 + 6993356981621667035285934283281619174134078232222713516422329525172595) * 10 ^ 70 + 6356868564250091860866439942390717415792767957624584025392369743687040)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_317 : Polynomial.coeff recurrence2Scalar0Main 317 = (967339076056192114580861246886321735172618213 * 10 ^ 70 + 1434025495073720984675327266075506382934850665318941991925190572094012) * 10 ^ 70 + 3028353581231891582133219236841829150549830286671722788135673594119186

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_318 : Polynomial.coeff recurrence2Scalar0Main 318 = -((99556399345891242931138624171136795338866347 * 10 ^ 70 + 4248850627150819509988662060799993863364437475141318018746278339014214) * 10 ^ 70 + 5480928914757604506604649291838896716621442781812377229436062288182737)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_319 : Polynomial.coeff recurrence2Scalar0Main 319 = (7443756064830284837920663225333731734679283 * 10 ^ 70 + 1868218164381174301713119870851220012743882840275406983078307179016114) * 10 ^ 70 + 9945851413440573119831871808631506811309739489185079163291257442016890

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_320 : Polynomial.coeff recurrence2Scalar0Main 320 = -((107574314259787030799618138558085865179591 * 10 ^ 70 + 7038359506014832320107713274443102694320293455525607832377029466258944) * 10 ^ 70 + 7339559290507746524255083382660075471312014147347457130612646499865297)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_321 : Polynomial.coeff recurrence2Scalar0Main 321 = -((94603000283693972853055956618655950863657 * 10 ^ 70 + 430338514353880486964311007767381995274730457427788300071638984495439) * 10 ^ 70 + 3173814970459826858636903793207207057323273449000747461398018938738926)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_322 : Polynomial.coeff recurrence2Scalar0Main 322 = (23126533298365883817953797120300421865131 * 10 ^ 70 + 3769299790231452026229261907135182137106953836092854285829090369532691) * 10 ^ 70 + 2706162160550839133017488029091855308641813649008795758773322885906123

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_323 : Polynomial.coeff recurrence2Scalar0Main 323 = -((3717451970750718124377219135060570900746 * 10 ^ 70 + 8974113690553412359429053175641803160523854508790707514016179315857123) * 10 ^ 70 + 8219744005792724911255006499803665216160795858843306590409825196104006)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_324 : Polynomial.coeff recurrence2Scalar0Main 324 = (474060458432510692422369581769890271109 * 10 ^ 70 + 4948110171889483905988603967680359184035826504196799062077346207311063) * 10 ^ 70 + 5139324548580879704759838621184860733752365674813098839450005384114521

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_325 : Polynomial.coeff recurrence2Scalar0Main 325 = -((49360163516387943226773181313093915287 * 10 ^ 70 + 8244729173087570043673358991183940710534231680326420633492781197817294) * 10 ^ 70 + 2652168166805710252535147944531276645231417197629002003224219859827307)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_326 : Polynomial.coeff recurrence2Scalar0Main 326 = (4031095699685932065030499212958323079 * 10 ^ 70 + 5718520732434552455333328762144293547411259729160606010163413483747344) * 10 ^ 70 + 3757749373617640332254601232245053330621161146621685318862796916358695

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_327 : Polynomial.coeff recurrence2Scalar0Main 327 = -((212574222187937552821681505512026222 * 10 ^ 70 + 629883353036632127565437751582135948327001941037358425514705697068005) * 10 ^ 70 + 7148539999963055513038404385688193738069016214647104477595542730140136)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_328 : Polynomial.coeff recurrence2Scalar0Main 328 = -((2436934416261278913332784669888278 * 10 ^ 70 + 3134207461342747076842947046396162280237364392204652638912434755739093) * 10 ^ 70 + 2915796992359593095216948206070878579207641360937326543331927350556592)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_329 : Polynomial.coeff recurrence2Scalar0Main 329 = (2276908397891162647236101210668375 * 10 ^ 70 + 6409238001212191765677375053148131618319019102044795521834072024773932) * 10 ^ 70 + 1233201030026815419841318061944851769316591753181463359014014338003505

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_330 : Polynomial.coeff recurrence2Scalar0Main 330 = -((328000199020452760072587656965377 * 10 ^ 70 + 5920542634098568375755913125228214113000918694472811782453033483309361) * 10 ^ 70 + 9874579397461101210154370001041747149062532594796423439287748877707944)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_331 : Polynomial.coeff recurrence2Scalar0Main 331 = (30289266453480759367367872092389 * 10 ^ 70 + 1261343185763702389628636411439245020400826924025533226501686612521128) * 10 ^ 70 + 7307930496807968654232319092003137403844187436243954528692175713576549

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_332 : Polynomial.coeff recurrence2Scalar0Main 332 = -((1877565466017380407646719537407 * 10 ^ 70 + 61186455965953625490990077949270502971656831277840640320418727835073) * 10 ^ 70 + 7620764029281708280898144507456173269618728746187774126695212100218890)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_333 : Polynomial.coeff recurrence2Scalar0Main 333 = (51938218172859840707316348072 * 10 ^ 70 + 8960587917687207995959258399461584145342774374067834981601747244599549) * 10 ^ 70 + 6127239462450446797028794105843830505257355181811973476403856652825344

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_334 : Polynomial.coeff recurrence2Scalar0Main 334 = (4327438710949920155349846119 * 10 ^ 70 + 3741406638069969576082201316906317126325713497068226457250275876517714) * 10 ^ 70 + 1246439042390960757207345981429540900551591692252164252268670304139552

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_335 : Polynomial.coeff recurrence2Scalar0Main 335 = -((750476104334498944323821439 * 10 ^ 70 + 187504830839361865547662672948330220918112972929207075089887122280379) * 10 ^ 70 + 2958082731668206053854898427701137387283259074288368243166418365404910)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_336 : Polynomial.coeff recurrence2Scalar0Main 336 = (59347853580534822405051781 * 10 ^ 70 + 3434425842115830613586541306046302328462256542798793999220469597855751) * 10 ^ 70 + 5099801447598638820255584674521198753086017817434454648503043458006964

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_337 : Polynomial.coeff recurrence2Scalar0Main 337 = -((2796558143083668872921983 * 10 ^ 70 + 2847312118003523270807066201696290248675672637875145875978078698568508) * 10 ^ 70 + 739832184091693686733114742301282675253755442793361675649253086646501)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_338 : Polynomial.coeff recurrence2Scalar0Main 338 = (44178320122863238523436 * 10 ^ 70 + 7609419462143753835443685825714143403053586545548140314718549584313406) * 10 ^ 70 + 7916886007977864185280422305801078461653795541258302755074984784467902

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_339 : Polynomial.coeff recurrence2Scalar0Main 339 = (4907344720406900476056 * 10 ^ 70 + 2766751433452334372360140267065448590808279864657519873246518868475500) * 10 ^ 70 + 5305404796760732198714552701319543746348374002787512253192404989609238