{"certification":{"candidate":{"gauge":{"kind":"none"},"index_shift":0,"operator":{"coefficients":[{"denominator":["1"],"numerator":["1"]},{"denominator":["1"],"numerator":["1"]}],"shape":"derivative_polynomial"},"parent":{"first_index":0,"initial_polynomials":[["1"],["1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","3"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["2","3"]]},"deriv_order":0,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent_name":"basis_map_A013610 of Square array A(n,r), the number of neighbors at a sharp Manhattan distance r in a finite n-hypercube lattice, read by upwards antidiagonals; A(n,r) = Sum_{k=0..min(n,r)} binomial(r-1,k-1)*binomial(n,k)* 2^k."},"identifying_rows":1,"identity":{"certificate":{"certificate":{"dividend_relation":{"terms":[{"coeff":{"coeffs":[["-96","-342","-54","405","243"],["-408","-1476","-324","1296","729"],["72","378","1296","729","0"],["216","486","0","0","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-256","-1902","-5922","-10314","-9639","-4374","-729"],["-744","-4068","-7398","-6966","-3402","-729","0"],["-72","-486","-162","243","0","0","0"],["216","486","0","0","0","0","0"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["-160","-1560","-5868","-10719","-9882","-4374","-729"],["-336","-2592","-7074","-8262","-4131","-729","0"],["-144","-864","-1458","-486","0","0","0"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["96","342","54","-405","-243"],["-72","-630","-864","0","243"],["0","216","648","243","0"],["0","162","0","0","0"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["96","342","54","-405","-243"],["-72","-630","-864","0","243"],["0","216","648","243","0"],["0","162","0","0","0"]]},"deriv_order":1,"shift":1}]},"exceptional_bases":[],"gauge":{"kind":"none"},"identifying_indices":[0],"index_shift":0,"input":{"first_index":0,"initial_polynomials":[["1"]],"recurrence":{"denominator":{"coeffs":[["168","1026","1566","-162","-486"],["-72","-576","-2160","-486","243"],["0","-270","648","243","0"],["0","162","0","0","0"]]},"terms":[{"coeff":{"coeffs":[["-168","-1026","-1566","162","486"],["-96","774","2916","162","-729"],["576","1080","-1296","-729","0"],["-216","-486","0","0","0"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["-32","-168","252","2943","5751","3645","729"],["48","864","4158","7290","4131","729","0"],["144","864","1458","486","0","0","0"]]},"deriv_order":1,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"input_valid_from_base":0,"multiplier":["1"],"operator":{"coefficients":[{"denominator":["1"],"numerator":["1"]},{"denominator":["1"],"numerator":["1"]}],"shape":"derivative_polynomial"},"parent":{"first_index":0,"initial_polynomials":[["1"],["1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","3"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["2","3"]]},"deriv_order":0,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent_leader_shift":2,"parent_valid_from_base":0,"quotients":[],"row_annihilation":{"kind":"system","system":{"generators":[{"annihilator":{"terms":[{"coeff":{"coeffs":[["-6","0"],["-12","-18"],["0","-18"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["8","12","-54","-54"],["0","24","72","27"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","-8","-48","-81","-27"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["6"]]},"deriv_order":0,"shift":1}]},"quotient":[{"coeff":{"coeffs":[["147456","2737152","21897216","98039808","264819456","422108496","309679200","-152346420","-586002276","-599111154","-315675954","-86093442","-9565938"],["-110592","-3068928","-33841152","-201553920","-723494592","-1620094608","-2206070640","-1563381324","-48183984","867311712","691936182","229582512","28697814"],["0","663552","13685760","119625984","580027392","1707749568","3123770832","3443029092","2000343924","242337096","-366694290","-191318760","-28697814"],["0","248832","2488320","1928448","-77822208","-475856208","-1338234048","-2088445032","-1818236808","-788658444","-92470734","38263752","9565938"],["0","0","-746496","-9331200","-44229888","-89019648","-18580752","230054904","393974928","268909146","82904796","9565938","0"],["0","0","0","559872","6718464","31492800","71803584","80070444","38263752","6377292","0","0","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["147456","2737152","21897216","98039808","264819456","422108496","309679200","-152346420","-586002276","-599111154","-315675954","-86093442","-9565938"],["-110592","-3068928","-33841152","-201553920","-723494592","-1620094608","-2206070640","-1563381324","-48183984","867311712","691936182","229582512","28697814"],["0","663552","13685760","119625984","580027392","1707749568","3123770832","3443029092","2000343924","242337096","-366694290","-191318760","-28697814"],["0","248832","2488320","1928448","-77822208","-475856208","-1338234048","-2088445032","-1818236808","-788658444","-92470734","38263752","9565938"],["0","0","-746496","-9331200","-44229888","-89019648","-18580752","230054904","393974928","268909146","82904796","9565938","0"],["0","0","0","559872","6718464","31492800","71803584","80070444","38263752","6377292","0","0","0"]]},"deriv_order":1}],"step_multiplier":{"coeffs":[["-884736","-19906560","-200060928","-1183942656","-4578633216","-12138584832","-22507274304","-29233506528","-26214921648","-15709395960","-5930881560","-1262703816","-114791256"],["0","3981312","83607552","774862848","4165447680","14355677952","33090114816","51647562144","54079436160","36847993176","15420292056","3558528936","344373768"],["0","0","-5971968","-116453376","-987614208","-4766750208","-14383391616","-28060084800","-35381216016","-28047330216","-13200994440","-3328946424","-344373768"],["0","0","0","2985984","53747712","413185536","1763596800","4546300608","7210591488","6874720776","3711583944","1033121304","114791256"]]},"step_quotients":[[{"coeff":{"coeffs":[["884736","22560768","259780608","1784125440","8130461184","25874484480","58923028800","96755329440","113915441232","94354160904","53059069440","19055348496","3902902704","344373768"],["1769472","43794432","483729408","3142748160","13322714112","38632847616","78104663424","110114575200","106509279456","68266785096","27282055176","6083936568","573956280","0"],["0","-5308416","-137355264","-1567641600","-10415858688","-44734892544","-130281934464","-262374075072","-365724941616","-347575168584","-218001349728","-85175111952","-18596183472","-1721868840"],["0","0","0","32845824","636014592","5351256576","25597347840","76463258688","147511015488","183780800856","143948235024","67038093504","16759523376","1721868840"],["0","0","0","11943936","214990848","1652742144","7054387200","18185202432","28842365952","27498883104","14846335776","4132485216","459165024","0"],["0","0","0","0","-8957952","-161243136","-1239556608","-5290790400","-13638901824","-21631774464","-20624162328","-11134751832","-3099363912","-344373768"]]},"deriv_order":0},{"coeff":{"coeffs":[["-1179648","-31850496","-388841472","-2834694144","-13719103488","-46308132864","-111249365760","-189833559552","-223252459200","-164653176384","-49258203408","33570065088","45170359236","22212108036","5337793404","516560652"],["0","1769472","45121536","503635968","3209932800","12659825664","30438001152","35430659712","-24983868096","-177300055008","-337494795696","-365750450784","-244658430288","-98950062672","-22039921152","-2066242608"],["0","0","7962624","191102976","2087202816","13732540416","60677807616","189803326464","431036914752","715855278528","863000662608","738643468608","431270748792","160822549656","34093003032","3099363912"],["0","0","0","-19906560","-447897600","-4492412928","-26464029696","-101537826048","-265968033408","-484838584416","-615663769680","-536763913056","-311390413776","-113643343440","-23417416224","-2066242608"],["0","0","0","0","11943936","250822656","2311151616","12254478336","41207698944","91334158848","134484333696","129790646784","79607736036","29558748420","6026540940","516560652"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","1179648","33619968","437944320","3451797504","18366787584","69697345536","194257668096","403510947840","627293115936","726600306960","619035231384","379174650444","161013868416","44653798584","7231849128","516560652"],["0","0","-5308416","-143327232","-1755758592","-12899450880","-63301367808","-218686003200","-546130501632","-996603512832","-1327913752464","-1277830752624","-868912412292","-402917308560","-120186445032","-20662426080","-1549681956"],["0","0","0","7962624","203046912","2329067520","15855575040","71168689152","221275971072","487281795840","763982575488","845896765464","647900980740","331517147328","107100241848","19629304776","1549681956"],["0","0","0","0","-3981312","-95551488","-1021206528","-6395977728","-25990377984","-71652418560","-136162270080","-177747882624","-156326558796","-89460652176","-31567595400","-6198727824","-516560652"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","0","-663552","-14929920","-148552704","-858843648","-3187071360","-7912251072","-13284607824","-14910108696","-10815887232","-4770214416","-1147912560","-114791256"],["0","0","-1327104","-26873856","-237385728","-1197006336","-3784174848","-7751007936","-10266022944","-8524313640","-4170748968","-1084139640","-114791256","0"],["0","0","0","5971968","116453376","987614208","4766750208","14383391616","28060084800","35381216016","28047330216","13200994440","3328946424","344373768"],["0","0","0","1990656","32845824","221709312","762545664","1267270272","260760384","-2627444304","-4400331480","-3022836408","-956593800","-114791256"],["0","0","0","0","-2985984","-53747712","-413185536","-1763596800","-4546300608","-7210591488","-6874720776","-3711583944","-1033121304","-114791256"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","-663552","-14929920","-151538688","-917070336","-3680878464","-10295626176","-20476303632","-28940151096","-28506495240","-18793879524","-7748409780","-1779264468","-172186884"],["0","0","884736","21233664","232906752","1546739712","6937933824","22170931200","51791799168","89134701696","112210578504","100999299168","62287010964","24507933156","5452584660","516560652"],["0","0","0","-3981312","-89579520","-900274176","-5327741952","-20603849472","-54623631744","-101282734368","-131550779376","-117967147416","-70692281820","-26688967020","-5682167172","-516560652"],["0","0","0","0","3981312","83607552","770383872","4084826112","13735899648","30444719616","44828111232","43263548928","26535912012","9852916140","2008846980","172186884"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","-589824","-15925248","-195084288","-1433272320","-7033485312","-24298444800","-60681166848","-110733723648","-147545972496","-141981194736","-96545823588","-44768589840","-13354049448","-2295825120","-172186884"],["0","0","0","1769472","45121536","517570560","3523461120","15815264256","49172438016","108284843520","169773905664","187977058992","143977995720","73670477184","23800053744","4362067728","344373768"],["0","0","0","0","-1327104","-31850496","-340402176","-2131992576","-8663459328","-23884139520","-45387423360","-59249294208","-52108852932","-29820217392","-10522531800","-2066242608","-172186884"]]},"deriv_order":2}]]},{"annihilator":{"terms":[{"coeff":{"coeffs":[["0","0"],["0","-54"],["0","0"],["0","54"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-48","-234","-324","-162"],["24","180","432","243"],["0","-72","-216","-81"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["-16","-120","-306","-297","-81"],["0","24","144","243","81"]]},"deriv_order":2,"shift":0}]},"quotient":[{"coeff":{"coeffs":[["92160","1516032","10623744","41357952","98358624","151311240","167742900","171635760","184705272","161912358","89636382","26572050","3188646"],["193536","2861568","18137088","65930112","158548752","279615240","372183660","329414688","114555060","-89636382","-114791256","-45703926","-6377292"],["82944","829440","1928448","-9310464","-73238256","-230527296","-441459072","-549864288","-417830724","-154826478","-1062882","15943230","3188646"],["0","-124416","-1617408","-8429184","-21461760","-21012696","27031320","110460996","145496736","91762146","27634932","3188646","0"],["0","0","0","186624","2239488","10497600","23934528","26690148","12754584","2125764","0","0","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","-73728","-1257984","-9061632","-35427456","-79268544","-92151432","-16612452","101091888","141363306","87510618","26572050","3188646"],["0","55296","1340928","13022208","67651200","207129312","380450520","394132392","165573396","-72630270","-112665492","-45703926","-6377292"],["0","0","-248832","-4458240","-33592320","-138148416","-335958192","-487272348","-399407436","-152700714","-1062882","15943230","3188646"],["0","0","-124416","-1430784","-5505408","-3219264","35534376","111878172","145496736","91762146","27634932","3188646","0"],["0","0","0","186624","2239488","10497600","23934528","26690148","12754584","2125764","0","0","0"]]},"deriv_order":1}],"step_multiplier":{"coeffs":[["-884736","-19906560","-200060928","-1183942656","-4578633216","-12138584832","-22507274304","-29233506528","-26214921648","-15709395960","-5930881560","-1262703816","-114791256"],["0","3981312","83607552","774862848","4165447680","14355677952","33090114816","51647562144","54079436160","36847993176","15420292056","3558528936","344373768"],["0","0","-5971968","-116453376","-987614208","-4766750208","-14383391616","-28060084800","-35381216016","-28047330216","-13200994440","-3328946424","-344373768"],["0","0","0","2985984","53747712","413185536","1763596800","4546300608","7210591488","6874720776","3711583944","1033121304","114791256"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","0","0","0","0","0","0","0","0","0","0","0","0","0"],["0","-15925248","-358318080","-3601096704","-21310967808","-82415397888","-218494526976","-405130937472","-526203117504","-471868589664","-282769127280","-106755868080","-22728668688","-2066242608"],["0","-23887872","-465813504","-3896709120","-18018920448","-48645038592","-69339587328","-12074339520","140351442336","265626966384","239110186248","117431454888","29960517816","3099363912"],["0","-7962624","-71663616","349360128","8169652224","53482332672","192554537472","431966582208","626301092736","587348593200","348659308224","125352051552","24794911296","2066242608"],["0","0","35831808","591224832","3883272192","11790904320","7936185600","-58795797888","-210960819360","-338787260208","-301901003280","-150835710384","-39258609552","-4132485216"],["0","0","0","-53747712","-967458816","-7437339648","-31744742400","-81833410944","-129790646784","-123744973968","-66808510992","-18596183472","-2066242608","0"],["0","0","0","0","26873856","483729408","3718669824","15872371200","40916705472","64895323392","61872486984","33404255496","9298091736","1033121304"]]},"deriv_order":0},{"coeff":{"coeffs":[["3538944","98205696","1234206720","9295368192","46778425344","166016604672","427354776576","808081313472","1123894261152","1139554055952","825489431064","412368455304","133731813240","25139285064","2066242608","0"],["-3538944","-100859904","-1337720832","-10874953728","-60125773824","-237571605504","-687651586560","-1473674083200","-2340670237344","-2736691567488","-2321551115928","-1395861672960","-573784093116","-152041018572","-23245229340","-1549681956"],["0","26542080","652935168","7321632768","49546432512","225713516544","730844591616","1730345442048","3034627312320","3949695021168","3785573285784","2622827144592","1269820873872","404294803632","75417855192","6198727824"],["0","0","-71663616","-1660207104","-17288847360","-106917636096","-437089830912","-1244650883328","-2535112453248","-3734389140192","-3975182931528","-3017632537728","-1584234124056","-541699937064","-107444615616","-9298091736"],["0","0","0","83607552","1845338112","18099542016","103901045760","387028876032","980572417920","1723484420640","2106572602608","1769507211240","993288738168","352983112200","71285369976","6198727824"],["0","0","0","0","-35831808","-752467968","-6933454848","-36763435008","-123623096832","-274002476544","-403453001088","-389371940352","-238823208108","-88676245260","-18079622820","-1549681956"]]},"deriv_order":1},{"coeff":{"coeffs":[["2359296","67239936","875888640","6903595008","36733575168","139394691072","388515336192","807021895680","1254586231872","1453200613920","1238070462768","758349300888","322027736832","89307597168","14463698256","1033121304","0"],["0","-14155776","-387514368","-4825350144","-36154294272","-181703098368","-646464043008","-1675034007552","-3203739869184","-4537706852736","-4735462426128","-3594930518736","-1943358568452","-723414495312","-175286247912","-24794911296","-1549681956"],["0","0","31850496","836075520","9925410816","70409502720","332241481728","1098609951744","2612955096576","4517775689472","5675534788320","5129294219352","3269771531532","1422952409376","399817944648","65086642152","4649045868"],["0","0","0","-31850496","-800243712","-9029615616","-60358680576","-265486823424","-807132750336","-1734169927680","-2647443491712","-2850343413984","-2122624246572","-1057686632784","-333698181192","-59921035632","-4649045868"],["0","0","0","0","11943936","286654464","3063619584","19187933184","77971133952","214957255680","408486810240","533243647872","468979676388","268381956528","94702786200","18596183472","1549681956"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["884736","19906560","198070272","1145124864","4249428480","10549668096","17712810432","19880144928","14421182976","6360285888","1530550080","153055008","0","0"],["1769472","38486016","376233984","2202163200","8713847808","25058191104","54870535296","93270966048","121321603008","115471500480","75328573104","30993639120","7117057872","688747536"],["0","-5308416","-105504768","-922669056","-4691727360","-15523011072","-35743068288","-60477513408","-78423685488","-78096317832","-56030887512","-25751505096","-6543101592","-688747536"],["0","0","7962624","134369280","922669056","3140881920","4353564672","-4992238656","-30576989376","-53990154072","-49628086344","-25062757560","-6543101592","-688747536"],["0","0","0","-11943936","-206032896","-1491499008","-5814830592","-12894412032","-15203464128","-5867108640","5777826552","7002266616","2640198888","344373768"],["0","0","0","0","8957952","161243136","1239556608","5290790400","13638901824","21631774464","20624162328","11134751832","3099363912","344373768"]]},"deriv_order":0},{"coeff":{"coeffs":[["-1179648","-31850496","-391495680","-2896404480","-14370048000","-50431030272","-128724090624","-242058699648","-336044552256","-341842691664","-250104637656","-127124938728","-42204918456","-8150179176","-688747536","0"],["0","5308416","132710400","1502945280","10185191424","45961012224","145437949440","331195920768","548704093248","661804185888","576775043064","357434462016","152997612372","42874534116","7059662244","516560652"],["0","0","-13271040","-306561024","-3180072960","-19559688192","-79348419072","-223528336128","-448715712960","-649004252256","-676783736208","-504022895928","-261284030532","-89020619028","-17735249052","-1549681956"],["0","0","0","19906560","435953664","4241590272","24152878080","89283347712","224760334464","393504425568","481179435984","406973266272","231782677740","84084595020","17390875284","1549681956"],["0","0","0","0","-11943936","-250822656","-2311151616","-12254478336","-41207698944","-91334158848","-134484333696","-129790646784","-79607736036","-29558748420","-6026540940","-516560652"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","-1179648","-31850496","-390168576","-2866544640","-14066970624","-48596889600","-121362333696","-221467447296","-295091944992","-283962389472","-193091647176","-89537179680","-26708098896","-4591650240","-344373768","0"],["0","0","5308416","138018816","1620393984","11346739200","52730984448","171240210432","398613187584","671748982272","818592035472","713899575648","436978425132","181905877008","48786283800","7576222896","516560652"],["0","0","0","-7962624","-199065600","-2233516032","-14834368512","-64772711424","-195285593088","-415629377280","-627820305408","-668148882840","-491574421944","-242056495152","-75532646448","-13430576952","-1033121304"],["0","0","0","0","3981312","95551488","1021206528","6395977728","25990377984","71652418560","136162270080","177747882624","156326558796","89460652176","31567595400","6198727824","516560652"]]},"deriv_order":2}]]}],"restart_bases":[],"row_multiplier":{"coeffs":[["9216","138240","870912","2985984","6030288","7243344","4960116","1732104","236196"],["0","-27648","-373248","-2052864","-5878656","-9272880","-7820712","-3149280","-472392"],["0","0","20736","248832","1166400","2659392","2965572","1417176","236196"]]},"start_base":0}},"shifted_parent_relation":{"terms":[{"coeff":{"coeffs":[["-1","-3"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-2","-3"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["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 0) and E the input rule gauged by lambda(n)/delta(n) and composed with (or conjugated through) T = phi(n, D) = 1 + (1) D; so the candidate rows satisfy the input rule at every base n >= 0 (the exceptional bases checked exactly), and agreement on the 1 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":["RealRooted.splits_add_C_mul_derivative_all","RealRooted.splits_C_mul_add_derivative","Polynomial.Splits.derivative"],"lift_summary":{"hypotheses":[{"evidence":"the polynomial with ascending coefficients [1, 1] is fixed; exact check: real-rooted = true, coefficients of one sign = true","name":"derivative_polynomial_real_rooted","statement":"the polynomial in D is real-rooted for every n >= n0","status":{"kind":"verified"}},{"evidence":"lambda(n) = 1","name":"gauge_finite_nonzero","statement":"lambda(n) is finite and nonzero for every n >= n0","status":{"kind":"verified"}},{"evidence":"delta(n) != 0 for every integer n in [0, +inf) (exact; Taylor shift: the coefficients of delta(n) at n = 0 + u have one sign)","name":"operator_coefficients_defined","sign_decision":{"certificate":{"condition":"nonzero","denominator":["1"],"method":{"kind":"taylor_shift","shifted_denominator":["1"],"shifted_numerator":["1"]},"numerator":["1"],"range":{"first":"0","last":null}},"decision":"holds"},"statement":"the operator coefficients are finite at every n >= n0 (their denominators do not vanish)","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":"phi(n, D) = 1 + (1) D","kind":"preserver_image","operator":{"coefficients":[{"denominator":["1"],"numerator":["1"]},{"denominator":["1"],"numerator":["1"]}],"shape":"derivative_polynomial"}},"parent":{"gauge":{"kind":"none"},"index_shift":0,"recurrence":{"first_index":0,"initial_polynomials":[["1"],["1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","3"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["2","3"]]},"deriv_order":0,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"relation":"Q_n = lambda(n) T_n(P_(n+0)) with T = phi(n, D) = 1 + (1) D, 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":"Laguerre's theorem on differential operators: if phi is a real polynomial with only real roots, then phi(D) maps every real-rooted polynomial to a real-rooted polynomial or zero (write phi(D) = C D^j prod (1 + c_i D); D preserves real-rootedness by Rolle's theorem and p + c p' is real-rooted for every real c by Rolle's theorem applied to e^(x/c) p; Polya--Schur 1914); when the coefficients of phi have one sign, coefficients of one sign stay of one sign; applied to phi(n, .) for each n"},"verdict":"proved"},"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":"not applicable: expected one nonzero lag term","route":"product_recurrence","success":false,"variant":"product_recurrence"},{"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: c_2(n, x) = gamma(n) w(x) with w neither constant nor a constant times a square (x + v_0)^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 >= 2, with A_n(x) = (2) + (3) x, V_n(x) = 0, W_n(x) = (1) + (3) x; open hypotheses: seed_degree_step: degrees 0 and 0 (exact); seed_strict_interlacing: the Bezout test fails or the degrees do not differ by one (exact); multipliers_vanish_at_zero: [x^0] c_2(n, x) = 1 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 = 0 (not a disproof): fails at n = 2: [x^0] W_n = 1 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 = 0 (not a disproof): fails at n = 2: [x^0] W_n = 1 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 >= 2, with A_n(x) = (2) + (3) x, B_n(x) = (1) + (3) x: every P_n, n >= 0, is nonzero and real-rooted with every root in (-inf, -1/3] (so its coefficients have one sign); for n >= 1, 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 >= 2","route":"liu_wang_three_term","success":true,"variant":"liu_wang_three_term"}],"conditional_on":[],"interlacing":{"from_index":1,"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 >= 2, with A_n(x) = (2) + (3) x, B_n(x) = (1) + (3) x","every P_n, n >= 0, is nonzero and real-rooted with every root in (-inf, -1/3] (so its coefficients have one sign); for n >= 1, 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 >= 2"],"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"},"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 = phi(n, D) = 1 + (1) D 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"}