{"certification":{"candidate":{"gauge":{"kind":"none"},"index_shift":0,"operator":{"intercept":"1","shape":"affine","slope":"1"},"parent":{"first_index":0,"initial_polynomials":[["1"],["2","2"],["3","8","3"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["3","3"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["-3","-6","-3"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["1","3","3","1"]]},"deriv_order":0,"offset":3,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent_name":"Triangle read by rows: T(n, k) = (n-k+1)*(k+1)*binomial(n, k)."},"identifying_rows":3,"identity":{"certificate":{"certificate":{"dividend_relation":{"terms":[{"coeff":{"coeffs":[["4","8","4"],["5","10","5"],["1","2","1"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-2","-2"],["-8","-8"],["-2","-2"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["0"],["3"],["1"]]},"deriv_order":0,"shift":2}]},"exceptional_bases":[],"gauge":{"kind":"none"},"identifying_indices":[0,1,2],"index_shift":0,"input":{"first_index":0,"initial_polynomials":[["1"],["4","2"],["14","14","3"]],"recurrence":{"denominator":{"coeffs":[["-2"],["-1"],["1"]]},"terms":[{"coeff":{"coeffs":[["8","8","2"],["-4","-4","-1"],["-4","-4","-1"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["-12","-6"],["0","0"],["4","2"]]},"deriv_order":0,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"input_valid_from_base":1,"multiplier":["1"],"operator":{"intercept":"1","shape":"affine","slope":"1"},"parent":{"first_index":0,"initial_polynomials":[["1"],["2","2"],["3","8","3"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["3","3"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["-3","-6","-3"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["1","3","3","1"]]},"deriv_order":0,"offset":3,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent_leader_shift":3,"parent_valid_from_base":0,"quotients":[],"row_annihilation":{"kind":"system","system":{"generators":[{"annihilator":{"terms":[{"coeff":{"coeffs":[["-6","-16","-6","0"],["7","8","-2","-2"],["-7","2","-2","0"],["6","0","0","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-12","0","-2","6","2"],["20","-6","0","2","0"],["-12","-6","0","0","0"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["-1","4","5"],["6","6","0"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["2"]]},"deriv_order":0,"shift":2}]},"quotient":[{"coeff":{"coeffs":[["0","0","0","0","0","0","0"],["6","36","90","120","90","36","6"],["14","72","162","208","162","72","14"],["10","56","140","188","140","56","10"],["2","24","68","92","68","24","2"],["0","4","18","28","18","4","0"],["0","0","2","4","2","0","0"]]},"deriv_order":0}],"step_multiplier":{"coeffs":[["16","192","1056","3520","7920","12672","14784","12672","7920","3520","1056","192","16"],["64","704","3584","11200","24000","37248","43008","37248","24000","11200","3584","704","64"],["96","1024","5152","16128","34848","54528","63168","54528","34848","16128","5152","1024","96"],["64","768","4224","14016","31296","49728","57856","49728","31296","14016","4224","768","64"],["16","320","2144","7872","18688","30784","36256","30784","18688","7872","2144","320","16"],["0","64","640","2880","7616","13184","15744","13184","7616","2880","640","64","0"],["0","0","96","640","2016","3840","4736","3840","2016","640","96","0","0"],["0","0","0","64","320","704","896","704","320","64","0","0","0"],["0","0","0","0","16","64","96","64","16","0","0","0","0"]]},"step_quotients":[[{"coeff":{"coeffs":[["48","624","3744","13728","34320","61776","82368","82368","61776","34320","13728","3744","624","48"],["192","2304","12864","44352","105600","183744","240768","240768","183744","105600","44352","12864","2304","192"],["288","3360","18528","63840","152928","268128","353088","353088","268128","152928","63840","18528","3360","288"],["192","2496","14976","54720","135936","243072","322752","322752","243072","135936","54720","14976","2496","192"],["48","1008","7392","30048","79680","148416","201120","201120","148416","79680","30048","7392","1008","48"],["0","192","2112","10560","31488","62400","86784","86784","62400","31488","10560","2112","192","0"],["0","0","288","2208","7968","17568","25728","25728","17568","7968","2208","288","0","0"],["0","0","0","192","1152","3072","4800","4800","3072","1152","192","0","0","0"],["0","0","0","0","48","240","480","480","240","48","0","0","0","0"]]},"deriv_order":0}],[{"coeff":{"coeffs":[["-48","-720","-5024","-21616","-64080","-138512","-225280","-280368","-268752","-198000","-110880","-46160","-13744","-2736","-320","-16"],["-104","-1536","-10688","-46448","-140856","-315328","-537392","-708336","-725976","-576512","-350304","-159056","-51848","-11328","-1456","-80"],["152","1392","4288","-1888","-58168","-225616","-512272","-804192","-924504","-795952","-514848","-246944","-85000","-19696","-2704","-160"],["736","7840","37616","105216","180736","163936","-37440","-369888","-629216","-649440","-462800","-233600","-82304","-19232","-2656","-160"],["1024","11344","58224","181008","373040","519712","461600","176832","-151728","-313888","-273488","-148928","-53088","-11920","-1504","-80"],["728","9024","50560","169200","375776","578272","616624","426688","135840","-64544","-108368","-66784","-23688","-4864","-496","-16"],["280","4432","28384","103872","247008","403360","459504","356896","169440","23968","-27600","-21728","-7368","-1232","-80","0"],["48","1312","10544","43936","113296","195296","231680","187296","96304","23648","-4144","-5120","-1520","-160","0","0"],["0","192","2448","12608","36576","67312","82240","66800","34176","8848","-400","-880","-160","0","0","0"],["0","0","288","2272","7960","16096","20384","16304","7736","1696","-80","-80","0","0","0","0"],["0","0","0","192","1048","2480","3264","2496","1016","144","-16","0","0","0","0","0"],["0","0","0","0","48","192","288","192","48","0","0","0","0","0","0","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["-32","-480","-3280","-13504","-37232","-71968","-98384","-91520","-48048","4576","34320","34112","19760","7456","1808","256","16"],["-160","-2320","-15296","-60880","-163232","-310224","-425216","-413072","-258720","-57904","72512","97168","62624","25360","6528","976","64"],["-416","-5808","-36960","-142688","-373600","-699344","-955456","-945024","-638592","-228944","51744","130848","91936","38096","9856","1472","96"],["-704","-9248","-56256","-210368","-539200","-996608","-1355840","-1352352","-950272","-406304","-23104","105472","82624","33856","8256","1120","64"],["-736","-9280","-55568","-207072","-530896","-981280","-1334112","-1332800","-949600","-436000","-74976","54304","49408","19392","4176","448","16"],["-416","-5712","-36480","-141456","-370624","-692192","-944064","-941792","-670336","-314144","-69440","18272","20384","7184","1216","80","0"],["-96","-2096","-15872","-67040","-184800","-355072","-489024","-485152","-339616","-156288","-36448","4064","5728","1616","160","0","0"],["0","-384","-4224","-21472","-65152","-131072","-183488","-180768","-122624","-53280","-11584","768","1024","160","0","0","0"],["0","0","-576","-4256","-15264","-33600","-48592","-47104","-30128","-11712","-2032","160","80","0","0","0","0"],["0","0","0","-384","-2144","-5456","-8256","-7888","-4576","-1392","-128","16","0","0","0","0","0"],["0","0","0","0","-96","-432","-768","-672","-288","-48","0","0","0","0","0","0","0"]]},"deriv_order":1},{"coeff":{"coeffs":[["40","560","3640","14560","40040","80080","120120","137280","120120","80080","40040","14560","3640","560","40"],["208","2704","16384","61408","159280","302896","436128","483648","415536","275440","138688","51424","13264","2128","160"],["432","5344","31104","112992","286240","534624","758448","829248","701424","456480","224992","81504","20544","3232","240"],["448","5600","33088","121920","311808","583968","824608","891008","739648","468768","222720","76608","17920","2528","160"],["232","3376","21976","85920","227376","433152","614032","657952","534352","326016","146160","46176","9496","1072","40"],["48","1168","9312","40608","114720","226656","325440","345760","272736","157920","65088","17952","2928","208","0"],["0","192","2352","12640","39968","83680","122864","129664","98480","52768","19040","4192","432","0","0"],["0","0","288","2368","9088","21088","32288","33728","24128","11488","3328","448","0","0","0"],["0","0","0","192","1192","3312","5400","5600","3672","1392","232","0","0","0","0"],["0","0","0","0","48","240","480","480","240","48","0","0","0","0","0"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["384","4208","20688","59680","110192","130944","89056","8976","-47520","-51216","-26224","-5952","688","800","192","16"],["1504","15368","71320","197384","357336","430160","318448","81168","-108720","-148760","-87880","-24920","248","2496","704","64"],["3408","33840","153800","419288","751280","901984","684192","226752","-137088","-227616","-139368","-41848","-1408","3344","1024","96"],["5128","50336","225624","606120","1073272","1286072","1001912","398808","-88688","-230040","-144592","-42304","-1616","2752","768","64"],["5280","52648","237280","637008","1123144","1339256","1048304","451216","-19784","-163088","-104096","-29056","-912","1536","320","16"],["4160","41464","186480","498424","872992","1033936","809176","362816","18568","-86696","-54152","-13400","-232","512","64","0"],["2400","24000","109320","294544","515392","604368","465920","209176","21440","-33744","-20296","-4216","32","80","0","0"],["920","10160","47848","130376","228536","266232","202072","89192","11152","-9800","-5152","-784","0","0","0","0"],["240","2808","14544","42192","75704","87576","64640","27472","3784","-1888","-832","-80","0","0","0","0"],["0","432","2936","9312","17560","20752","15016","5952","776","-224","-64","0","0","0","0","0"],["0","0","240","1240","2720","3264","2256","824","96","-16","0","0","0","0","0","0"],["0","0","0","48","192","288","192","48","0","0","0","0","0","0","0","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["-96","-1536","-10496","-41392","-105808","-184640","-223168","-182512","-91344","-16896","8448","3952","-2416","-2752","-1088","-208","-16"],["-912","-11408","-63904","-212736","-469056","-719040","-776320","-574992","-259968","-33936","35680","19040","-2688","-6432","-2880","-592","-48"],["-2776","-31152","-158824","-487312","-1000560","-1437824","-1455744","-998640","-394824","-10192","82488","39920","704","-6912","-3152","-624","-48"],["-4656","-49032","-236864","-692592","-1357952","-1861280","-1789904","-1154464","-411744","19624","104832","48832","4640","-4352","-1904","-304","-16"],["-4960","-50512","-237464","-676784","-1291608","-1716976","-1591160","-977136","-320344","28672","83456","36256","4624","-1536","-624","-64","0"],["-3440","-35712","-168816","-478312","-899040","-1167760","-1049824","-621144","-195264","15264","43776","17552","2288","-288","-80","0","0"],["-1608","-17584","-85288","-244864","-461760","-594784","-523152","-299072","-91160","3536","14808","5248","640","0","0","0","0"],["-432","-5416","-29472","-90208","-173984","-223328","-192848","-107248","-32192","-440","3120","912","80","0","0","0","0"],["0","-912","-6520","-22208","-45720","-60432","-51480","-27168","-7720","-448","336","64","0","0","0","0","0"],["0","0","-624","-3336","-7840","-10608","-8896","-4488","-1152","-64","16","0","0","0","0","0","0"],["0","0","0","-144","-624","-1056","-864","-336","-48","0","0","0","0","0","0","0","0"]]},"deriv_order":1},{"coeff":{"coeffs":[["80","1000","5720","19760","45760","74360","85800","68640","34320","5720","-5720","-5200","-2080","-440","-40"],["528","6040","31616","100008","212344","316976","336600","247632","111936","12408","-22352","-18040","-6984","-1472","-136"],["1288","13960","69696","211728","434600","630768","654168","471744","210744","26632","-35120","-27792","-10152","-1984","-168"],["1704","18400","91472","275960","560144","800040","813312","575000","256064","41016","-29464","-24048","-8152","-1376","-88"],["1496","16360","81504","244760","492528","695616","697992","487016","216592","40992","-14840","-12768","-3768","-488","-16"],["872","9656","49176","150760","306952","433056","428408","291952","127440","26568","-4112","-4152","-960","-64","0"],["240","3400","19800","64720","135096","191264","187160","124368","52216","10840","-560","-736","-96","0","0"],["0","624","4856","18056","40592","59144","57008","35928","13904","2664","-8","-64","0","0","0"],["0","0","528","3000","7664","11544","11040","6568","2160","264","-16","0","0","0","0"],["0","0","0","144","672","1248","1152","528","96","0","0","0","0","0","0"]]},"deriv_order":2},{"coeff":{"coeffs":[["0","0","0","0","0","0","0","0","0","0","0","0","0"],["-40","-480","-2640","-8800","-19800","-31680","-36960","-31680","-19800","-8800","-2640","-480","-40"],["-168","-1848","-9360","-28920","-60840","-92016","-102816","-85680","-52920","-23640","-7248","-1368","-120"],["-264","-2760","-13464","-40536","-83784","-124944","-137424","-111984","-66936","-28584","-8280","-1464","-120"],["-184","-2040","-10488","-32784","-69048","-102984","-111424","-88008","-50184","-19968","-5160","-744","-40"],["-48","-792","-4872","-16608","-36432","-55080","-59040","-44952","-23808","-8352","-1752","-168","0"],["0","-144","-1272","-5160","-12432","-19464","-20544","-14712","-6960","-1992","-264","0","0"],["0","0","-144","-904","-2544","-4200","-4400","-2904","-1104","-184","0","0","0"],["0","0","0","-48","-240","-480","-480","-240","-48","0","0","0","0"]]},"deriv_order":3}]]},{"annihilator":{"terms":[{"coeff":{"coeffs":[["-4","-4","0"],["2","2","-1"],["-1","0","0"],["1","0","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-2","-3","0","1"],["3","0","0","0"],["-2","-1","0","0"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","0"],["1","1"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["2"]]},"deriv_order":0,"shift":1}]},"quotient":[{"coeff":{"coeffs":[["-4","-28","-84","-140","-140","-84","-28","-4"],["-24","-160","-464","-760","-760","-464","-160","-24"],["-40","-248","-684","-1092","-1092","-684","-248","-40"],["-24","-168","-512","-864","-864","-512","-168","-24"],["-4","-60","-220","-388","-388","-220","-60","-4"],["0","-8","-48","-104","-104","-48","-8","0"],["0","0","-4","-12","-12","-4","0","0"]]},"deriv_order":0}],"step_multiplier":{"coeffs":[["16","192","1056","3520","7920","12672","14784","12672","7920","3520","1056","192","16"],["64","704","3584","11200","24000","37248","43008","37248","24000","11200","3584","704","64"],["96","1024","5152","16128","34848","54528","63168","54528","34848","16128","5152","1024","96"],["64","768","4224","14016","31296","49728","57856","49728","31296","14016","4224","768","64"],["16","320","2144","7872","18688","30784","36256","30784","18688","7872","2144","320","16"],["0","64","640","2880","7616","13184","15744","13184","7616","2880","640","64","0"],["0","0","96","640","2016","3840","4736","3840","2016","640","96","0","0"],["0","0","0","64","320","704","896","704","320","64","0","0","0"],["0","0","0","0","16","64","96","64","16","0","0","0","0"]]},"step_quotients":[[{"coeff":{"coeffs":[["16","192","1056","3520","7920","12672","14784","12672","7920","3520","1056","192","16"],["64","704","3584","11200","24000","37248","43008","37248","24000","11200","3584","704","64"],["96","1024","5152","16128","34848","54528","63168","54528","34848","16128","5152","1024","96"],["64","768","4224","14016","31296","49728","57856","49728","31296","14016","4224","768","64"],["16","320","2144","7872","18688","30784","36256","30784","18688","7872","2144","320","16"],["0","64","640","2880","7616","13184","15744","13184","7616","2880","640","64","0"],["0","0","96","640","2016","3840","4736","3840","2016","640","96","0","0"],["0","0","0","64","320","704","896","704","320","64","0","0","0"],["0","0","0","0","16","64","96","64","16","0","0","0","0"]]},"deriv_order":0}],[{"coeff":{"coeffs":[["-16","-208","-1256","-4672","-11968","-22352","-31416","-33792","-27984","-17776","-8536","-3008","-736","-112","-8"],["-40","-464","-2552","-8896","-22120","-41680","-61368","-71424","-65592","-46960","-25640","-10304","-2872","-496","-40"],["16","192","880","1760","-224","-10496","-30576","-52032","-61296","-52544","-33072","-15008","-4672","-896","-80"],["152","1600","7792","23168","46360","64128","59024","28832","-6776","-25440","-23344","-12576","-4280","-864","-80"],["208","2256","11544","36416","78064","118624","129152","98304","46992","7232","-7712","-6656","-2528","-496","-40"],["136","1712","9624","32320","72736","115680","132528","108512","60736","20096","1216","-2176","-1000","-176","-8"],["48","800","5184","19072","45616","75424","88592","74080","42848","15648","2544","-416","-256","-32","0"],["8","224","1856","7808","20192","34976","42048","35200","19984","7136","1264","-32","-40","0","0"],["0","32","416","2176","6352","11696","14328","11840","6432","2096","312","0","0","0","0"],["0","0","48","384","1352","2736","3464","2784","1368","368","40","0","0","0","0"],["0","0","0","32","176","416","544","416","176","32","0","0","0","0","0"],["0","0","0","0","8","32","48","32","8","0","0","0","0","0","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["-8","-128","-912","-3864","-10904","-21648","-30976","-31944","-22968","-10208","-1232","1752","1368","496","96","8"],["-40","-592","-3920","-15552","-41528","-79088","-110464","-113760","-84504","-41776","-9616","3328","3960","1648","352","32"],["-96","-1320","-8272","-31552","-82048","-153640","-212448","-217872","-162720","-83256","-23376","1952","5120","2312","512","48"],["-144","-1856","-11184","-41632","-106448","-196704","-269120","-274112","-204816","-106784","-33168","-1344","3952","1856","384","32"],["-136","-1712","-10256","-38152","-97504","-179808","-244848","-247392","-183008","-95040","-30768","-3312","1880","928","160","8"],["-72","-1008","-6448","-24928","-65056","-120960","-164432","-164576","-119872","-61088","-19664","-2688","536","272","32","0"],["-16","-360","-2736","-11536","-31600","-60240","-82432","-81632","-57840","-28256","-8688","-1248","80","40","0","0"],["0","-64","-720","-3648","-10992","-21920","-30368","-29696","-20272","-9248","-2544","-320","0","0","0","0"],["0","0","-96","-720","-2568","-5584","-7984","-7672","-4904","-1984","-448","-40","0","0","0","0"],["0","0","0","-64","-360","-912","-1360","-1280","-744","-240","-32","0","0","0","0","0"],["0","0","0","0","-16","-72","-128","-112","-48","-8","0","0","0","0","0","0"]]},"deriv_order":1},{"coeff":{"coeffs":[["8","104","624","2288","5720","10296","13728","13728","10296","5720","2288","624","104","8"],["40","488","2768","9680","23320","40920","53856","53856","40920","23320","9680","2768","488","40"],["80","944","5232","18032","43088","75312","98976","98976","75312","43088","18032","5232","944","80"],["80","976","5584","19760","48144","85200","112640","112640","85200","48144","19760","5584","976","80"],["40","584","3728","14128","35936","65248","87312","87312","65248","35936","14128","3728","584","40"],["8","200","1584","6768","18528","35136","47984","47984","35136","18528","6768","1584","200","8"],["0","32","400","2128","6576","13328","18752","18752","13328","6576","2128","400","32","0"],["0","0","48","400","1520","3440","5088","5088","3440","1520","400","48","0","0"],["0","0","0","32","200","552","880","880","552","200","32","0","0","0"],["0","0","0","0","8","40","80","80","40","8","0","0","0","0"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["120","1216","5480","14304","23368","23360","10872","-4800","-11832","-9024","-3560","-544","120","64","8"],["432","4088","17520","44560","73392","78440","47424","1248","-26544","-25656","-12112","-2544","208","216","32"],["848","8016","34640","89312","149832","165536","111200","25728","-29360","-35280","-17952","-4256","88","288","48"],["1152","11064","47968","123480","207936","235184","171056","61792","-14784","-31160","-16720","-3896","32","208","32"],["1120","10896","47744","124320","211680","242384","181864","77072","2408","-18144","-10624","-2384","40","96","8"],["816","8032","35728","93688","159888","184152","141040","64552","9264","-7424","-4672","-944","16","24","0"],["432","4416","20008","53328","92000","105968","80712","37760","7624","-1936","-1488","-240","8","0","0"],["160","1768","8432","22960","39824","45888","34832","16168","3504","-280","-288","-40","0","0","0"],["40","480","2488","7232","12968","14912","11008","4960","1120","0","-40","0","0","0","0"],["0","72","496","1576","2960","3488","2544","1064","208","8","0","0","0","0","0"],["0","0","40","208","456","544","376","144","24","0","0","0","0","0","0"],["0","0","0","8","32","48","32","8","0","0","0","0","0","0","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["-16","-328","-2424","-9672","-24112","-39960","-44696","-32568","-13104","-184","2648","1032","-144","-232","-72","-8"],["-208","-2624","-14416","-46264","-97232","-140928","-142752","-97896","-39216","-1984","7216","3512","80","-512","-192","-24"],["-648","-6928","-33608","-98296","-192840","-264952","-255840","-166328","-61544","-912","11752","5448","440","-488","-192","-24"],["-1016","-10128","-46864","-131968","-249280","-328600","-303776","-189432","-67592","-992","12144","5536","608","-280","-96","-8"],["-976","-9728","-44616","-123440","-228184","-293992","-264800","-159680","-54792","-1496","8032","3520","464","-80","-24","0"],["-624","-6512","-30328","-84272","-154896","-196128","-172152","-101280","-34752","-2264","3584","1472","176","-8","0","0"],["-280","-3056","-14856","-42200","-78064","-98544","-85360","-48904","-16432","-1712","904","368","40","0","0","0"],["-72","-928","-5024","-15272","-29152","-36816","-31296","-17536","-5880","-784","128","40","0","0","0","0"],["0","-152","-1104","-3744","-7608","-9928","-8392","-4464","-1384","-208","-8","0","0","0","0","0"],["0","0","-104","-560","-1312","-1752","-1448","-736","-208","-24","0","0","0","0","0","0"],["0","0","0","-24","-104","-176","-144","-56","-8","0","0","0","0","0","0","0"]]},"deriv_order":1},{"coeff":{"coeffs":[["16","184","960","2992","6160","8712","8448","5280","1584","-440","-704","-336","-80","-8"],["104","1120","5504","16280","32120","44088","42240","26928","9240","-880","-2816","-1480","-376","-40"],["248","2576","12280","35432","68584","92984","88912","57872","22120","1024","-4104","-2424","-648","-72"],["320","3344","16000","46240","89496","121200","115872","76024","30624","3896","-3200","-2072","-536","-56"],["272","2896","14032","40848","79232","107088","102032","67096","27976","5088","-1360","-1048","-232","-16"],["152","1672","8392","25112","49560","67440","64024","41624","17312","3640","-192","-288","-48","0"],["40","584","3360","10784","21992","30192","28456","18176","7408","1608","56","-32","0","0"],["0","104","824","3032","6664","9464","8872","5416","2040","416","32","0","0","0"],["0","0","88","504","1280","1888","1752","1016","336","48","0","0","0","0"],["0","0","0","24","112","208","192","88","16","0","0","0","0","0"]]},"deriv_order":2},{"coeff":{"coeffs":[["0","0","0","0","0","0","0","0","0","0","0","0"],["-8","-88","-440","-1320","-2640","-3696","-3696","-2640","-1320","-440","-88","-8"],["-32","-328","-1544","-4416","-8544","-11760","-11760","-8544","-4416","-1544","-328","-32"],["-48","-480","-2232","-6360","-12312","-16968","-16968","-12312","-6360","-2232","-480","-48"],["-32","-352","-1760","-5272","-10520","-14704","-14704","-10520","-5272","-1760","-352","-32"],["-8","-136","-824","-2728","-5744","-8224","-8224","-5744","-2728","-824","-136","-8"],["0","-24","-216","-864","-2016","-3024","-3024","-2016","-864","-216","-24","0"],["0","0","-24","-152","-424","-680","-680","-424","-152","-24","0","0"],["0","0","0","-8","-40","-80","-80","-40","-8","0","0","0"]]},"deriv_order":3}]]},{"annihilator":{"terms":[{"coeff":{"coeffs":[["0","0","0"],["0","-3","-1"],["-2","0","-1"],["0","-1","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["1","3","3","1"],["1","2","2","1"],["0","1","1","0"]]},"deriv_order":1,"shift":0}]},"quotient":[{"coeff":{"coeffs":[["-8","-44","-96","-100","-40","12","16","4"],["14","40","-8","-144","-186","-80","4","8"],["22","54","12","-114","-194","-132","-28","4"],["18","90","92","-70","-166","-96","-20","0"],["26","70","72","-2","-74","-48","-4","0"],["8","38","44","-2","-24","-8","0","0"],["0","8","12","0","-4","0","0","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","0","0"],["10","14","-44","-116","-94","-26"],["-8","-62","-122","-110","-62","-20"],["-26","-66","-92","-80","-18","10"],["-8","-38","-50","-14","10","4"],["0","-8","-12","0","4","0"]]},"deriv_order":1}],"step_multiplier":{"coeffs":[["4","36","144","336","504","504","336","144","36","4"],["12","96","348","756","1092","1092","756","348","96","12"],["12","96","360","816","1212","1212","816","360","96","12"],["4","48","216","524","792","792","524","216","48","4"],["0","12","72","204","336","336","204","72","12","0"],["0","0","12","48","84","84","48","12","0","0"],["0","0","0","4","12","12","4","0","0","0"]]},"step_quotients":[[],[{"coeff":{"coeffs":[["-4","-44","-220","-660","-1320","-1848","-1848","-1320","-660","-220","-44","-4"],["-20","-204","-954","-2706","-5184","-7056","-6972","-5004","-2556","-884","-186","-18"],["-40","-390","-1766","-4902","-9258","-12474","-12222","-8706","-4422","-1528","-324","-32"],["-40","-400","-1858","-5258","-10036","-13544","-13178","-9238","-4568","-1516","-304","-28"],["-20","-240","-1236","-3706","-7290","-9942","-9610","-6576","-3108","-956","-168","-12"],["-4","-84","-530","-1766","-3678","-5134","-4934","-3258","-1432","-388","-54","-2"],["0","-14","-138","-562","-1290","-1870","-1786","-1122","-442","-96","-8","0"],["0","0","-18","-110","-300","-468","-446","-258","-84","-12","0","0"],["0","0","0","-10","-42","-74","-70","-36","-8","0","0","0"],["0","0","0","0","-2","-6","-6","-2","0","0","0","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["4","48","264","880","1980","3168","3696","3168","1980","880","264","48","4"],["14","158","824","2630","5730","8988","10416","8988","5730","2630","824","158","14"],["18","206","1094","3558","7878","12492","14532","12492","7878","3558","1094","206","18"],["10","138","822","2868","6618","10722","12556","10722","6618","2868","822","138","10"],["2","50","374","1476","3664","6178","7328","6178","3664","1476","374","50","2"],["0","8","98","486","1360","2434","2940","2434","1360","486","98","8","0"],["0","0","12","94","324","642","800","642","324","94","12","0","0"],["0","0","0","8","44","104","136","104","44","8","0","0","0"],["0","0","0","0","2","8","12","8","2","0","0","0","0"]]},"deriv_order":1}],[{"coeff":{"coeffs":[["-4","-36","-140","-300","-360","-168","168","360","300","140","36","4"],["-22","-190","-730","-1626","-2268","-1932","-756","300","594","362","110","14"],["-60","-496","-1846","-4044","-5690","-5198","-2838","-526","446","390","132","18"],["-74","-622","-2360","-5276","-7602","-7212","-4320","-1322","96","246","84","10"],["-50","-476","-1930","-4458","-6510","-6210","-3782","-1292","-96","98","32","2"],["-24","-246","-1058","-2544","-3792","-3620","-2166","-726","-78","24","6","0"],["-6","-80","-394","-1012","-1536","-1440","-822","-256","-26","4","0","0"],["0","-14","-92","-264","-420","-390","-204","-52","-4","0","0","0"],["0","0","-10","-42","-72","-64","-30","-6","0","0","0","0"],["0","0","0","-2","-6","-6","-2","0","0","0","0","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["8","84","396","1100","1980","2376","1848","792","0","-220","-132","-36","-4"],["32","306","1320","3380","5670","6444","4872","2160","180","-430","-288","-84","-10"],["52","488","2076","5256","8718","9778","7294","3258","446","-402","-274","-74","-8"],["52","492","2090","5240","8554","9418","6930","3148","600","-186","-144","-32","-2"],["32","312","1364","3486","5728","6264","4528","2030","442","-30","-38","-6","0"],["8","114","578","1572","2634","2862","2022","884","202","8","-4","0","0"],["0","20","144","454","812","892","608","246","52","4","0","0","0"],["0","0","16","76","154","172","112","40","6","0","0","0","0"],["0","0","0","4","14","18","10","2","0","0","0","0","0"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","0","0","0","0","0","0","0"],["-4","-40","-180","-480","-840","-1008","-840","-480","-180","-40","-4"],["-10","-94","-402","-1032","-1764","-2100","-1764","-1032","-402","-94","-10"],["-8","-82","-376","-1016","-1792","-2156","-1792","-1016","-376","-82","-8"],["-2","-34","-192","-574","-1062","-1296","-1062","-574","-192","-34","-2"],["0","-6","-52","-190","-388","-488","-388","-190","-52","-6","0"],["0","0","-6","-34","-82","-108","-82","-34","-6","0","0"],["0","0","0","-2","-8","-12","-8","-2","0","0","0"]]},"deriv_order":2}]]}],"restart_bases":[],"row_multiplier":{"coeffs":[["4","24","60","80","60","24","4"],["8","40","88","112","88","40","8"],["4","24","64","88","64","24","4"],["0","8","24","32","24","8","0"],["0","0","4","8","4","0","0"]]},"start_base":1}},"shifted_parent_relation":{"terms":[{"coeff":{"coeffs":[["-1","-3","-3","-1"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["3","6","3"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["-3","-3"]]},"deriv_order":0,"shift":2},{"coeff":{"coeffs":[["1"]]},"deriv_order":0,"shift":3}]},"statement":"w(n) E = sum_nu H_nu S^nu L' (with any remainder removed by row annihilators of the parent), where L' is the parent rule at P'_n = P_(n+0) (valid from base 0) and E the input rule gauged by lambda(n)/delta(n) and composed with (or conjugated through) T = P((1) x + (1)); so the candidate rows satisfy the input rule at every base n >= 1 (the exceptional bases checked exactly), and agreement on the 3 identifying rows gives Q_n = lambda(n) T_n(P_(n+0)) for every n >= 0"},"method":"operator_division"},"status":"certified"},"input_first_index":0,"interlacing":{"reason":"no parent theorem report with an interlacing conclusion","status":"none"},"lean_declarations":["Polynomial.Splits.comp_of_degree_le_one"],"lift_summary":{"hypotheses":[{"evidence":"lambda(n) = 1","name":"gauge_finite_nonzero","statement":"lambda(n) is finite and nonzero for every n >= n0","status":{"kind":"verified"}}],"identity":{"method":"forward_division","status":"certified"},"input_first_index":0,"input_interlacing":{"reason":"no parent theorem report with an interlacing conclusion","status":"not_proved"},"lean_replay":"not_attempted","operation":{"description":"P((1) x + (1))","kind":"preserver_image","operator":{"intercept":"1","shape":"affine","slope":"1"}},"parent":{"gauge":{"kind":"none"},"index_shift":0,"recurrence":{"first_index":0,"initial_polynomials":[["1"],["2","2"],["3","8","3"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["3","3"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["-3","-6","-3"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["1","3","3","1"]]},"deriv_order":0,"offset":3,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"relation":"Q_n = lambda(n) T_n(P_(n+0)) with T = P((1) x + (1)), for every n >= 0"},"parent_proof":{"statement":"open: no route proved that every parent row P_n, n >= 0, is zero or real-rooted with coefficients of one sign; the first 10 parent rows pass the exact check (evidence only)","status":"open"},"root_transfer":{"input_conclusion":"every Q_n, n >= 0, is zero or real-rooted with roots in (-inf, -1]","input_root_region":{"upper":{"closed":true,"value":"-1"}},"parent_hypothesis":"every parent row used is zero or real-rooted with all roots in (-inf, 0] (coefficients of one sign)","parent_root_region":{"upper":{"closed":true,"value":"0"}},"theorem":"a real affine substitution x -> a x + b (a != 0), the reversal x^d p(1/x) (d >= deg p) and a real Mobius map (c x + e)^d p((a x + b)/(c x + e)) (a e - b c != 0, d >= deg p) map real roots to real roots: a root r of p gives the root (r - b)/a, 1/r (and 0) or (e r - b)/(a - c r) (and -e/c); for an input row that is a polynomial the degree condition holds automatically"},"verdict":"open"},"notes":["the division remainder is removed by row annihilators of the shifted parent"],"parent_proof":{"attempts":[{"detail":"the rule is not P_(n+k) = c(x) P_n with c free of n","route":"periodic_product","success":false,"variant":"P_(n+k) = c(x) P_n"},{"detail":"no theorem matched (weighted_renewal_window: coefficient of P_(n-1) must be 1 after normalization; fixed_delay_predecessor_window: coefficient of P_(n-1) must be 1 (+ w(n) t) after normalization)","route":"paper_theorem","success":false,"variant":"match_recurrence_theorems"},{"detail":"not applicable: the rule is not f(n) P_n = c_1(n, x) P_(n-1) + c_2(n, x) P_(n-2) with both terms nonzero","route":"three_term_recurrence","success":false,"variant":"three_term_recurrence"},{"detail":"not applicable: the rule is not f(n) P_n = c_0(n, x) P_(n-1) + c_1(n, x) P'_(n-1)","route":"liu_wang","success":false,"variant":"liu_wang"},{"detail":"not applicable: the rule is not f(n) P_n = c_0(n, x) P_(n-1) + c_1(n, x) P'_(n-1) + c_2(n, x) P_(n-2) with a derivative or a lag term","route":"liu_wang_derivative_lag","success":false,"variant":"liu_wang_derivative_lag"},{"detail":"not applicable: the rule is not f(n) P_n = c_0(n, x) P_(n-1) + gamma(n) (x - L)(x - U) P'_(n-1)","route":"ma_wang_interval","success":false,"variant":"ma_wang_interval"},{"detail":"the parent equals the flagged entry, but the flag gives real-rootedness only and one-signed coefficients are not shown: the weight of the coefficient of x^s of P_(n-2) in the coefficient of x^(s+0) is not shown to be >= 0 for n >= 3","route":"attestation","success":false,"variant":"oeis_catalog:A141611:lean_proved"},{"detail":"no lean_proved catalog entry equals the parent; 1 with the same first index and seeds differ in the rule or in later initial rows (oeis_catalog:A145596:lean_proved)","route":"attestation","success":false,"variant":"oeis_catalog"}],"conditional_on":[],"rows_checked":10,"statement":"open: no route proved that every parent row P_n, n >= 0, is zero or real-rooted with coefficients of one sign; the first 10 parent rows pass the exact check (evidence only)","status":"not_proved"},"rows_compared":16,"schema":"polytool.recurrence-preserver-image.v1","statement":"Q_n = lambda(n) T_n(P_(n+0)) with T = P((1) x + (1)) for every n >= 0 is certified; the lift is Open (open: no route proved that every parent row P_n, n >= 0, is zero or real-rooted with coefficients of one sign; the first 10 parent rows pass the exact check (evidence only))"},"kind":"preserver_image"}