Recurrence 4 lookup certificate: Scalar0Exceptional 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.recurrence4Scalar0Exceptional_coeff_205 :
Polynomial.coeff recurrence4Scalar0Exceptional 205 = -((((145662205867588138312 * 10 ^ 70 + 1544889301289169765823629781738050253760271289555218006635878451569354) * 10 ^ 70 + 1221899074708020001449049699804100679624941698588205940072699331797112) * 10 ^ 70 + 1388030019857019694949956442444311220278916354206974301409248462726894) * 10 ^ 70 + 6041905232090805886146221266403166262858449404030623850417562151010940)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_206 :
Polynomial.coeff recurrence4Scalar0Exceptional 206 = (((300316798183546859976 * 10 ^ 70 + 1447826573402689158089466376318066702355062497729668689766181266069316) * 10 ^ 70 + 6849287098910939993083940627926539572386963880551069772371500978152469) * 10 ^ 70 + 6432410784127603146167105210304632856038166537483864605722665325528118) * 10 ^ 70 + 3130216012480299057628917380024321108168143186916027583288477154663002
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_207 :
Polynomial.coeff recurrence4Scalar0Exceptional 207 = -((((610495237946426500892 * 10 ^ 70 + 3125281117875702625327068860194119766097850107317147429493223124161830) * 10 ^ 70 + 5100473800356173676469577083285690387754962581826108435486964387878960) * 10 ^ 70 + 2252065927481122419385706007113677554244204187062047425318640091447772) * 10 ^ 70 + 8794739796285425561519222289990789343373015917645472995604279980344592)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_208 :
Polynomial.coeff recurrence4Scalar0Exceptional 208 = (((1223708679782179571334 * 10 ^ 70 + 849948553568883771002194197337958875027033733301870223615509710677896) * 10 ^ 70 + 6725783212932156447647286888284681260745514848922967797825242313195833) * 10 ^ 70 + 2845508130487300436519861505325920159376433666842969797031030008978701) * 10 ^ 70 + 5921799634073478786181368667882429103340561552522381515843686749283128
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_209 :
Polynomial.coeff recurrence4Scalar0Exceptional 209 = -((((2418740865742487112066 * 10 ^ 70 + 2032914584766447218250100871151962043879278484634054629109018718494012) * 10 ^ 70 + 2235957949021359183271549293060673022017073956740927616676216304857973) * 10 ^ 70 + 6063944475898432402404201698186377816708360731554982467454624844187843) * 10 ^ 70 + 9022735779462921356233002954712538008240181262834996408195015382602220)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_210 :
Polynomial.coeff recurrence4Scalar0Exceptional 210 = (((4714524504244204290364 * 10 ^ 70 + 8484509301051020707808611974524210381164818527752431982119421274922601) * 10 ^ 70 + 306304392094179321123595487899769037941213728630277961975210654108629) * 10 ^ 70 + 6439489821269248777825002720757761552266707975034425400908323390147039) * 10 ^ 70 + 7937083443286794750429959658178160565649007336470520147309067142509225
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_211 :
Polynomial.coeff recurrence4Scalar0Exceptional 211 = -((((9062431073655492206242 * 10 ^ 70 + 1595057773037042286899611582140052410468896549100399387591264287731551) * 10 ^ 70 + 7836739961522786181366755078653835584432885390639077345081830015610252) * 10 ^ 70 + 9599317890439430421195453912401533037089163637890056113211387771753653) * 10 ^ 70 + 9917877617712551719218150985014749012770790662971732758717591624808063)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_212 :
Polynomial.coeff recurrence4Scalar0Exceptional 212 = (((17180275877190132745313 * 10 ^ 70 + 3573046100639951875639614401729517327228398769297267633655200138193473) * 10 ^ 70 + 8901625435908936356358276750702917384969121639420742151642761869112362) * 10 ^ 70 + 3378721511777084005262163382320528130626961058011733019626214916276315) * 10 ^ 70 + 3873098727353738616448997370856742371077731589859904973456681382494343
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_213 :
Polynomial.coeff recurrence4Scalar0Exceptional 213 = -((((32122832065073475073777 * 10 ^ 70 + 3259111534376489215494205552897180985732569235184680108675287512091173) * 10 ^ 70 + 452305966282153293076751040638627392662046187420527118356759607689557) * 10 ^ 70 + 3554712745958686463328013813027695547115396344978566290015250811697563) * 10 ^ 70 + 6932969232212478972321717267123915955639273381339046417532144153180308)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_214 :
Polynomial.coeff recurrence4Scalar0Exceptional 214 = (((59239971884404161901093 * 10 ^ 70 + 6686278345702904593620581153629978104633430311161517694360305654222058) * 10 ^ 70 + 1063493012704740694661054584390723189392857682764243495512766271044346) * 10 ^ 70 + 6181380225717528590161027353693175609844694900876418757767401279579408) * 10 ^ 70 + 5064399083117597215480885344568362889914160780771914165447929841424271
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_215 :
Polynomial.coeff recurrence4Scalar0Exceptional 215 = -((((107758519059204361154312 * 10 ^ 70 + 8335396573673357364081983397829030611135961568461866174719160249364647) * 10 ^ 70 + 282761001302744932810118718205475543778674749786313029677007762509683) * 10 ^ 70 + 2268302850321342125996322449765980597858578431990571504275542079447009) * 10 ^ 70 + 5395760141489649059090345258852299489622161399096487030341807407447990)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_216 :
Polynomial.coeff recurrence4Scalar0Exceptional 216 = (((193349019626962177810083 * 10 ^ 70 + 1272287687823218929747147306885998687208498346564764283435931261713155) * 10 ^ 70 + 593393876238223936061753781010855545791780591078157604334078116679007) * 10 ^ 70 + 4976140669437695276621909033177926338273055062380008749022221607228514) * 10 ^ 70 + 6721706591774358320376624882671794614082467561501863545118447569053144
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_217 :
Polynomial.coeff recurrence4Scalar0Exceptional 217 = -((((342218262046801429711379 * 10 ^ 70 + 2453112606667863841166231073345999667137343905567243670713648763600433) * 10 ^ 70 + 4724191419671727373112773004513090649501821658552325196846999840463140) * 10 ^ 70 + 1557007479446865269172228278672812052398214515494744190063661166441727) * 10 ^ 70 + 2683069919865651516279674394683682289021995204780135180939418521413159)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_218 :
Polynomial.coeff recurrence4Scalar0Exceptional 218 = (((597519289990889381084091 * 10 ^ 70 + 8507535535030519810310316572581339289488171942694621735788352020714654) * 10 ^ 70 + 1194519140001285817348173317176284010555818993472731949769585327545482) * 10 ^ 70 + 3064680043033628263183144689145039326338947157157304757088319247278849) * 10 ^ 70 + 2851859680316178692503839075862703420994320829565713988855460142775547
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_219 :
Polynomial.coeff recurrence4Scalar0Exceptional 219 = -((((1029210881588230251631279 * 10 ^ 70 + 4442754598375687241802257229390810160720143622219707088222339892619262) * 10 ^ 70 + 6198772456183622853575818934884511164693635110797276708029383870067806) * 10 ^ 70 + 6813277603584276479011385879339846687399861633771843228056062291625203) * 10 ^ 70 + 5756520495224724188199736271070980424441382792112939591003525516048788)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_220 :
Polynomial.coeff recurrence4Scalar0Exceptional 220 = (((1748944843764138378861252 * 10 ^ 70 + 1017131119299561982821524289230662075762171388114034967772966188272798) * 10 ^ 70 + 8215138099984065006155832014744192077831391727258844561206355605939497) * 10 ^ 70 + 1200508104318448215236888820347254199493707922370081202557385636420854) * 10 ^ 70 + 8185841821396922699316522838385441986967781678428148446263154068626906
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_221 :
Polynomial.coeff recurrence4Scalar0Exceptional 221 = -((((2932123503316514134197643 * 10 ^ 70 + 1868879111684935747086698927721899191838686321480532098196539242127774) * 10 ^ 70 + 3248014442059231890156860096304625463627112539711916194066635049269261) * 10 ^ 70 + 5053899537351217765705311803396665381613105340216371813786304837049835) * 10 ^ 70 + 9566424341063947279900371831560481928975993384819462988511804587983728)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_222 :
Polynomial.coeff recurrence4Scalar0Exceptional 222 = (((4849951510471557501658122 * 10 ^ 70 + 418584546241052158056869758524358158525145869334608770580680100327132) * 10 ^ 70 + 1860904814285606106110775731208239013150547564844273661867168877153862) * 10 ^ 70 + 1339901204248123167300041572269748492950094349848752912149885371588153) * 10 ^ 70 + 6706627288400944158556087379802749126044827148601024000712399119551182
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_223 :
Polynomial.coeff recurrence4Scalar0Exceptional 223 = -((((7915085697569532038145749 * 10 ^ 70 + 3653199698729850341036965382693665803865007884634446224100151457355729) * 10 ^ 70 + 350763808588096050949340800960073855672818834631614959776473098314499) * 10 ^ 70 + 361291387749572402907705220814640410810243548112020328332178541245635) * 10 ^ 70 + 389283906428889538376128824317479156329343418011500409235441576331162)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_224 :
Polynomial.coeff recurrence4Scalar0Exceptional 224 = (((12745314207245562381171801 * 10 ^ 70 + 7387378880551148670618580986476676301028293131308501061743150618217192) * 10 ^ 70 + 6178453985616415655814923399330556146792850379382736883319475329768062) * 10 ^ 70 + 6292817288529494506544039215294935038682940490409284835691036756713487) * 10 ^ 70 + 3194193128080313100439236743194597791668288048719536043856824122873972
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_225 :
Polynomial.coeff recurrence4Scalar0Exceptional 225 = -((((20250479573652379668568648 * 10 ^ 70 + 8230130452994135838430409480195742018920365356430194420351499282727634) * 10 ^ 70 + 4883400165117278334163750977559295738019454022802743439444221290511995) * 10 ^ 70 + 3277916200033344455634406110637167305820367954726645831284581568277145) * 10 ^ 70 + 9705393780953817007063741977505462064113129608169406274390954084632909)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_226 :
Polynomial.coeff recurrence4Scalar0Exceptional 226 = (((31748455213473260906110695 * 10 ^ 70 + 8592931292013784429348212409932561867226825676386022537713310898654689) * 10 ^ 70 + 1423432156139021828306597959433208518305773614324726854699213989918284) * 10 ^ 70 + 6713984421170240607356809655297707162789217337252797123883036434836190) * 10 ^ 70 + 8923942645028613352583701613711796930364997623786432079362070792294095