Recurrence 4 lookup certificate: A4Square 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.recurrence4A4Square_coeff_70 : Polynomial.coeff recurrence4A4Square 70 = (121 * 10 ^ 70 + 1534643685817519413433339731003074014794538053102062300213004932093038) * 10 ^ 70 + 6227950585070902001303901505155087438073789219707008036104929522782558

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_71 : Polynomial.coeff recurrence4A4Square 71 = -((1402 * 10 ^ 70 + 846868475353084867545266195341901481367287691888685888565353370142222) * 10 ^ 70 + 6789606501061443759987784874581612625816908688300022652437053010996406)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_72 : Polynomial.coeff recurrence4A4Square 72 = (15698 * 10 ^ 70 + 4176882582775400738189851525001734291444210583608805700826298282204633) * 10 ^ 70 + 9699829461184653157267822790436347629251710004326739701168138824292494

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_73 : Polynomial.coeff recurrence4A4Square 73 = -((170129 * 10 ^ 70 + 2375706269731522003957751769832931112240464554743471261178567330394465) * 10 ^ 70 + 338236985506304565588556395169799914665534545096927764144324322715528)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_74 : Polynomial.coeff recurrence4A4Square 74 = (1785401 * 10 ^ 70 + 7602956900639606485236896879462828107609519892399576604616109022252701) * 10 ^ 70 + 3236785470417773427356119689266842492808924066032586329663729633943767

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_75 : Polynomial.coeff recurrence4A4Square 75 = -((18151555 * 10 ^ 70 + 5976489777653766258799973698277840510537522761421762218903601075861559) * 10 ^ 70 + 1505539790075715352403573488452531572956725396822757406927280271414730)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_76 : Polynomial.coeff recurrence4A4Square 76 = (178852190 * 10 ^ 70 + 3486976349903797013658556562002695074193471850961370272390381676579361) * 10 ^ 70 + 4063518924553775367789715744443862950018039914879529144765060157770245

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_77 : Polynomial.coeff recurrence4A4Square 77 = -((1708652270 * 10 ^ 70 + 3040379915703962603633780378201400038377969106502087706718510611287126) * 10 ^ 70 + 5174726702376328215921389764604103857056693787437073366803237205513856)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_78 : Polynomial.coeff recurrence4A4Square 78 = (15833015997 * 10 ^ 70 + 2208771919317759951038335429454001582267343039087090668264606733743423) * 10 ^ 70 + 9686171222479112293778196078787243458894387701901529842879324514910743

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_79 : Polynomial.coeff recurrence4A4Square 79 = -((142360951520 * 10 ^ 70 + 1037682921942781565147161531759412947747837096873916852161600032586555) * 10 ^ 70 + 4326926795962454191102499988762759618827734403993814493576077975132042)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_80 : Polynomial.coeff recurrence4A4Square 80 = (1242503099071 * 10 ^ 70 + 5919445767979660390912932799987673880692940117636878157401503929839940) * 10 ^ 70 + 6031143769036556598362498931326336109656133793323967099031654145413100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_81 : Polynomial.coeff recurrence4A4Square 81 = -((10530307798575 * 10 ^ 70 + 118293315350349261390068848860762242410939504442699563511340491671326) * 10 ^ 70 + 2089313794708357924325934723479250980326827949839142571924539933173392)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_82 : Polynomial.coeff recurrence4A4Square 82 = (86691182332666 * 10 ^ 70 + 8753058026025789890046191382373497766884754487679408250172486073983574) * 10 ^ 70 + 9830387345781753270134298270525753248786986646429515306959869360882927

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_83 : Polynomial.coeff recurrence4A4Square 83 = -((693502707678186 * 10 ^ 70 + 6280279621774109213121882412847176459488294522813557480167015671421725) * 10 ^ 70 + 6863285090688084811836651763965032419221219330241006821901421793668)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_84 : Polynomial.coeff recurrence4A4Square 84 = (5392694469944563 * 10 ^ 70 + 6635402414393251905250954501389097511454072779175547154611102846489448) * 10 ^ 70 + 3413339129855917221698125154564156746946015891364299357149512776040430

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_85 : Polynomial.coeff recurrence4A4Square 85 = -((40774534277927273 * 10 ^ 70 + 159485322033389681505779490973678323563860996870371613435433102379243) * 10 ^ 70 + 7012153169925902343808545227834669838800653788821559050009488679911012)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_86 : Polynomial.coeff recurrence4A4Square 86 = (299871409754196118 * 10 ^ 70 + 6693878651380710768307825709750314501715688895246687426180819473013644) * 10 ^ 70 + 3134060390140302952040838947050437191914906571167671777526163433890548

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_87 : Polynomial.coeff recurrence4A4Square 87 = -((2145742525425643424 * 10 ^ 70 + 9818294316546171879761937625558088101526774947241257208816002587627837) * 10 ^ 70 + 5684423937733157639096709132654025285183255477525222476988922493035918)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_88 : Polynomial.coeff recurrence4A4Square 88 = (14943306988411491839 * 10 ^ 70 + 5065099365752871229127728665694081332705200517212686283410157002276925) * 10 ^ 70 + 1916622040997604657083859537795700797952493585794931207965902629613688

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_89 : Polynomial.coeff recurrence4A4Square 89 = -((101313892370570571371 * 10 ^ 70 + 9406935964649570946702012689236325195845509701788762073305659210766718) * 10 ^ 70 + 1621569680117544807988028372383328065484794103150717653078820112425802)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_90 : Polynomial.coeff recurrence4A4Square 90 = (668910032938026433797 * 10 ^ 70 + 6506335478206286670907190716541127566644965694800418243887912978596440) * 10 ^ 70 + 9163976103701348193460214225346298091954281400669217311327471989964826

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_91 : Polynomial.coeff recurrence4A4Square 91 = -((4301925121105871829782 * 10 ^ 70 + 9399210851313506693258210906957746962772851971164064523342048339479673) * 10 ^ 70 + 9972846764348826979731535901862643665601865075121653409093271301013748)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_92 : Polynomial.coeff recurrence4A4Square 92 = (26956981160551674745347 * 10 ^ 70 + 466641364111463012284991554334250390955318710489934701553953035886681) * 10 ^ 70 + 5598574853509032395628159910914853024073583665354110741920399927808224

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_93 : Polynomial.coeff recurrence4A4Square 93 = -((164629141768510058510261 * 10 ^ 70 + 4793903945037670582852661840301217533681651175777424269109405145607626) * 10 ^ 70 + 2325634508809585502421664753932464893521585100140667376309507706285770)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_94 : Polynomial.coeff recurrence4A4Square 94 = (980121752978857754811432 * 10 ^ 70 + 3500599300892779756420644949984771474157427387205726046817059417931681) * 10 ^ 70 + 4211535798270469651148258094887096094641677319649162790442732274206597

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_95 : Polynomial.coeff recurrence4A4Square 95 = -((5689827652863679885945254 * 10 ^ 70 + 3167933395146337215288690643335084020196008028200477110216164280514842) * 10 ^ 70 + 2468078252546915455254442000373881174084190226353814803330565262844976)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_96 : Polynomial.coeff recurrence4A4Square 96 = (32215811277337237311843844 * 10 ^ 70 + 4544384870660888052076235498367384871983768264877503365300232343058265) * 10 ^ 70 + 7289204935790351519480513135884940434183831880685141760326447245730666

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_97 : Polynomial.coeff recurrence4A4Square 97 = -((177947663756419691664463046 * 10 ^ 70 + 8200342838805517126415062660011498561825506255885177158164830927403520) * 10 ^ 70 + 1568951455222745155631880992205612818763320901834422007247843281438292)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_98 : Polynomial.coeff recurrence4A4Square 98 = (959110166725786317278873333 * 10 ^ 70 + 6475262766791002041052505020389176244863687645515975433593191239615688) * 10 ^ 70 + 9382306035359777588131050468504053269079937568191683643040925570407578

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_99 : Polynomial.coeff recurrence4A4Square 99 = -((5045391080830939695602557225 * 10 ^ 70 + 4552384734110005118051034703235229462615239749199824638050778682802796) * 10 ^ 70 + 3947365961209768380924589062827247373535259313939128504373237115566818)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_100 : Polynomial.coeff recurrence4A4Square 100 = (25909913046638331367009347535 * 10 ^ 70 + 8704826708530155281229315849278656340676589534757083995206664887898385) * 10 ^ 70 + 4754524691449511534156014823273491857002417530116762226913215949720750

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_101 : Polynomial.coeff recurrence4A4Square 101 = -((129919416053747677098383990592 * 10 ^ 70 + 9404985505294396681169537513457893216556210786061038904389626240858255) * 10 ^ 70 + 840263524119473555113549016730842320564480928111737911078152132905848)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_102 : Polynomial.coeff recurrence4A4Square 102 = (636222433970374568701592777460 * 10 ^ 70 + 261187351745507664163221408026247826561237138649286899885697405972758) * 10 ^ 70 + 9096498070785464870491937717646782206839144847789847772156391826272737

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_103 : Polynomial.coeff recurrence4A4Square 103 = -((3043394365481115963301083020889 * 10 ^ 70 + 9334166646844306701140112239431733708694205694346153334184231108501964) * 10 ^ 70 + 3248520359909938824247406259190784306927046332641611756325713461071822)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_104 : Polynomial.coeff recurrence4A4Square 104 = (14223520093087037089623099725539 * 10 ^ 70 + 454839014346647140185129341550501197741576419837730130918258959246237) * 10 ^ 70 + 2074244388768023993068130334806321155226394582500140224670216857411420

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_105 : Polynomial.coeff recurrence4A4Square 105 = -((64958895709119057271518929948668 * 10 ^ 70 + 8601098700986306196583051670012188450339418107418678844703695556716974) * 10 ^ 70 + 4885554038231882574589020258885793324422862569161393936510188309985056)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_106 : Polynomial.coeff recurrence4A4Square 106 = (289957138678144205254735688749791 * 10 ^ 70 + 3523988757096910484111227632324694562362236220779103149338906933911924) * 10 ^ 70 + 9568597400461008167390618613336924486206611565989414111020967138363470

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_107 : Polynomial.coeff recurrence4A4Square 107 = -((1265235800257924475318266790682718 * 10 ^ 70 + 2497228147639392176600899078776115193506700955270351121935643138212349) * 10 ^ 70 + 4893129550026176167761077731683804256416842851400721506190387297079630)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_108 : Polynomial.coeff recurrence4A4Square 108 = (5397945189658800281095996618576143 * 10 ^ 70 + 9960408922834276068501033573248162738398476462231590948964629423323759) * 10 ^ 70 + 3695259826430974429620232997475042252126693820020929876839582288085811

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_109 : Polynomial.coeff recurrence4A4Square 109 = -((22520584706548924053422373420879169 * 10 ^ 70 + 9260187714136016322457034412908585540592182737598284798006976467284689) * 10 ^ 70 + 8552318285814049259918660770382029484040541222957567810395619056763656)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_110 : Polynomial.coeff recurrence4A4Square 110 = (91896290249053689272254020603020709 * 10 ^ 70 + 7103149783393714523857119901335759844177463418988078081507870652780650) * 10 ^ 70 + 9546829773304708395033580582233292527143087397853356476171674988515237

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_111 : Polynomial.coeff recurrence4A4Square 111 = -((366821241372714869281156667301802204 * 10 ^ 70 + 1675816251720345604092184593339380637619520997940841224732525975250828) * 10 ^ 70 + 8781013275540193953309086098113935240061036949924420752224222478702072)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_112 : Polynomial.coeff recurrence4A4Square 112 = (1432578301618874266950209517363219070 * 10 ^ 70 + 934795715173208127601434420521799699882224466860641898860959857524409) * 10 ^ 70 + 2579819086226853713881245524139812808083236650670400658534511452708194

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_113 : Polynomial.coeff recurrence4A4Square 113 = -((5474659131042137173370436277190642624 * 10 ^ 70 + 3023591744138561610157666907777316428712173013303524610418146315260378) * 10 ^ 70 + 2505938429830638909388999185505484976602664670297691306012130937118976)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_114 : Polynomial.coeff recurrence4A4Square 114 = (20475584050149818403307982618746170510 * 10 ^ 70 + 3089276401240169793151869811950838808651667539699020804878645639543301) * 10 ^ 70 + 2665653984143472165002148183438885142330236295853455226174547050410820

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_115 : Polynomial.coeff recurrence4A4Square 115 = -((74958343802990487650432096140980775471 * 10 ^ 70 + 5683855481720162239647891561164058876677059741754163275071380957709495) * 10 ^ 70 + 8614905763424966472315378382953908247107732268479304301081102669496870)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_116 : Polynomial.coeff recurrence4A4Square 116 = (268639849892015564157038053271085077549 * 10 ^ 70 + 8644250178332215565483864373169561736660702981104535550660967595408081) * 10 ^ 70 + 1984978756935689009608854996406666341766853454891657672289582119851134

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_117 : Polynomial.coeff recurrence4A4Square 117 = -((942645352370670324555443627562534231648 * 10 ^ 70 + 5332048660289219197585292274211173688555435361260238247838790212178377) * 10 ^ 70 + 4052791763041922898656711139627103356027414601991521194685072933945380)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_118 : Polynomial.coeff recurrence4A4Square 118 = (3239013385918346317421066688207094440012 * 10 ^ 70 + 440564053213499477324411766416186967504720076953546322214162045564477) * 10 ^ 70 + 3984219126005772870678449616636262027347162471129347515621656032380149

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_119 : Polynomial.coeff recurrence4A4Square 119 = -((10899866825679694014300868933026455625886 * 10 ^ 70 + 8861418549366717702198359648002757103026204829616676177201071494492391) * 10 ^ 70 + 6532649568166566290749394506731264075042405300052982755872265580967442)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_120 : Polynomial.coeff recurrence4A4Square 120 = (35927721266290084259409332230566357350755 * 10 ^ 70 + 3001022890082543232775308918695699050845773105471632363512187901290593) * 10 ^ 70 + 2845233871085974417870754404917811707317649341182273127264480806277595