Recurrence 5 lookup certificate: Scalar1First 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.recurrence5Scalar1First_coeff_337 :
Polynomial.coeff recurrence5Scalar1First 337 = (((134277475880703789983423465647404235972430883772655 * 10 ^ 70 + 3619506533416464134196776182670729330413737225674311520369358770303635) * 10 ^ 70 + 5383545788782460291468431552834942668786905319505359581211775300335563) * 10 ^ 70 + 5375314262739415743609079353444747053726519857279016752737270099694067) * 10 ^ 70 + 946890481648353028473794502116777522609906149918748586713095929874140
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_338 :
Polynomial.coeff recurrence5Scalar1First 338 = -((((51181656995983686257187786656969994052373199027298 * 10 ^ 70 + 538997499777823055889579790153437265453107621786431709314895968983809) * 10 ^ 70 + 4011896240281190120552320499807914957669571337067664772229769034711642) * 10 ^ 70 + 635474278329304939842040166858605813541933738966631311248035121057804) * 10 ^ 70 + 9795406921399760874976890219047035987289759226911705461557998161113494)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_339 :
Polynomial.coeff recurrence5Scalar1First 339 = (((19022225779819436911170683787226822088588210069184 * 10 ^ 70 + 7496594586991660890802427418974132222943470467539189049655883109347218) * 10 ^ 70 + 7480911993756048048832174461586812445365941467523720562635263659690427) * 10 ^ 70 + 2216775405468166672729610306451211819570383201026709359102623019800011) * 10 ^ 70 + 7258162304526445839248629983913238071442114323286790816741054815055192
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_340 :
Polynomial.coeff recurrence5Scalar1First 340 = -((((6883452557500582723732564944676818989093951778181 * 10 ^ 70 + 5657032636600749199852124307737144068477099504556454015633046844118692) * 10 ^ 70 + 5117067225858132954637184696627010527535577153171027574237457712135877) * 10 ^ 70 + 4416544275516020771304707240728394715298928790645002804101603712264506) * 10 ^ 70 + 3251924683934275618841176223568487984282264019483097734022878799554208)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_341 :
Polynomial.coeff recurrence5Scalar1First 341 = (((2421074148833925857422659988156205836192686640808 * 10 ^ 70 + 1784603394575772895137737748555366373670489690503213247162560611658704) * 10 ^ 70 + 2119282579684193720625426453795156147978470805439188053469501083992398) * 10 ^ 70 + 3830594260965522618122040831535218751040521652560116904610143260749049) * 10 ^ 70 + 3864674896681984893634730111372509120450759008579810057922455521220941
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_342 :
Polynomial.coeff recurrence5Scalar1First 342 = -((((825944425565597992098930904607766428868299321545 * 10 ^ 70 + 733189528547354830139275407838176948954742840428128570183382041773588) * 10 ^ 70 + 1028547987749073046498560053571672615441033336827442217637227552296258) * 10 ^ 70 + 7284258766074945329423516711788897692965505556543487778814394573952387) * 10 ^ 70 + 689004604461730531646532275917446939917015452224428280464100655408905)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_343 :
Polynomial.coeff recurrence5Scalar1First 343 = (((272545036432642248449913610808289642773797449502 * 10 ^ 70 + 865370856987828989846036895250000755163753049356770160039572838928567) * 10 ^ 70 + 337972831207735596340828402600158291492971634806442720564955364232804) * 10 ^ 70 + 2579179867141142484152510162728946487813638713885651117863198851394833) * 10 ^ 70 + 4736595085542054367186759989693590139972389955370914247338087892980378
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_344 :
Polynomial.coeff recurrence5Scalar1First 344 = -((((86661184692212155204028502130230097566969289006 * 10 ^ 70 + 1630249083388338078541856874236450002097159839599830615327175681543534) * 10 ^ 70 + 1630669677272325687397132917367333932231114016794979197417135914601469) * 10 ^ 70 + 6936591310056099576657167290696549971896891936028405106744373966345418) * 10 ^ 70 + 5603951305854609422419378116400471828264242843109526173307504789603518)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_345 :
Polynomial.coeff recurrence5Scalar1First 345 = (((26407261497637128038449579657451219442527432279 * 10 ^ 70 + 6376591980543771000189772903412168595373916633655788316329530427158109) * 10 ^ 70 + 4708849396461936422801134434457475958453650504391524416707974076659031) * 10 ^ 70 + 9300582864211048943589540356679161211176936852911223536987128113024127) * 10 ^ 70 + 4879512844947932907472196448820538586113623386240213899760171732066569
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_346 :
Polynomial.coeff recurrence5Scalar1First 346 = -((((7646465484935683696688790537602349436843957859 * 10 ^ 70 + 4151855299306168711621969688688416068361099585395414229629222318786260) * 10 ^ 70 + 1069580630455494734094943319870441014648343043352639290530354005946523) * 10 ^ 70 + 4490643886307613745357428485436996683243042791589491679979692195886283) * 10 ^ 70 + 9546268126221290491986464289528294876572000752931447883825765051068379)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_347 :
Polynomial.coeff recurrence5Scalar1First 347 = (((2074573246450945604634537189258961584375810611 * 10 ^ 70 + 3969442061365417166272669036150348664645371574590602643930246041620930) * 10 ^ 70 + 7519566362352653996939341856383540328965927825363059913470644561643418) * 10 ^ 70 + 8626497658061507378747306287392911920911553887078906546697979411503820) * 10 ^ 70 + 1900224423741073477245120285775562235120328840032596459880115611801897
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_348 :
Polynomial.coeff recurrence5Scalar1First 348 = -((((513781204995698839180337955999243617658072854 * 10 ^ 70 + 7819538941790539349725114682004592170472442150319357626595895210299743) * 10 ^ 70 + 1976981064034179192711864729886125332210634134049968737598143889179762) * 10 ^ 70 + 4777872001586915317594232978723929390218282655146291870125995816375993) * 10 ^ 70 + 6846746215443180906489602221944651731946605699693569699506934610012406)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_349 :
Polynomial.coeff recurrence5Scalar1First 349 = (((109573748602307036786157238495702273765348857 * 10 ^ 70 + 5819918268507981600196591229154183913778500294905252019514451545886045) * 10 ^ 70 + 6696512783056589515550347398210952671933173724134324540800218944980657) * 10 ^ 70 + 2338891285289348329984039855094920571975322020010943392268900003816029) * 10 ^ 70 + 7522117372922774921720353771749177303712763290512950255572618584575815
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_350 :
Polynomial.coeff recurrence5Scalar1First 350 = -((((16683141029293490434671094650622488690697787 * 10 ^ 70 + 9075554521073425155205705472534334997314225229604209581185199984309244) * 10 ^ 70 + 9256572346604440020415154222615816438494564691711364844757999957837190) * 10 ^ 70 + 8932010492685079934085859652140769719705256198492441338495307611666383) * 10 ^ 70 + 4163810391018881534533869455494732726218017035616413199012610930245320)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_351 :
Polynomial.coeff recurrence5Scalar1First 351 = -((((285381158898765464524698682941970779550486 * 10 ^ 70 + 3411723459850214469503767372984611159640983668217018087473681973098606) * 10 ^ 70 + 4465700453827370221787580129073673446382096299203348689721751470406729) * 10 ^ 70 + 433892024021289532968660396312605671433708171951154302961319160993835) * 10 ^ 70 + 7676541204125842616263983900582457661194109557648783529986182472896059)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_352 :
Polynomial.coeff recurrence5Scalar1First 352 = (((1620239258703696961420636505292678956453321 * 10 ^ 70 + 224410512095851648480244195841041442633648405622820912325465342548203) * 10 ^ 70 + 3607112184147362594914670818008480911149543814544348014449107740632189) * 10 ^ 70 + 4523431040185284135763129203297734193982880899982284141237733919051712) * 10 ^ 70 + 2511274082692528122272630987793262149351000172314095493173375353048606
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_353 :
Polynomial.coeff recurrence5Scalar1First 353 = -((((857975872361741276875270217544917342716543 * 10 ^ 70 + 2953978748912738946662900542447952548416887732825890018677693581557050) * 10 ^ 70 + 4873580916062880528051548353128309395109374804353357427038403373633731) * 10 ^ 70 + 4352608043446063292797513432500620233933436485080550883862364896924948) * 10 ^ 70 + 2200561231682852547946082427916967387949651275102065469616574187290803)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_354 :
Polynomial.coeff recurrence5Scalar1First 354 = (((315493911418897158506124639598713173903034 * 10 ^ 70 + 3578108274753542656979865107107565392487157752355215477459694609480164) * 10 ^ 70 + 4398381884409965878142976491646415536129011644051447011771643900291392) * 10 ^ 70 + 5969331921102474853663099531809527996090303924048922473501985746548688) * 10 ^ 70 + 1258123823299467369644085421839015411103134500377630507869378385009956
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_355 :
Polynomial.coeff recurrence5Scalar1First 355 = -((((86656042232116785260112546393807792931762 * 10 ^ 70 + 4206569531596472897099322676181994704968060155656614635098902042917944) * 10 ^ 70 + 7396573488281556877473248977324911783299132603295685570617208940933826) * 10 ^ 70 + 5417816251927091824064588683437580966322166181083712266105843075365335) * 10 ^ 70 + 9829622488406404915661425582652779479958710001746654654597182313724196)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_356 :
Polynomial.coeff recurrence5Scalar1First 356 = (((12883342075622462695642017686300498738565 * 10 ^ 70 + 7197094972842541988063449472112131878272301013744857565265548507881025) * 10 ^ 70 + 864359264930537452961937578202455400662396589662720106828287815460032) * 10 ^ 70 + 3730353906321693718488362486037561019522178899689712459396649581868905) * 10 ^ 70 + 2973770546818503553698797446220017260589872303173796503013319830231927
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_357 :
Polynomial.coeff recurrence5Scalar1First 357 = (((4241933652794903980038979094450014220593 * 10 ^ 70 + 2163435224571229535225300773454498710377064018408499717207783219422801) * 10 ^ 70 + 6771364965577479813656497936356397100893424249264190293254719052014155) * 10 ^ 70 + 1272597674836380473948313961960987191097556269930081090164452490888965) * 10 ^ 70 + 344503799991520410943711203355672348927669467870686820680853369184921
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_358 :
Polynomial.coeff recurrence5Scalar1First 358 = -((((5233193743665091234455612255090370122128 * 10 ^ 70 + 1367004040781512731249095944295443716126636292170939310063471214037893) * 10 ^ 70 + 7862677396366377086534295556823828465183670241371775928439247703695922) * 10 ^ 70 + 6484617160926687402606541131040325785728175929400970877302353922054689) * 10 ^ 70 + 766754216088821049102158274485064408614315684768408329111108647818009)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_359 :
Polynomial.coeff recurrence5Scalar1First 359 = (((3289068962024230959098481955407776983791 * 10 ^ 70 + 5336335151875595418485129371362758594999264560904118412968622955877713) * 10 ^ 70 + 1966620693372017335131728563354766036206037121814988051028142018296004) * 10 ^ 70 + 490043472110442200472945773671060391753285139444106806326239929577943) * 10 ^ 70 + 3725342654500459653473593773380910573157020242392783696540051055133448
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_360 :
Polynomial.coeff recurrence5Scalar1First 360 = -((((1677740149393132308235644522137431778020 * 10 ^ 70 + 1522513394891437571504097878192279330982576659837493088732436921148057) * 10 ^ 70 + 8302556817145714355499176844044493797528715180072091934620837955372960) * 10 ^ 70 + 1558443463001061975143244595920241695231403728842994540890724447987352) * 10 ^ 70 + 8235847140111399309065052068213838278925394403408499905591415657198312)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_361 :
Polynomial.coeff recurrence5Scalar1First 361 = (((765519012014617913715736388503784061595 * 10 ^ 70 + 2652507109252749923876217423705936300885773322830520135059971031838378) * 10 ^ 70 + 3987329848995108332372083760030307414471558795942816824133253015496247) * 10 ^ 70 + 523736812789229799828268069664022659423488713539531749238661365219228) * 10 ^ 70 + 9440445675039723015355747400611748810210290050779692527630058825882624
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_362 :
Polynomial.coeff recurrence5Scalar1First 362 = -((((324501231123546288074324545749941353150 * 10 ^ 70 + 538129153129808754553729545060449409816558984153392179871031459844753) * 10 ^ 70 + 1280273957656097472500102874426026259777953802755113796893790676470569) * 10 ^ 70 + 6667471773004062330649175952561075312606739326723731608148184054783607) * 10 ^ 70 + 974547247856922553475139552355469320269435791617390482411491069594476)