Recurrence 4 lookup certificate: Scalar2Left 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.recurrence4Scalar2Left_coeff_433 :
Polynomial.coeff recurrence4Scalar2Left 433 = ((244857973921286128882791047080303530771 * 10 ^ 70 + 3643603392798810437252986679496734048858010057772849715353325830194864) * 10 ^ 70 + 9395858937915070980090858719875929318231044168839495529890638973222420) * 10 ^ 70 + 6729038284752113022364515775617409464301365046981242193379766290156991
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_434 :
Polynomial.coeff recurrence4Scalar2Left 434 = -(((108770027275399426401931260369832576951 * 10 ^ 70 + 7794409692855535966183875352406638918978071158230306279613641348905657) * 10 ^ 70 + 6756788542988497490839151479470168814201710536855365425445069261116929) * 10 ^ 70 + 7757105375398512780750885760083207342487537668949416552986384318005135)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_435 :
Polynomial.coeff recurrence4Scalar2Left 435 = ((36390089365785479015045692416453643188 * 10 ^ 70 + 5203193404579713167530785937493767479438911421446003944391027569201998) * 10 ^ 70 + 8013200759830146911646481728103773561740670762831064422718820414777731) * 10 ^ 70 + 1301400858588347946859237734126410242877584003897524894466070735865815
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_436 :
Polynomial.coeff recurrence4Scalar2Left 436 = -(((10507236258510291726465354828124268781 * 10 ^ 70 + 9813609142627558688552402465248899017650152840757730133417997049814357) * 10 ^ 70 + 2978064772845870887666273879365631326894019134778560063074046522373764) * 10 ^ 70 + 4184917650136564045947132037673979708994640088498778888533165401585322)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_437 :
Polynomial.coeff recurrence4Scalar2Left 437 = ((2737135914561965601530245204498934309 * 10 ^ 70 + 6069114745368280056603194150257405828735332427837133961473177687778165) * 10 ^ 70 + 6365364589371818807975571411588532249450668934717993222035795283301566) * 10 ^ 70 + 4028159804728396727755776541117140318114790117756266796868702020372776
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_438 :
Polynomial.coeff recurrence4Scalar2Left 438 = -(((655559400858226313292605653768815265 * 10 ^ 70 + 6584240500416062464586115892015282407245812007087094576608222394356411) * 10 ^ 70 + 2640344714142582777450063867315965697677439208120452267664510149405974) * 10 ^ 70 + 5718126615919028116101917078661384772569901608266819529674338711254728)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_439 :
Polynomial.coeff recurrence4Scalar2Left 439 = ((145602557772450920258604809693012914 * 10 ^ 70 + 3785761936534684596683724854693228271008685643331447660894433601089293) * 10 ^ 70 + 4484417602739051491499752511091749968018284986688255701683585275650117) * 10 ^ 70 + 1607711969635203654445830973928602158024267425013856999370232655445682
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_440 :
Polynomial.coeff recurrence4Scalar2Left 440 = -(((30086290218814662587956104952054903 * 10 ^ 70 + 8472928923867647910154310808342797944094540400219320298008743595138866) * 10 ^ 70 + 1065225915164592237756179201707785347083143732084687208222705837025378) * 10 ^ 70 + 6313938470544652389732480798014344772514853232930916891031657536189963)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_441 :
Polynomial.coeff recurrence4Scalar2Left 441 = ((5781568149269423938867536152279338 * 10 ^ 70 + 9517053505847482506066775326402202821613165756253861519898230680115625) * 10 ^ 70 + 9393154049144597425882689513141097184255466261240869561813668788092459) * 10 ^ 70 + 9496401147058651529138392397347984977286299249975386987304017642322771
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_442 :
Polynomial.coeff recurrence4Scalar2Left 442 = -(((1029489477725073053895473184963298 * 10 ^ 70 + 9362050127693988419486261080631317948663268985258898855234244945696371) * 10 ^ 70 + 6536150925415534719400142357445927083967826199541687736266366876742870) * 10 ^ 70 + 1983343180045386012335427625499806332718199052384007585415329188748461)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_443 :
Polynomial.coeff recurrence4Scalar2Left 443 = ((168572755922375647841859210333753 * 10 ^ 70 + 9340005217287166224867320989404283799961135146720986485246850865261696) * 10 ^ 70 + 3605765832426339526121382345334496189656984759433678812109078655477468) * 10 ^ 70 + 180455053055888267963263252995802819145765117585701591185117573711779
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_444 :
Polynomial.coeff recurrence4Scalar2Left 444 = -(((25029659532904333649476350978613 * 10 ^ 70 + 6105082933457370051527697800765194308349885493368970232542077465772712) * 10 ^ 70 + 1546399727006276437279945216674477137511167339567627959793132395226100) * 10 ^ 70 + 2712806076828690650239104859057542611392389234390456142336733269775958)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_445 :
Polynomial.coeff recurrence4Scalar2Left 445 = ((3280242475819258281657725471360 * 10 ^ 70 + 7580503205311419255083746137833385764612866073952295853819928814054520) * 10 ^ 70 + 607078538867935197666004973162096382372386818440769506441189170536224) * 10 ^ 70 + 3417823883751788969246719433100994645842926293458924378580230107334940
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_446 :
Polynomial.coeff recurrence4Scalar2Left 446 = -(((356874590095574098078731083728 * 10 ^ 70 + 4557062487353632587142892975537569828305994413190773987024144430328633) * 10 ^ 70 + 5650069375852594905093166104063286229673349209297271604829122665519641) * 10 ^ 70 + 7076200780895418976738683482114971460810650949733021311897675720134633)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_447 :
Polynomial.coeff recurrence4Scalar2Left 447 = ((26279921571167459537796825670 * 10 ^ 70 + 1606652562477943229816438703956620800692394292089258969884273971634424) * 10 ^ 70 + 6397510894983794900463026628264148512695362969329893985218938834522049) * 10 ^ 70 + 990934723888325887082010114926847034937052153226382874870772214274358
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_448 :
Polynomial.coeff recurrence4Scalar2Left 448 = ((479697964311174565542602172 * 10 ^ 70 + 3783199075403823121245281125732660615961365773001611976642666981630487) * 10 ^ 70 + 5865650271267530593793783947303778295145770774938881346550186339048380) * 10 ^ 70 + 8301917531988218879121367289189045667941937525379385991571543727814226
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_449 :
Polynomial.coeff recurrence4Scalar2Left 449 = -(((656133061299634177993419894 * 10 ^ 70 + 5998129961111324247985337496965544639163758595867185760066552991529269) * 10 ^ 70 + 3543626271952447749742211340569333698256188616538598843943105613592893) * 10 ^ 70 + 7061703571086828982643416240857540829226227197809589144567220299389826)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_450 :
Polynomial.coeff recurrence4Scalar2Left 450 = ((157092477577848120427454062 * 10 ^ 70 + 5950925936388784920134300102095054841997306471239060564537253971712701) * 10 ^ 70 + 4272577961086020118106026818386726962140050397098121026527860242629848) * 10 ^ 70 + 6379386569858144525108677654612142764097672359632789401735321053899079
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_451 :
Polynomial.coeff recurrence4Scalar2Left 451 = -(((26610476783237604383142834 * 10 ^ 70 + 5515186227201519897583964653594149397701584912897089389819745016297960) * 10 ^ 70 + 2149400182123046138500819174810753272788926362287555601204613770567912) * 10 ^ 70 + 5784729722155269302046665002485765146333027879102280812280780781973819)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_452 :
Polynomial.coeff recurrence4Scalar2Left 452 = ((3612475393548972481552048 * 10 ^ 70 + 9916843114746303110162741599273444653617152505518655143147570989788190) * 10 ^ 70 + 9579014829388419264149605702728359868237052351374944387278821835567224) * 10 ^ 70 + 469623625416580859464386312363742242815119416433516872242677839622349
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_453 :
Polynomial.coeff recurrence4Scalar2Left 453 = -(((396384754952312783774800 * 10 ^ 70 + 4618274370694882244088828074429688422839660610023959952526105213820141) * 10 ^ 70 + 8627596164662228843062398345563677858418736526846635185678394788002291) * 10 ^ 70 + 3446437198392789145611792014007400247142026920996702469299915286072566)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_454 :
Polynomial.coeff recurrence4Scalar2Left 454 = ((32535676168496441201324 * 10 ^ 70 + 4049914642448452502919929067074521138341269987498146854937110427728780) * 10 ^ 70 + 6291394334869141176716216704739663795280748599693237289484888318407901) * 10 ^ 70 + 4293772439239529811179545748398056848628282823326127653254694989822000
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_455 :
Polynomial.coeff recurrence4Scalar2Left 455 = -(((1255575505533262477172 * 10 ^ 70 + 6623718473261454583919643805723285003232442236896785155133777395676271) * 10 ^ 70 + 285212136123907910794827569350848986161065612049705809924721485176701) * 10 ^ 70 + 387827117920143179258904318883446408029543709852147571949931666209784)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_456 :
Polynomial.coeff recurrence4Scalar2Left 456 = -(((179836074289554000156 * 10 ^ 70 + 8509920584764508671944286705061279822853149731913236467018993449755644) * 10 ^ 70 + 2048442724796566060182923871992875217131204619551467898787089268169817) * 10 ^ 70 + 6000645207262154282708711193719045285459330036592415045362581949792323)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_457 :
Polynomial.coeff recurrence4Scalar2Left 457 = ((51600506174003621026 * 10 ^ 70 + 97512666465292667900290705596294933224156591739109683972724285791518) * 10 ^ 70 + 4433658588430544275991933254585261860579582992512403083835832932220250) * 10 ^ 70 + 3707307089734486246393512960211710745396505823837980989880224166647207
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_458 :
Polynomial.coeff recurrence4Scalar2Left 458 = -(((7776987944088435849 * 10 ^ 70 + 5103199646060860379370591437701642319658387429018190283861011501615568) * 10 ^ 70 + 5960932466954338464443942871415929026082288839177374573740926823940798) * 10 ^ 70 + 1695439751542229515043372721372109836847612582688408517892171973038657)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_459 :
Polynomial.coeff recurrence4Scalar2Left 459 = ((873518243253726487 * 10 ^ 70 + 4756829098503031195142832185527750842938340890203895541586222338386137) * 10 ^ 70 + 3727834088785353505412994375575879413400146680041620420813934836878107) * 10 ^ 70 + 9530835731746400678545619540041750243908483337504517139437848595532445
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_460 :
Polynomial.coeff recurrence4Scalar2Left 460 = -(((77176331542928346 * 10 ^ 70 + 1845022550509563754894219588692459401666768163588798819141349087803195) * 10 ^ 70 + 3388096902413920839788455458946719360873454334829910838331142195814649) * 10 ^ 70 + 3329691709835002211738849332038032685290773661357231744319978158676434)