Recurrence 5 lookup certificate: LeadingSquare 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.recurrence5LeadingSquare_coeff_122 : Polynomial.coeff recurrence5LeadingSquare 122 = ((129605067626788106107562152276019148226072608 * 10 ^ 70 + 7676376028443077097060740611827341112563815100152568697543265171197199) * 10 ^ 70 + 2633281363091429749048920443630583113699249522646834430338093456295880) * 10 ^ 70 + 3538920543841765990015925494498312460747858639286009167203655361163341

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_123 : Polynomial.coeff recurrence5LeadingSquare 123 = -(((148394186326300445355052758581293045441520315 * 10 ^ 70 + 253518052309560306038851650087001002422366357201215321972013012411809) * 10 ^ 70 + 3311305095894211724255004797497941689114855753930684686184864353020756) * 10 ^ 70 + 1987885948337511618124958026173761192625534956401510869340483122147956)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_124 : Polynomial.coeff recurrence5LeadingSquare 124 = ((165322828932800719419908433389757231511455154 * 10 ^ 70 + 7277979564491780208709525763363614360544877633071240325927325874641536) * 10 ^ 70 + 9904732679301193597184063115984002300783933462012498896912688424598227) * 10 ^ 70 + 4854966403584294367168274184887166870579420525092089373989999147911909

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_125 : Polynomial.coeff recurrence5LeadingSquare 125 = -(((179223957370904624858044348960621748345526483 * 10 ^ 70 + 1240743821660776594111647294539243425089123274230074327730048325112856) * 10 ^ 70 + 9423149059279135898596449172290653346117649353366399152734537774563032) * 10 ^ 70 + 8968232696076246114912320972973693418341336197257092611405695722697264)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_126 : Polynomial.coeff recurrence5LeadingSquare 126 = ((189072478706326840920165007372457749190317576 * 10 ^ 70 + 8769669509786894868092993238389288023841138653370291818144708079528432) * 10 ^ 70 + 776186475654818970677317166253924559124260737041126270313188946386241) * 10 ^ 70 + 7300089961096289977412648542762340880096269644834786691002483085913082

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_127 : Polynomial.coeff recurrence5LeadingSquare 127 = -(((194109159518572843180370639572637599150504418 * 10 ^ 70 + 9912277232775313605730415336928765619788961822833471276483994434437589) * 10 ^ 70 + 1471443642680610009185555868129775212730696995338228319312751843650221) * 10 ^ 70 + 278875185850803316769124531115917684592831842885857514805901692446732)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_128 : Polynomial.coeff recurrence5LeadingSquare 128 = ((193936375152811637472379457785821470842350516 * 10 ^ 70 + 1744274028937728711163269932103326316974134762976355500054008119719478) * 10 ^ 70 + 5686003928844077784752879388706213154565471973966000587633479281485160) * 10 ^ 70 + 5958804828967494204840734460447105802912926220818059379571336014988185

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_129 : Polynomial.coeff recurrence5LeadingSquare 129 = -(((188568995755303370900338030615713775130612195 * 10 ^ 70 + 2720181895655325768083489268139910408259142100161962615081661696948602) * 10 ^ 70 + 2000943571873341902590135780111409021428194033630342199865548867080583) * 10 ^ 70 + 832300016433431714541526972985584933836193586984705198814193775094600)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_130 : Polynomial.coeff recurrence5LeadingSquare 130 = ((178431450456711028079890014897546537035556942 * 10 ^ 70 + 481282588196120926641215260356617829286827694399768957643750507705000) * 10 ^ 70 + 292368530599372900264533569928200917058403763583085621499550347313906) * 10 ^ 70 + 4053736591666946328132959063184438065430947147914881344923021977206058

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_131 : Polynomial.coeff recurrence5LeadingSquare 131 = -(((164301755334427459149416738679885271663304998 * 10 ^ 70 + 5065238531171136287667471651816707393862678231633712507894160178329977) * 10 ^ 70 + 4143570274491215128054211574179644066064146779806865287516058665869186) * 10 ^ 70 + 9930877885431294412875280662419639981027541615741555948788192957989920)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_132 : Polynomial.coeff recurrence5LeadingSquare 132 = ((147212790908979379553585113935161185762993643 * 10 ^ 70 + 7572904819065102169987599999199733426634015946634278958709710777653294) * 10 ^ 70 + 9581064879961425556773111457245605988331900249844382701808583512382182) * 10 ^ 70 + 4878421557109082623303222212629093254898042020259549009532055821453375

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_133 : Polynomial.coeff recurrence5LeadingSquare 133 = -(((128328206930385291172546479106243747159647173 * 10 ^ 70 + 7365403329788083835824761751686936904778358522873202023649522243153731) * 10 ^ 70 + 3060868177387138020808599185568298017179447130116329768325471380636306) * 10 ^ 70 + 8785397768954599648915872615226718027101068611256865577168947618872200)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_134 : Polynomial.coeff recurrence5LeadingSquare 134 = ((108813532911996842710851896283024036138906863 * 10 ^ 70 + 1908212318369778636653881203071921385123256738872649093970685567488706) * 10 ^ 70 + 6010366394285168384858711137034524101520719568889007884420161115222630) * 10 ^ 70 + 7969064180984958753912395734873916360716589183323987421401041896255347

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_135 : Polynomial.coeff recurrence5LeadingSquare 135 = -(((89721951345247897599812436896625827747861920 * 10 ^ 70 + 4584475349735587596198729212899914611777058441216126520755176384103298) * 10 ^ 70 + 682916949714791914457141709254582925272816904651260821292380409429203) * 10 ^ 70 + 1577675907770070428379894603786886181742319184448575400386447173947920)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_136 : Polynomial.coeff recurrence5LeadingSquare 136 = ((71909407668202025034229712025628780809350618 * 10 ^ 70 + 1279608096058988906833493680449286290314397051586280411941285678687022) * 10 ^ 70 + 8051494605871567313071445052326139753917983563447960323203244455619373) * 10 ^ 70 + 477827140101822191096004654923475943260661637328378754594639775353233

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_137 : Polynomial.coeff recurrence5LeadingSquare 137 = -(((55986758871640287973985593491015254385395844 * 10 ^ 70 + 2429239121144579988776319408076955341496691636915017713435916275794214) * 10 ^ 70 + 563340805274718385429890275540143398410492379670391176459501665246360) * 10 ^ 70 + 6767776004846578651467845914677350492683343820302940372963341854363782)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_138 : Polynomial.coeff recurrence5LeadingSquare 138 = ((42309301207394749114526225466292865916892849 * 10 ^ 70 + 101621279959584846499808996071167271573156043011438950461413870244129) * 10 ^ 70 + 7612124349662134454843324380932741587325466359882348370057818980080224) * 10 ^ 70 + 7494140422973452506830098496047281908825704505507922976366980533026342

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_139 : Polynomial.coeff recurrence5LeadingSquare 139 = -(((30997881964934048676657399555357055207678595 * 10 ^ 70 + 8239826179847636561805966845068809821893824655947454644954368506551599) * 10 ^ 70 + 7040867123490159071725597411840490853593486008573294944983969524407062) * 10 ^ 70 + 4988589589924008452634241890900576119937879288857778426868883175126548)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_140 : Polynomial.coeff recurrence5LeadingSquare 140 = ((21981937796973889427095325194097530639211753 * 10 ^ 70 + 9510737895223571344908245942987315637374955216255004094968480100855757) * 10 ^ 70 + 5591006090591881983747356606829846200220412055044511352076969174598560) * 10 ^ 70 + 746579319505646915258902279667005582007324362515255007214987688511401

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_141 : Polynomial.coeff recurrence5LeadingSquare 141 = -(((15053532347131435926860320606854433761880355 * 10 ^ 70 + 951396057828333688833810422675492863224556459099984697882729191307882) * 10 ^ 70 + 5926073483369839671533880122591318741201444168888298697571115609221265) * 10 ^ 70 + 1292071535157148852265635837159133901095292567049612004358642873457104)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_142 : Polynomial.coeff recurrence5LeadingSquare 142 = ((9922452112511361394064969939919745837724322 * 10 ^ 70 + 7306249313504241096210465224571164366526989737201475678795112665945457) * 10 ^ 70 + 1620176886880381533460699923491827894824655950159511200150705566157147) * 10 ^ 70 + 5464938119936842862613003091140585797449888148689420948842663428446797

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_143 : Polynomial.coeff recurrence5LeadingSquare 143 = -(((6264901188806242284326216059749335027655291 * 10 ^ 70 + 3350548301839257568678009830764725575791777842272671978429440625634099) * 10 ^ 70 + 844619017470742288832445342004331887809004251517996101345455778115097) * 10 ^ 70 + 6001487849348893764128165764213146197919648744072597542532220045898756)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_144 : Polynomial.coeff recurrence5LeadingSquare 144 = ((3761420114917036626777584184704034509450106 * 10 ^ 70 + 9030332881629408941794513542877104134705039041970348397995744257983270) * 10 ^ 70 + 7111238060878443179657594256125752257791408834831149128949909281246258) * 10 ^ 70 + 4964501464103047362421754151927561707236778843077888609543639376096590

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_145 : Polynomial.coeff recurrence5LeadingSquare 145 = -(((2122567813219978507314431464354260935725732 * 10 ^ 70 + 3413664143074393093989838859611505704775486083277336260818915489622298) * 10 ^ 70 + 2343606714743642396877058805017621232040360225284885019415947625839318) * 10 ^ 70 + 7743030247940050343228520425225709028399872080995237600590010830443564)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_146 : Polynomial.coeff recurrence5LeadingSquare 146 = ((1103144369398619933525397511230423169127795 * 10 ^ 70 + 9956160280854195536878011474694707449414010463023940610863450221667810) * 10 ^ 70 + 7705440554808905369357022038625173636374420653762615286166044708686674) * 10 ^ 70 + 8895455768574452082622402531362085926188445691891726031821819279749295

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_147 : Polynomial.coeff recurrence5LeadingSquare 147 = -(((507096888130376186472648894450376749314160 * 10 ^ 70 + 3395083354113912558006391155484098016453406664902858665526759887975145) * 10 ^ 70 + 2753372328177790247853992483426907121101691636060468112950640939296032) * 10 ^ 70 + 6824713142701729956427227272489923407095304048060195519926984517263312)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_148 : Polynomial.coeff recurrence5LeadingSquare 148 = ((185792457761665591250443886146675305651750 * 10 ^ 70 + 8618332169105016798746462321291580837832229245592361254357091502762711) * 10 ^ 70 + 474090707279551113410846110194603747309073082949948039834006466245012) * 10 ^ 70 + 1254304630593849434664299979804870875689489489593418647573966245195460

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_149 : Polynomial.coeff recurrence5LeadingSquare 149 = -(((32263812902917402340912468344450399102860 * 10 ^ 70 + 4234399182417490502956560691486885277625761598651009517386910114690764) * 10 ^ 70 + 6909764155741976059666681405797412516304855172088414341011818964508437) * 10 ^ 70 + 1655878883902033984481264719631892750549640606981189431842897391379520)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_150 : Polynomial.coeff recurrence5LeadingSquare 150 = -(((26414282384498192251138504142062701182595 * 10 ^ 70 + 9535729430341391413863857752384152444020798755394890714578939715884225) * 10 ^ 70 + 2120609717889678342196324157731070274602605973343865790643654288086536) * 10 ^ 70 + 1890663757485069017482358957924363661281645706464889378212290519359155)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_151 : Polynomial.coeff recurrence5LeadingSquare 151 = ((37052426003333889416293611867356182891226 * 10 ^ 70 + 7697909268118925606142838482208925683958096113199184767901654141207600) * 10 ^ 70 + 5402791024502216258427456115974459648285688409835608474004711553088722) * 10 ^ 70 + 2515133273350348577944374482720375490885689459809515013861751397177984

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_152 : Polynomial.coeff recurrence5LeadingSquare 152 = -(((27591042294336266798017982824834856359882 * 10 ^ 70 + 147151944899741535648400062861038517692718324178825825926804249429951) * 10 ^ 70 + 3004835516927124906629991813266598361988637317615239423375025686617615) * 10 ^ 70 + 4949946012514417841237858219864141256025821431810263714384306639556064)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_153 : Polynomial.coeff recurrence5LeadingSquare 153 = ((13153206931570719592663862059260795466841 * 10 ^ 70 + 2462402709099151483918093780921885087321968484013605838385738024044235) * 10 ^ 70 + 3914593298741410758816393166590578169971788107144156934679979775144133) * 10 ^ 70 + 8494142587837344017080764363380153528933934024521168083520964738223778

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_154 : Polynomial.coeff recurrence5LeadingSquare 154 = -(((744643345152276387811968634684404506317 * 10 ^ 70 + 7571611734216853639206587369078457895630682691497372617700524014930200) * 10 ^ 70 + 4587536951537413428345249310084125807420837886400370667540516373764787) * 10 ^ 70 + 9405619738679565040399531318272512397743468357137536509111343168875087)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_155 : Polynomial.coeff recurrence5LeadingSquare 155 = -(((7336739104398618569439480662683547387135 * 10 ^ 70 + 7110016722873097953764797406804327056795760121388080574771242957799447) * 10 ^ 70 + 9286377599716706569291600309453947954918140162700648402107895963577935) * 10 ^ 70 + 112629252865083335012828461117872979727330771584781615342144200051554)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_156 : Polynomial.coeff recurrence5LeadingSquare 156 = ((11196388882370625535179499330092978495252 * 10 ^ 70 + 2781570704897720685441144224790637233867038047933609253428000868868002) * 10 ^ 70 + 7001530783834971526887044053651486048323362101841494445671526964666099) * 10 ^ 70 + 777876047426249867533758775995269197509432824762989643017017482276455

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_157 : Polynomial.coeff recurrence5LeadingSquare 157 = -(((11908587128675596295027181324487037892638 * 10 ^ 70 + 959795552857866653483379738766458558053220988130852734815415881706191) * 10 ^ 70 + 9885212434275054061503584503358195070271426750672183685759173906257499) * 10 ^ 70 + 4882063331552636807532209198849962111327681752569137292395945026573166)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_158 : Polynomial.coeff recurrence5LeadingSquare 158 = ((10715547922557629161707611747738648215031 * 10 ^ 70 + 773583484781037681528613973877169942805832550674416553716984953597943) * 10 ^ 70 + 9535832487872205554638593953946638808474672092181678688078288495722095) * 10 ^ 70 + 7487966323029723598087465036211429232178307876218512332033091028636702

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_159 : Polynomial.coeff recurrence5LeadingSquare 159 = -(((8651571969695396303885732432255766503670 * 10 ^ 70 + 2645572467563829294780877692347509200748357996456706847619836796006494) * 10 ^ 70 + 9248424293740024258677375736472943325502740662983207538831582555566115) * 10 ^ 70 + 7015624977682508465095547413606660564939373462659206435011993211146334)