Recurrence 4 lookup certificate: Scalar0Left 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.recurrence4Scalar0Left_coeff_394 :
Polynomial.coeff recurrence4Scalar0Left 394 = ((43982076148679491018658408521865738167413625899525649262513641 * 10 ^ 70 + 2982703374291418992981898298915703229856338472102245149499970983126274) * 10 ^ 70 + 4705670927219170061363099206243869537452506905578093355967961963962617) * 10 ^ 70 + 1748106982153931314637716531240048289220829020957002245515540873554873
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_395 :
Polynomial.coeff recurrence4Scalar0Left 395 = -(((19751284147636301144132524945351575647969082696185809499574822 * 10 ^ 70 + 8307769454350640430128543114154368588155267456392363267554230376868940) * 10 ^ 70 + 843438490039698962110055011187936057189227467340276891937606271877290) * 10 ^ 70 + 7292067596583379471249155506286412960738095967262855187349329857949232)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_396 :
Polynomial.coeff recurrence4Scalar0Left 396 = ((8187752860633531266325260009810006771204936501048493132207148 * 10 ^ 70 + 4679521266092559859816892952669941885649905015904949920799880651592559) * 10 ^ 70 + 188052622348819442154985787947642444179440420640728910208879617291780) * 10 ^ 70 + 4186893604368915095215105960565050549061859820518611240139834113807980
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_397 :
Polynomial.coeff recurrence4Scalar0Left 397 = -(((3198343860854018507195050294244942111456680909864733035347392 * 10 ^ 70 + 3971116473507612052760038302989709167396716071364093891228402037769708) * 10 ^ 70 + 5080231278438695345321248519233763118244770562818390478374925455186866) * 10 ^ 70 + 5941854713790418228107767802538271718233589855820935101544680277952463)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_398 :
Polynomial.coeff recurrence4Scalar0Left 398 = ((1189211810106404413746429159853900090823788194972702694902280 * 10 ^ 70 + 7771892780314862707248750271897430872534757493011529617988513517946670) * 10 ^ 70 + 6925558561025502657476366840114521500931406198389135533217837938468878) * 10 ^ 70 + 1093810014126297331941722907255638148760824613340308539243329020933224
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_399 :
Polynomial.coeff recurrence4Scalar0Left 399 = -(((422825847040416241243548572429874139103878918307565092996057 * 10 ^ 70 + 9218385544164640078921656758110772848200270107683510746941667143582495) * 10 ^ 70 + 9357138395889117145621892239036400707375583448197484152037302398758210) * 10 ^ 70 + 5039886412391883698004791072366614380486939850046539030836450372239900)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_400 :
Polynomial.coeff recurrence4Scalar0Left 400 = ((143900057795459888564740434704329015059234707263650851251734 * 10 ^ 70 + 2898993384782550030509260142757754206003814151104081589081491169468310) * 10 ^ 70 + 2982540008349724547346902623095981310998799970000675706522267822914060) * 10 ^ 70 + 8134511900908385284513874739287140000933776650154143283939149254220993
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_401 :
Polynomial.coeff recurrence4Scalar0Left 401 = -(((46779861763074126998602538756227875098661603652629015454294 * 10 ^ 70 + 7924102115541735991296816377009062606925812131267061187936647108443922) * 10 ^ 70 + 8324427508474226376286971916156287921667102969828274263580898943166032) * 10 ^ 70 + 3611993121336068570418096634228426745038220759027150798281169053298421)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_402 :
Polynomial.coeff recurrence4Scalar0Left 402 = ((14446058148060816263931403912567960819297650156954730274037 * 10 ^ 70 + 3289083732935294540149955335961623086022417713990128691809917841679816) * 10 ^ 70 + 6638559455935674356723069450012792258186735812319839793178325437762809) * 10 ^ 70 + 8080055770066946755600170235389606281364733366208960318212018356133741
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_403 :
Polynomial.coeff recurrence4Scalar0Left 403 = -(((4192370481042734285386473336190088546776753262901379659527 * 10 ^ 70 + 7324412234470827783043069608299576338027407864034548625492970091675398) * 10 ^ 70 + 1047834813505580827130873508111119894686441988895213706611831460851995) * 10 ^ 70 + 1261554174624262766367620982865386526752994877613158471234870522703076)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_404 :
Polynomial.coeff recurrence4Scalar0Left 404 = ((1119877513427549928831219895514466366005933503394013790244 * 10 ^ 70 + 8272111274293092755159372817651248357688960940200294924412825872423216) * 10 ^ 70 + 1043125782727214827987766170061338784591302894500654318867980399641941) * 10 ^ 70 + 9057942367375249839179894336539819669196877074019560168376454618618866
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_405 :
Polynomial.coeff recurrence4Scalar0Left 405 = -(((263142373992167143638194105940087640256831852241389981948 * 10 ^ 70 + 6407270613721980303589415397244277619621299974747244300993808264942093) * 10 ^ 70 + 9677349815581337376810360023786980589585375793497041071437751739464855) * 10 ^ 70 + 8114799420822273004034601435741789138906849197709096904209896255475742)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_406 :
Polynomial.coeff recurrence4Scalar0Left 406 = ((47652931152295610769356932514310286173608767101624165845 * 10 ^ 70 + 4766460942453117145992704518906278100959111987065778302661023573206568) * 10 ^ 70 + 4340786330382021953091399409204645372447539394449450618863945219379572) * 10 ^ 70 + 8969868143230336872938600900841611247038888436069218791037734371258924
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_407 :
Polynomial.coeff recurrence4Scalar0Left 407 = -(((2400891061326046862435565594969754911843792010739161250 * 10 ^ 70 + 4703659866397808879172297695382943424339916855238459910754834498998474) * 10 ^ 70 + 3967541086977319712624184336140520975209723290550602523582796946188668) * 10 ^ 70 + 140133214980563666757146812656470201422967855284161081068111069854890)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_408 :
Polynomial.coeff recurrence4Scalar0Left 408 = -(((3393181612745557108355429792833293028089791289789232701 * 10 ^ 70 + 5306744947662052220177638702706353062232264496201189552631462828227346) * 10 ^ 70 + 494102455270981553325911880262812515077052556677359944079922484744350) * 10 ^ 70 + 163645227593407843993335206191528011370260428177112999245330265180348)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_409 :
Polynomial.coeff recurrence4Scalar0Left 409 = ((2320304179845566052915249629956914154324977677973361018 * 10 ^ 70 + 1478833880317962934990257045951861918669485826025133111098543713738818) * 10 ^ 70 + 5877655443659886026295911687614228049489426943779432630008830073383642) * 10 ^ 70 + 8932284124608574328890428926394981112037696831236144179366683575674440
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_410 :
Polynomial.coeff recurrence4Scalar0Left 410 = -(((1070179458741956119732961747393114067458612624648038776 * 10 ^ 70 + 5225046669980917303828278796943742118517687814806613593093289850779720) * 10 ^ 70 + 8713719461270528725180137931783807654802365834384827315418229897693842) * 10 ^ 70 + 234488468870183940181597072184924971149773859473226229469523809894277)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_411 :
Polynomial.coeff recurrence4Scalar0Left 411 = ((415364408079554801722187452178826514771286308645507813 * 10 ^ 70 + 9711854718746183164506245187858427792650788409596137827803076907072324) * 10 ^ 70 + 731294915204524335439605126616800271517561019734996838680801661852346) * 10 ^ 70 + 6756920153885351952228493028825146640043416390260150463397465098209426
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_412 :
Polynomial.coeff recurrence4Scalar0Left 412 = -(((143424341468588634412110038653181232845810224566599556 * 10 ^ 70 + 1163574150284997830831070919787360233322042975260121033999131055009184) * 10 ^ 70 + 5379426125476168342614105258273245704222306412529333235726919987487826) * 10 ^ 70 + 4897136554970051448301156984576396344502704639633467724274608827664814)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_413 :
Polynomial.coeff recurrence4Scalar0Left 413 = ((44635644028222665258233750307627675305022953342304654 * 10 ^ 70 + 6131729174168181207672836995061328811862892382092251424375009832712148) * 10 ^ 70 + 2005737352641644575164029239124668797416254066970106897027185257190804) * 10 ^ 70 + 6444558541071649581069580076646586398850612736782363236082013133176405
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_414 :
Polynomial.coeff recurrence4Scalar0Left 414 = -(((12346096200983800780270677365890618500858762223546823 * 10 ^ 70 + 9727474763754635260194704552481072103839626322377958398883943994880708) * 10 ^ 70 + 5634611251596274279944872290093871978913503585460820339453028773863965) * 10 ^ 70 + 4776835694174413551493131613009687066672701268205184159765297759748846)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_415 :
Polynomial.coeff recurrence4Scalar0Left 415 = ((2857257732128003381842964707211956174896705981761852 * 10 ^ 70 + 8470335231639797036498358495151426748870053926786801145496437270767393) * 10 ^ 70 + 5761599499001674635850856755760381327942939830320510206095883528374435) * 10 ^ 70 + 6159397471915541330601449751397051972389933257966531086682206488513735
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_416 :
Polynomial.coeff recurrence4Scalar0Left 416 = -(((428210890559018278949118904090147140774155503321283 * 10 ^ 70 + 8863870700523675813294226482543831504632575626662897139513741865112849) * 10 ^ 70 + 8434385947025693293912787180753410584899596618044326161098388982977889) * 10 ^ 70 + 8759344197220307169621560217478141515794602328923718956679958648855533)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_417 :
Polynomial.coeff recurrence4Scalar0Left 417 = -(((54703378317517970253119678452185037624712872984940 * 10 ^ 70 + 4512896082805451677450448275614470925367432823662510567874280778069335) * 10 ^ 70 + 5289888491857268325866763461692732191578597049125237626133950140554536) * 10 ^ 70 + 8937794223903062401498081627570564337930987290557351924076310685888792)