Recurrence 5 lookup certificate: ExceptionalProduct 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.recurrence5ExceptionalProduct_coeff_303 : Polynomial.coeff recurrence5ExceptionalProduct 303 = -((5257408570997693248642 * 10 ^ 70 + 3304046149068527800338679752384839235911315418818159804942781035159980) * 10 ^ 70 + 887383746302513159068865991057158335227511912614620037068380046532527) / 5461721348121829606670420

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_304 : Polynomial.coeff recurrence5ExceptionalProduct 304 = ((2954635679898342737077 * 10 ^ 70 + 9544101415468578099251465648145546173118469420978438866217370969007812) * 10 ^ 70 + 5528956958285243948684385807178839701095751783196917269120199241479634) / 6827151685152287008338025

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_305 : Polynomial.coeff recurrence5ExceptionalProduct 305 = -((4804503319645411774064 * 10 ^ 70 + 6591581507479850495461343678237887888911237079362630727107033483654295) * 10 ^ 70 + 1090151768382308616635358528716666930532702786312139615304117886773581) / 27308606740609148033352100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_306 : Polynomial.coeff recurrence5ExceptionalProduct 306 = ((364993752578561961003 * 10 ^ 70 + 4644164772933589921629014989638344970127601238034329346504041005304320) * 10 ^ 70 + 7147303926008614857548395752336036216759342799252917014615721571755849) / 5461721348121829606670420

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_307 : Polynomial.coeff recurrence5ExceptionalProduct 307 = -((328659275303495616250 * 10 ^ 70 + 4080926795717506114871625740735823711467036364977872420655962536924441) * 10 ^ 70 + 7307833624099420334863821330380937097850638505757536131637243225483649) / 13654303370304574016676050

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_308 : Polynomial.coeff recurrence5ExceptionalProduct 308 = ((226011574397341964558 * 10 ^ 70 + 7793702313104187622705269354466489946990339216385852965790648801523253) * 10 ^ 70 + 8083562426388653520803101464461596842136119285662733102350980460796659) / 27308606740609148033352100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_309 : Polynomial.coeff recurrence5ExceptionalProduct 309 = -((74349967250895229638 * 10 ^ 70 + 976041806495301126965727399779188830627454003154466914976743235422384) * 10 ^ 70 + 620763283769522892186063974119151415371501860240201217897037852843033) / 27308606740609148033352100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_310 : Polynomial.coeff recurrence5ExceptionalProduct 310 = ((631794915626572828 * 10 ^ 70 + 2768286544526970733301639932193362937544176407725378337769046417587266) * 10 ^ 70 + 6336551471025899359911796097303474189764977478028246777071045836039257) / 738070452448895892793300

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_311 : Polynomial.coeff recurrence5ExceptionalProduct 311 = -((1749191706348660415 * 10 ^ 70 + 1679486692941522120874010544836962900611380268462661517201049804629829) * 10 ^ 70 + 9108793702501175164906511602988673590727961992808171461028052132945804) / 6827151685152287008338025

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_312 : Polynomial.coeff recurrence5ExceptionalProduct 312 = ((494768647796408364 * 10 ^ 70 + 7575141492140896055776758984496231482426910302491288495643160487904134) * 10 ^ 70 + 6931573371816149684883168553930535425057594328578411451632264547622342) / 6827151685152287008338025

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_313 : Polynomial.coeff recurrence5ExceptionalProduct 313 = -((130653250530948076 * 10 ^ 70 + 8508032720488684203308624061516796803135570009681924654386525230501529) * 10 ^ 70 + 1374073016087800399815859052596538466771172503526987534486200352683594) / 6827151685152287008338025

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_314 : Polynomial.coeff recurrence5ExceptionalProduct 314 = ((31531727444336553 * 10 ^ 70 + 2741546109196923830963005217487703729287368470029635282915341618173188) * 10 ^ 70 + 440070165630005466111665223592133502134610294734968302983460421117682) / 6827151685152287008338025

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_315 : Polynomial.coeff recurrence5ExceptionalProduct 315 = -((6660617468659714 * 10 ^ 70 + 1674129016015389657069123518831155515187148394707758864629908143665416) * 10 ^ 70 + 7177557707886537605182087975256009665350534399634474020277287671577702) / 6827151685152287008338025

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_316 : Polynomial.coeff recurrence5ExceptionalProduct 316 = ((175108478219092 * 10 ^ 70 + 7229175915709439957699350013591418597365598436382642206948243442967485) * 10 ^ 70 + 8943674968127466122867257531560274476632540607943487110648910230473145) / 1092344269624365921334084

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_317 : Polynomial.coeff recurrence5ExceptionalProduct 317 = -((53753338210177 * 10 ^ 70 + 7265452323785428943543747876419261646422558957220981957698802321742076) * 10 ^ 70 + 5194682918496131528411950376786810963454055524538461740390179688387293) / 5461721348121829606670420

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_318 : Polynomial.coeff recurrence5ExceptionalProduct 318 = -((188154583636307 * 10 ^ 70 + 8673895239522118677456772605229843419954586609629453875023827398459836) * 10 ^ 70 + 6830865406375427678243915681774970251304017079473310205748111900350631) / 27308606740609148033352100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_319 : Polynomial.coeff recurrence5ExceptionalProduct 319 = ((11654296128916 * 10 ^ 70 + 4396197118000385667968836079396077298344515060823126314502421222682100) * 10 ^ 70 + 1380113585214643750996981274912531171117286609503650299131098068977621) / 2730860674060914803335210

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_320 : Polynomial.coeff recurrence5ExceptionalProduct 320 = -((2291305765841 * 10 ^ 70 + 6312078641031560056844543023550364726402892701442733337368965160597275) * 10 ^ 70 + 7968011146420324457402154516646423433629938273266728714717526283762088) / 1365430337030457401667605

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_321 : Polynomial.coeff recurrence5ExceptionalProduct 321 = ((3729936773944 * 10 ^ 70 + 1618633979318017127480707499564604431552195728438585161719149619498676) * 10 ^ 70 + 4271120378807977044934404054799288133658590775352035078364747895998926) / 6827151685152287008338025

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_322 : Polynomial.coeff recurrence5ExceptionalProduct 322 = -((1077398324935 * 10 ^ 70 + 3850410433928891514684349536534363472755950766209549931321088836133498) * 10 ^ 70 + 1264470381422740792867329669648207484981449506091937199973797032536501) / 6827151685152287008338025

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_323 : Polynomial.coeff recurrence5ExceptionalProduct 323 = ((15348835039 * 10 ^ 70 + 1484796243962643740909077902562920094627766972337627960875015129590082) * 10 ^ 70 + 2051724235777012484783378484229329595333627542648070358211110212121977) / 369035226224447946396650

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_324 : Polynomial.coeff recurrence5ExceptionalProduct 324 = -((27692933472 * 10 ^ 70 + 8627052358524317989213838104171709808397551540328027236206383902030184) * 10 ^ 70 + 241467354251586419162792136593478242088473621826854774544045892274519) / 2730860674060914803335210

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_325 : Polynomial.coeff recurrence5ExceptionalProduct 325 = ((6293361698 * 10 ^ 70 + 506222827660106821761214268383474413513100781465909809238846702507217) * 10 ^ 70 + 1063846855571604378652845403586928541296408060119321960423045477950539) / 2730860674060914803335210

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_326 : Polynomial.coeff recurrence5ExceptionalProduct 326 = -((13387330199 * 10 ^ 70 + 7787747295817114876193999043723120980942775435062910043200524229210795) * 10 ^ 70 + 7515356730361063332607933432849778427091883394629279495224100779551849) / 27308606740609148033352100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_327 : Polynomial.coeff recurrence5ExceptionalProduct 327 = ((2671945959 * 10 ^ 70 + 335201865442054399896438703094515720428162461092016205783863896004186) * 10 ^ 70 + 4883751070899260951166736031122166844920095471695963633688276073114981) / 27308606740609148033352100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_328 : Polynomial.coeff recurrence5ExceptionalProduct 328 = -((500942234 * 10 ^ 70 + 1255938524709231200633898269745170040804314707036852205875640060591369) * 10 ^ 70 + 4930764615699866441850328674524989223193118268371706495830195525541131) / 27308606740609148033352100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_329 : Polynomial.coeff recurrence5ExceptionalProduct 329 = ((4412561 * 10 ^ 70 + 8674447825545753125220476730068076982784288834897091068180177940318102) * 10 ^ 70 + 669752269527297283855602398531998773861693660370901294673159386739058) / 1365430337030457401667605

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_330 : Polynomial.coeff recurrence5ExceptionalProduct 330 = -((3651339 * 10 ^ 70 + 1985357504264585688961311895267521272279533737035480806262884152954072) * 10 ^ 70 + 8416137060997951529145050454714908297726496621633329370442643191727064) / 6827151685152287008338025

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_331 : Polynomial.coeff recurrence5ExceptionalProduct 331 = ((1134519 * 10 ^ 70 + 9163524440089742360335811239676157672532051734265412953779843082611655) * 10 ^ 70 + 6988796213827392380805662634894730069555280687288047317209397124729661) / 13654303370304574016676050

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_332 : Polynomial.coeff recurrence5ExceptionalProduct 332 = -((165268 * 10 ^ 70 + 8469039586204211916220005269819785298495846714265858662823793273570291) * 10 ^ 70 + 57008320348188843928473370496361093537933874350787159776993800780629) / 13654303370304574016676050

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_333 : Polynomial.coeff recurrence5ExceptionalProduct 333 = ((22541 * 10 ^ 70 + 3156211430317061031903266345211144013408946147995980092935344044504499) * 10 ^ 70 + 9715709564463980407519347446171418343738463695193094918466417650552851) / 13654303370304574016676050

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_334 : Polynomial.coeff recurrence5ExceptionalProduct 334 = -((5746 * 10 ^ 70 + 8193550616919213793411578933262014063252245229536832748307582307968553) * 10 ^ 70 + 6077257939856200130704262220850901161507103391182082781799731058887389) / 27308606740609148033352100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_335 : Polynomial.coeff recurrence5ExceptionalProduct 335 = ((683 * 10 ^ 70 + 2175595152030797750079402004280977188323284739865169823942942434260748) * 10 ^ 70 + 2561095458221093590010198108912775059207251694824810602451576331895191) / 27308606740609148033352100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_336 : Polynomial.coeff recurrence5ExceptionalProduct 336 = -((18 * 10 ^ 70 + 8923194520463007587830928701936532449569588721333314831594070444777785) * 10 ^ 70 + 9984372844401080425444502723845896947450371522091654326181717819548276) / 6827151685152287008338025

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_337 : Polynomial.coeff recurrence5ExceptionalProduct 337 = ((1 * 10 ^ 70 + 5509804684660227281341545078923948584016875304641119394000913205958034) * 10 ^ 70 + 994463841327757556930868286537919833828519820634417123594006569147557) / 5461721348121829606670420

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_338 : Polynomial.coeff recurrence5ExceptionalProduct 338 = -(7359946853665670940795698378012010811120283416099447515591289398728702 * 10 ^ 70 + 2488520607107108998831273262269052708038335548567312553799734065862517) / 27308606740609148033352100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_339 : Polynomial.coeff recurrence5ExceptionalProduct 339 = (160920958499834557701133595538379729599563872265142293799821596117960 * 10 ^ 70 + 3719587632684497289430547976725405165140789771299976969282131814225722) / 6827151685152287008338025

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_340 : Polynomial.coeff recurrence5ExceptionalProduct 340 = -(12915810721850819730268630845187683005434695463361429459873462487262 * 10 ^ 70 + 5628469095960103356339670880649450678094918319141832398874997231070418) / 6827151685152287008338025

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_341 : Polynomial.coeff recurrence5ExceptionalProduct 341 = (946873617974393075011933025481417935680181584922803763426325445316 * 10 ^ 70 + 7095829880998342345306959588716066613365196248936035618459358145390519) / 6827151685152287008338025

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_342 : Polynomial.coeff recurrence5ExceptionalProduct 342 = -(12612119366028136319782234689941108496809757823495398558843663141 * 10 ^ 70 + 3140236560673929004944073455503301410784019919229762118770958528839039) / 1365430337030457401667605