{"certification":{"candidate":{"gauge":{"kind":"none"},"index_shift":0,"operator":{"schedule":{"first_degree":0,"first_index":0,"step":1},"shape":"reversal"},"parent":{"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"},"parent_name":"shift_x_plus_one of 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":[["16","8","0"],["-6","3","3"],["-8","-2","1"],["-2","-1","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["0","-12","-12","-3"],["0","-4","-4","-1"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["-4"],["1"],["2"],["1"]]},"deriv_order":0,"shift":1}]},"exceptional_bases":[],"gauge":{"kind":"none"},"identifying_indices":[0,1,2],"index_shift":0,"input":{"first_index":0,"initial_polynomials":[["1"],["2","4"],["3","14","14"]],"recurrence":{"denominator":{"coeffs":[["-4"],["0"],["-1"],["1"]]},"terms":[{"coeff":{"coeffs":[["-12","-24"],["0","0"],["3","6"],["1","2"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["-2","-8","-8"],["-1","-4","-4"]]},"deriv_order":1,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"input_valid_from_base":2,"multiplier":["1"],"operator":{"schedule":{"first_degree":0,"first_index":0,"step":1},"shape":"reversal"},"parent":{"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"},"parent_leader_shift":2,"parent_valid_from_base":1,"quotients":[],"row_annihilation":{"kind":"system","system":{"generators":[{"annihilator":{"terms":[{"coeff":{"coeffs":[["-8","-4","0"],["3","0","-1"],["-1","0","0"],["1","0","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-4","0","3","1"],["3","0","0","0"],["-3","-1","0","0"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","0"],["2","1"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["2"]]},"deriv_order":0,"shift":1}]},"quotient":[{"coeff":{"coeffs":[["-256","-768","-960","-640","-240","-48","-4"],["-320","-960","-1232","-864","-348","-76","-7"],["-48","-144","-164","-88","-22","-2","0"],["228","684","885","630","261","60","6"],["240","720","908","616","236","48","4"],["120","360","438","276","94","16","1"],["32","96","112","64","18","2","0"],["4","12","13","6","1","0","0"]]},"deriv_order":0}],"step_multiplier":{"coeffs":[["32768","196608","540672","901120","1013760","811008","473088","202752","63360","14080","2112","192","8"],["98304","589824","1630208","2744320","3133440","2555904","1526784","672768","216960","49920","7776","736","32"],["143360","860160","2375680","3993600","4551168","3704832","2209536","973056","314160","72544","11376","1088","48"],["129024","774144","2130432","3555840","4008576","3214848","1880288","807840","252960","56288","8448","768","32"],["77952","467712","1278912","2107200","2328840","1816992","1024560","419616","123368","25216","3360","256","8"],["32256","193536","524544","848640","911328","682368","363584","137856","36448","6400","672","32","0"],["8960","53760","144000","227200","234288","165312","80992","27264","6048","800","48","0","0"],["1536","9216","24320","37120","36192","23424","10080","2784","448","32","0","0","0"],["128","768","1984","2880","2568","1440","496","96","8","0","0","0","0"]]},"step_quotients":[[{"coeff":{"coeffs":[["131072","851968","2555904","4685824","5857280","5271552","3514368","1757184","658944","183040","36608","4992","416","16","0"],["671744","4292608","12640256","22683648","27630592","24059904","15341568","7197696","2447808","575872","82016","3232","-1116","-208","-12"],["1654784","10412032","30101504","52793344","62391296","52077568","31157760","13148160","3631296","467680","-79792","-52688","-11716","-1328","-64"],["2635776","16359424","46485504","79700992","91293440","72764672","40357376","14666944","2583576","-485680","-479808","-157248","-29144","-3040","-140"],["3057152","18756864","52498944","88222080","98287584","75169168","38850608","12013552","695048","-1333408","-738504","-210992","-36420","-3616","-160"],["2738240","16649856","46047264","76180896","83145700","61815744","30579164","8594224","-50740","-1255344","-612836","-163168","-26416","-2448","-100"],["1947328","11766400","32258720","52785888","56879084","41729040","20453704","5860368","213540","-630464","-307816","-77616","-11532","-944","-32"],["1108224","6670336","18172864","29501952","31536496","23040384","11422884","3541952","432040","-155424","-92932","-22528","-2952","-192","-4"],["501440","3011968","8163488","13154656","13951340","10149568","5085768","1684976","313204","2736","-14584","-3664","-396","-16","0"],["177024","1062400","2863872","4571584","4789592","3441872","1715516","581792","125264","13520","-332","-256","-20","0","0"],["47168","283008","757728","1193376","1225476","858064","415160","137136","29612","3776","216","0","0","0","0"],["8960","53760","142656","220416","219472","146976","66892","20352","3936","432","20","0","0","0","0"],["1088","6528","17120","25760","24516","15312","6280","1632","244","16","0","0","0","0","0"],["64","384","992","1440","1284","720","248","48","4","0","0","0","0","0","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0"],["-196608","-1228800","-3391488","-5283840","-4706304","-1520640","1858560","3244032","2661120","1442496","555456","154080","30288","4020","324","12"],["-802816","-5079040","-14376960","-23547904","-23530496","-12438528","1280000","8624640","8387136","4920064","1997344","578160","118060","16244","1356","52"],["-1695744","-10815488","-31148032","-52807680","-56884224","-37570304","-10007296","7630464","11071776","7232376","3084920","919024","191400","26748","2264","88"],["-2344960","-15027200","-43765760","-75928320","-85836288","-63829696","-27902592","-1807440","7092936","5837080","2663216","809264","168180","23148","1912","72"],["-2313984","-14859968","-43532736","-76516064","-88958960","-70529484","-37002748","-10524940","943128","2585412","1371796","428340","87008","11308","852","28"],["-1689408","-10851904","-31836960","-56231168","-66215220","-54159996","-30788940","-11470532","-2086132","382644","397188","135308","26548","3084","188","4"],["-924672","-5933760","-17368320","-30608928","-36060000","-29745324","-17416792","-7110128","-1870208","-220916","39440","22552","4392","420","16","0"],["-377920","-2420800","-7046880","-12314560","-14361188","-11735484","-6849840","-2845504","-815148","-147220","-11944","936","300","20","0","0"],["-112896","-721472","-2082496","-3586848","-4098768","-3264452","-1849708","-745772","-209672","-39140","-4364","-220","0","0","0","0"],["-23488","-149696","-427232","-720768","-798396","-609172","-326156","-122212","-31276","-5172","-492","-20","0","0","0","0"],["-3072","-19520","-54912","-90080","-95456","-68292","-33408","-11032","-2352","-292","-16","0","0","0","0","0"],["-192","-1216","-3360","-5312","-5292","-3444","-1464","-392","-60","-4","0","0","0","0","0","0"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","0","0","0","0","0","0","0","0","0","0"],["98304","638976","1916928","3514368","4392960","3953664","2635776","1317888","494208","137280","27456","3744","312","12"],["425984","2768896","8331264","15364096","19374080","17639424","11928576","6065664","2318976","658240","134816","18864","1616","64"],["856064","5564416","16756736","30953472","39130624","35749632","24283392","12417408","4780176","1368232","283040","40072","3480","140"],["1058816","6882304","20700672","38148352","48056960","43701696","29515680","14991408","5726736","1625200","333104","46704","4016","160"],["893312","5806528","17414080","31905632","39841272","35801196","23811968","11865448","4427736","1221396","241920","32552","2664","100"],["537600","3494400","10432512","18940416","23323200","20558880","13334240","6434512","2305712","604240","112080","13840","1008","32"],["233856","1520064","4510656","8087904","9768696","8380908","5243072","2413768","813720","196868","32800","3480","200","4"],["72704","472576","1391616","2455552","2891456","2392416","1424736","614160","189616","40688","5712","464","16","0"],["15488","100672","293696","507936","578920","456708","254464","100088","27208","4860","512","24","0","0"],["2048","13312","38400","64768","70784","52416","26656","9200","2064","272","16","0","0","0"],["128","832","2368","3872","4008","2724","1216","344","56","4","0","0","0","0"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["65536","327680","688128","720896","225280","-405504","-675840","-540672","-278784","-98560","-23936","-3840","-368","-16","0"],["262144","1261568","2531328","2478080","575488","-1560576","-2260992","-1623552","-725760","-202432","-29024","912","1192","200","12"],["626688","2967552","5859328","5675008","1468928","-2964736","-4145664","-2659200","-925680","-101112","61080","33680","7988","988","52"],["1152000","5426176","10791424","10960640","4270336","-3019456","-5241632","-3313456","-983844","34864","154312","65360","14336","1708","88"],["1627648","7697024","15595904","16825792","8747680","-894808","-4707944","-3332160","-1064020","-12000","133036","57756","12492","1448","72"],["1752768","8336384","17184288","19437728","11920876","1998632","-2816304","-2554952","-971340","-121544","50008","27420","5928","640","28"],["1444608","6896320","14384448","16797536","11342960","3497740","-860780","-1386268","-629760","-130708","-4","6616","1516","140","4"],["917184","4383168","9198880","10951424","7835276","3063972","174056","-483196","-270460","-69084","-7384","408","176","12","0"],["448320","2141120","4501472","5412160","4005076","1769396","342792","-79284","-71656","-20504","-2796","-132","4","0","0"],["166784","796096","1671808","2014880","1515512","713772","188924","11476","-9476","-3216","-424","-20","0","0","0"],["45952","219712","460288","552672","416184","200756","59716","9244","96","-188","-20","0","0","0","0"],["8896","42816","89504","106432","78988","37628","11328","2012","176","4","0","0","0","0","0"],["1088","5312","11104","12992","9316","4196","1160","180","12","0","0","0","0","0","0"],["64","320","672","768","516","204","44","4","0","0","0","0","0","0","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0"],["-180224","-917504","-1974272","-2211840","-1139712","135168","439296","-33792","-432960","-428032","-234784","-83776","-20028","-3120","-288","-12"],["-745472","-3805184","-8355840","-9906176","-6089728","-662016","1643008","720384","-659808","-982672","-612640","-234840","-59128","-9620","-924","-40"],["-1597440","-8133632","-17977344","-21837312","-14444288","-2850048","3259968","2720352","320016","-762132","-629860","-263808","-68928","-11404","-1104","-48"],["-2242048","-11368192","-25207552","-31172096","-21826208","-5992240","3487712","4214104","1665204","28396","-281736","-147316","-40260","-6544","-600","-24"],["-2254656","-11391040","-25326240","-31826752","-23491380","-8312764","1627452","3525016","1871000","460868","1136","-36340","-11844","-1856","-144","-4"],["-1687360","-8505984","-18968928","-24204960","-18755316","-8042816","-498376","1633344","1084204","351956","58468","1480","-1272","-220","-12","0"],["-953216","-4803584","-10746432","-13891456","-11199160","-5490096","-1224592","299708","341528","127528","25892","2752","96","-4","0","0"],["-404864","-2043968","-4585600","-5980768","-4954520","-2639956","-834876","-89700","43216","22180","4648","484","20","0","0","0"],["-126528","-641600","-1442080","-1886272","-1580580","-875964","-316548","-68256","-5728","916","272","20","0","0","0","0"],["-27712","-141568","-318304","-414304","-344772","-190728","-70432","-16888","-2444","-180","-4","0","0","0","0","0"],["-3840","-19840","-44544","-57088","-46064","-24280","-8360","-1812","-224","-12","0","0","0","0","0","0"],["-256","-1344","-3008","-3744","-2832","-1332","-380","-60","-4","0","0","0","0","0","0","0"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","0","0","0","0","0","0","0","0","0","0"],["49152","245760","516096","540672","168960","-304128","-506880","-405504","-209088","-73920","-17952","-2880","-276","-12"],["274432","1384448","2989056","3390464","1661440","-811008","-2082432","-1820544","-980496","-357280","-89012","-14628","-1436","-64"],["648192","3315712","7387136","9038848","5839232","437760","-2894784","-3048000","-1753692","-661944","-168868","-28280","-2824","-128"],["933120","4835840","11056832","14321600","10869872","3762560","-1334092","-2519380","-1619740","-633724","-163140","-27216","-2688","-120"],["914432","4785600","11149312","15018400","12536736","6136476","962312","-932800","-822468","-342960","-87856","-14056","-1292","-52"],["639552","3370112","7943840","10953760","9640580","5453920","1777652","109512","-192664","-101336","-26180","-3836","-292","-8"],["323136","1710912","4055328","5650560","5095140","3066284","1206820","274764","13756","-11728","-3708","-480","-24","0"],["116608","619776","1469440","2045184","1847000","1126432","465932","126572","20396","1308","-100","-16","0","0"],["28800","153664","362816","499104","442472","263476","106240","28424","4764","440","16","0","0","0"],["4416","23680","55456","74528","63412","35456","13036","3040","408","24","0","0","0","0"],["320","1728","4000","5184","4116","2052","628","108","8","0","0","0","0","0"]]},"deriv_order":2},{"coeff":{"coeffs":[["0","0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","0","0","0","0","0","0"],["-24576","-135168","-337920","-506880","-506880","-354816","-177408","-63360","-15840","-2640","-264","-12"],["-88064","-484352","-1215488","-1837056","-1857792","-1319808","-672000","-245184","-62808","-10756","-1108","-52"],["-141824","-780032","-1958528","-2963136","-3001440","-2137296","-1091832","-400164","-103128","-17800","-1852","-88"],["-136320","-749760","-1876992","-2823264","-2834952","-1995420","-1004604","-361776","-91332","-15396","-1560","-72"],["-85632","-470976","-1172352","-1743264","-1719912","-1181292","-575684","-198716","-47492","-7456","-688","-28"],["-36096","-198528","-489984","-715968","-687312","-454104","-209912","-67472","-14624","-1996","-148","-4"],["-9984","-54912","-134016","-191232","-176688","-110376","-47136","-13548","-2496","-264","-12","0"],["-1664","-9152","-22016","-30432","-26664","-15372","-5836","-1408","-196","-12","0","0"],["-128","-704","-1664","-2208","-1800","-924","-292","-52","-4","0","0","0"]]},"deriv_order":3}]]},{"annihilator":{"terms":[{"coeff":{"coeffs":[["0","0","0"],["-4","-5","-1"],["-3","-2","-1"],["-1","-1","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["8","12","6","1"],["6","9","5","1"],["2","3","1","0"]]},"deriv_order":1,"shift":0}]},"quotient":[{"coeff":{"coeffs":[["-128","-384","-480","-320","-120","-24","-2"],["-64","-304","-528","-456","-212","-51","-5"],["-8","-140","-326","-329","-172","-46","-5"],["56","52","-90","-165","-101","-28","-3"],["68","116","45","-32","-33","-10","-1"],["52","100","65","12","-3","-1","0"],["20","40","29","9","1","0","0"],["4","8","5","1","0","0","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","0"],["64","128","96","32","4"],["32","64","52","20","3"],["-28","-56","-47","-19","-3"],["-44","-88","-67","-23","-3"],["-20","-40","-29","-9","-1"],["-4","-8","-5","-1","0"]]},"deriv_order":1}],"step_multiplier":{"coeffs":[["2048","9216","18432","21504","16128","8064","2688","576","72","4"],["4608","20736","41856","49728","38304","19824","6888","1548","204","12"],["4992","22464","45120","53088","40344","20556","7032","1560","204","12"],["3168","14256","28344","32676","24036","11664","3716","744","84","4"],["1248","5616","10968","12180","8436","3744","1044","168","12","0"],["288","1296","2472","2604","1644","624","132","12","0","0"],["32","144","264","252","132","36","4","0","0","0"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","0","0","0","0","0","0","0","0","0","0","0"],["-24576","-135168","-337920","-506880","-506880","-354816","-177408","-63360","-15840","-2640","-264","-12"],["-103424","-565760","-1412096","-2122752","-2135424","-1509312","-764736","-277728","-70836","-12082","-1240","-58"],["-199936","-1088640","-2707392","-4059168","-4076496","-2879352","-1459668","-531126","-135954","-23318","-2412","-114"],["-235968","-1280096","-3166048","-4711920","-4688172","-3274158","-1637760","-586764","-147570","-24816","-2512","-116"],["-188560","-1020040","-2504916","-3685398","-3608310","-2467224","-1201250","-416006","-100268","-15984","-1512","-64"],["-106656","-575904","-1402224","-2031504","-1944114","-1288386","-601870","-197442","-44304","-6410","-528","-18"],["-43248","-233352","-562692","-799686","-742764","-471804","-207972","-63044","-12682","-1566","-100","-2"],["-12416","-67040","-159968","-222144","-198672","-119346","-48596","-13160","-2242","-212","-8","0"],["-2416","-13080","-30876","-41730","-35598","-19872","-7250","-1662","-216","-12","0","0"],["-288","-1568","-3664","-4800","-3858","-1950","-606","-106","-8","0","0","0"],["-16","-88","-204","-258","-192","-84","-20","-2","0","0","0","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","0","0","0","0","0","0","0","0","0"],["49152","294912","811008","1351680","1520640","1216512","709632","304128","95040","21120","3168","288","12"],["157696","946176","2609664","4375040","4965120","4018176","2377536","1036224","330120","74960","11514","1074","46"],["242176","1453056","4003840","6699520","7581888","6114048","3602592","1562976","495570","112004","17130","1592","68"],["229760","1378560","3785632","6291360","7046664","5602656","3241302","1374162","423450","92422","13548","1196","48"],["147360","884160","2414640","3968400","4369146","3391944","1901356","773784","226194","46096","6168","480","16"],["65952","395712","1072752","1736400","1866618","1400904","750112","287220","77410","14124","1614","98","2"],["20544","123264","331104","525600","547620","392784","197504","69384","16594","2548","222","8","0"],["4288","25728","68352","105920","106044","71664","33086","10290","2058","238","12","0","0"],["544","3264","8560","12880","12258","7656","3140","816","122","8","0","0","0"],["32","192","496","720","642","360","124","24","2","0","0","0","0"]]},"deriv_order":1}],[{"coeff":{"coeffs":[["0","0","0","0","0","0","0","0","0","0","0","0"],["0","12288","61440","138240","184320","161280","96768","40320","11520","2160","240","12"],["-18432","-51200","-4096","179712","367872","392448","266112","121152","37176","7416","872","46"],["-65280","-249984","-368960","-187680","166224","360168","302244","152490","49710","10332","1254","68"],["-104768","-433824","-758080","-685520","-266868","86222","170878","103908","36086","7608","912","48"],["-102368","-437120","-806416","-822000","-475582","-118956","33124","39586","15408","3220","356","16"],["-67344","-291144","-547220","-579254","-369406","-135156","-18106","6670","3780","780","72","2"],["-30928","-134120","-252436","-268502","-174994","-69794","-15174","-726","438","96","6","0"],["-9888","-42864","-80040","-83980","-53932","-21490","-5046","-572","-2","4","0","0"],["-2112","-9168","-16920","-17308","-10686","-4040","-896","-102","-4","0","0","0"],["-272","-1192","-2180","-2158","-1250","-424","-78","-6","0","0","0","0"],["-16","-72","-132","-126","-66","-18","-2","0","0","0","0","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","0","0","0","0","0","0","0","0","0"],["24576","110592","202752","168960","0","-152064","-177408","-114048","-47520","-13200","-2376","-252","-12"],["78848","354816","666624","616960","155520","-297792","-417984","-284256","-122220","-34790","-6408","-696","-34"],["133376","607104","1180224","1213408","578928","-122232","-390516","-295926","-130476","-37046","-6720","-714","-34"],["145088","666912","1332160","1474352","915340","210554","-140490","-155798","-73144","-20450","-3500","-338","-14"],["108496","502408","1021012","1179382","826202","328672","36796","-34334","-21408","-6046","-940","-74","-2"],["56752","264328","541764","638166","470784","219296","58936","4870","-2246","-836","-116","-6","0"],["20576","96400","197928","233532","173960","84236","26064","4726","358","-20","-4","0","0"],["4960","23408","47912","55804","40688","19182","5802","1070","106","4","0","0","0"],["720","3432","6980","7918","5486","2380","632","94","6","0","0","0","0"],["48","232","468","510","324","120","24","2","0","0","0","0","0"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","0","0","0","0","0","0","0"],["0","0","0","0","0","0","0","0","0","0","0"],["-12288","-61440","-138240","-184320","-161280","-96768","-40320","-11520","-2160","-240","-12"],["-30208","-151040","-340992","-457728","-404544","-245952","-104160","-30336","-5814","-662","-34"],["-34816","-174080","-391680","-522240","-456960","-274176","-114240","-32640","-6120","-680","-34"],["-23776","-118880","-265552","-348928","-298462","-173434","-69196","-18658","-3238","-324","-14"],["-10304","-51520","-113856","-146304","-120788","-66684","-24766","-6040","-906","-72","-2"],["-2816","-14080","-30688","-38272","-30080","-15424","-5142","-1068","-124","-6","0"],["-448","-2240","-4800","-5760","-4236","-1956","-554","-88","-6","0","0"],["-32","-160","-336","-384","-258","-102","-22","-2","0","0","0"]]},"deriv_order":2}]]}],"restart_bases":[],"row_multiplier":{"coeffs":[["128","384","480","320","120","24","2"],["192","576","736","512","204","44","4"],["136","408","506","332","122","24","2"],["48","144","172","104","32","4","0"],["8","24","26","12","2","0","0"]]},"start_base":2}},"shifted_parent_relation":{"terms":[{"coeff":{"coeffs":[["16","16","4"],["20","20","5"],["4","4","1"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-4","-2"],["-16","-8"],["-4","-2"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["0"],["3"],["1"]]},"deriv_order":0,"shift":2}]},"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 1) and E the input rule gauged by lambda(n)/delta(n) and composed with (or conjugated through) T = x^(d_n) P(1/x), d_n = 0 + 1 (n - 0); so the candidate rows satisfy the input rule at every base n >= 2 (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":"the schedule d_n depends on n","status":"none"},"lean_declarations":["RealRooted.X_pow_mul_reverse_eq_zero_or_splits","RealRooted.reflect_eq_zero_or_splits"],"lean_route":"reversed","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":"the schedule d_n depends on n","status":"not_proved"},"lean_replay":"not_attempted","operation":{"description":"x^(d_n) P(1/x), d_n = 0 + 1 (n - 0)","kind":"preserver_image","operator":{"schedule":{"first_degree":0,"first_index":0,"step":1},"shape":"reversal"}},"parent":{"gauge":{"kind":"none"},"index_shift":0,"recurrence":{"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"},"relation":"Q_n = lambda(n) T_n(P_(n+0)) with T = x^(d_n) P(1/x), d_n = 0 + 1 (n - 0), for every n >= 0"},"parent_proof":{"route":"liu_wang_three_term","statement":"every parent row P_n, n >= 0, is zero or real-rooted with coefficients of one sign","status":"proved"},"root_transfer":{"input_conclusion":"every Q_n, n >= 0, is zero or real-rooted with roots in (-inf, 0]","input_root_region":{"upper":{"closed":true,"value":"0"}},"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":"proved"},"notes":["the division remainder is removed by row annihilators of the shifted parent"],"parent_proof":{"attempts":[{"detail":"the leader is not a nonzero constant","route":"periodic_product","success":false,"variant":"P_(n+k) = c(x) P_n"},{"detail":"not applicable: expected one nonzero lag term","route":"product_recurrence","success":false,"variant":"product_recurrence"},{"detail":"no theorem matched (weighted_renewal_window: LHS must be a nonzero constant; fixed_delay_predecessor_window: LHS must be a nonzero constant)","route":"paper_theorem","success":false,"variant":"match_recurrence_theorems"},{"detail":"HypothesisFailed: P_n = (a_n + b_n (x + 2)) P_(n-1) - c_n (x + 2)^2 P_(n-2) for n >= 3, with a_n = (0)/(n^2 - n - 2), b_n = (2 n^2 - 6)/(n^2 - n - 2), c_n = (n^2 + n - 2)/(n^2 - n - 2); Q_n(y) = y^(d_n) P_n(1/y - 2), d_n = deg P_1 + n - 1, satisfies Q_n = (a_n y + b_n) Q_(n-1) - c_n Q_(n-2); open hypotheses: leading_coefficient_nonzero: fails at n = 3: f(n) a_n = 0 = 0 there (exact); seeds_interlace: P_1 vanishes at x = -2, so deg Q_1 < deg P_1; first_coefficient_positive: not checked: the seeds do not satisfy the seed hypothesis; recurrence_coefficient_positive: fails at n = 4: the denominator of beta_n = n^4 - 2 n^3 - 5 n^2 + 6 n vanishes there; root_region: the region contains the pole x = -2 of the coordinate change y = 1/(x + 2)","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":"HypothesisFailed: P_n = A_n(x) P_(n-1) + V_n(x) P'_(n-1) + W_n(x) P_(n-2) for n >= 3, with A_n(x) = ((4 n^2 - 12)/(n^2 - n - 2)) + ((2 n^2 - 6)/(n^2 - n - 2)) x, V_n(x) = 0, W_n(x) = ((-4 n^2 - 4 n + 8)/(n^2 - n - 2)) + ((-4 n^2 - 4 n + 8)/(n^2 - n - 2)) x + ((-n^2 - n + 2)/(n^2 - n - 2)) x^2; open hypotheses: lag_degree_step_nonnegative: fails at n = 3: mu_n = (-n^2 - n + 2)/(n^2 - n - 2) = -5/2 there (exact); multipliers_vanish_at_zero: [x^0] c_2(n, x) = -4 n^2 - 4 n + 8 is not the zero polynomial; lag_coefficient_nonpositive: W_n is not separable with a factor of one sign on (-inf, 0), and the sufficient monomial test (-1)^k [x^k] W_n <= 0 fails for k = 1 (not a disproof): fails at n = 3: [x^1] W_n = -10 there (exact); derivative_or_lag_coefficient_negative: W_n is not separable with a factor of one sign on (-inf, 0), and the sufficient monomial test (-1)^k [x^k] W_n <= 0 fails for k = 1 (not a disproof): fails at n = 3: [x^1] W_n = -10 there (exact)","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":"P_n = A_n(x) P_(n-1) + B_n(x) P_(n-2) for n >= 3, with A_n(x) = ((4 n^2 - 12)/(n^2 - n - 2)) + ((2 n^2 - 6)/(n^2 - n - 2)) x, B_n(x) = ((-4 n^2 - 4 n + 8)/(n^2 - n - 2)) + ((-4 n^2 - 4 n + 8)/(n^2 - n - 2)) x + ((-n^2 - n + 2)/(n^2 - n - 2)) x^2: every P_n, n >= 0, is nonzero and real-rooted with every root in (-inf, 0) (so its coefficients have one sign); for n >= 2, P_(n-1) interlaces P_n (weakly, in the sense of Liu and Wang), and deg P_n - deg P_(n-1) is 0 or 1 for n >= 3","route":"liu_wang_three_term","success":true,"variant":"liu_wang_three_term"}],"conditional_on":[],"interlacing":{"from_index":2,"justification":{"premises":["every hypothesis of the theorem is verified exactly for every index: P_n = A_n(x) P_(n-1) + B_n(x) P_(n-2) for n >= 3, with A_n(x) = ((4 n^2 - 12)/(n^2 - n - 2)) + ((2 n^2 - 6)/(n^2 - n - 2)) x, B_n(x) = ((-4 n^2 - 4 n + 8)/(n^2 - n - 2)) + ((-4 n^2 - 4 n + 8)/(n^2 - n - 2)) x + ((-n^2 - n + 2)/(n^2 - n - 2)) x^2","every P_n, n >= 0, is nonzero and real-rooted with every root in (-inf, 0) (so its coefficients have one sign); for n >= 2, P_(n-1) interlaces P_n (weakly, in the sense of Liu and Wang), and deg P_n - deg P_(n-1) is 0 or 1 for n >= 3"],"theorem":"liu_wang_three_term: L. L. Liu and Y. Wang, Adv. Appl. Math. 38 (2007) 542-560, Theorem 2.1 and Corollary 2.4 (A unified approach to polynomial sequences with only real zeros; the lag row as the interlacer, b_n = 0), weak interlacing of consecutive rows, with nonnegativity of the coefficients replaced, where a root region is certified, by an exact root-location induction; Proposition 3.3 (the case B_n(x) = -(c_n x + d_n)^2)"},"kind":"weak","orientation":"previous_interlaces_next"},"route":"liu_wang_three_term","rows_checked":10,"statement":"every parent row P_n, n >= 0, is zero or real-rooted with coefficients of one sign","status":"proved"},"rows_compared":16,"schema":"polytool.recurrence-preserver-image.v1","statement":"proved: Q_n = lambda(n) T_n(P_(n+0)) with T = x^(d_n) P(1/x), d_n = 0 + 1 (n - 0) for every n >= 0, the side conditions hold for every n, and every parent row P_n, n >= 0, is zero or real-rooted with coefficients of one sign; so every Q_n, n >= 0, is zero or real-rooted with roots in (-inf, 0]"},"kind":"preserver_image"}