{"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":[["4","1"],["4","5"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["2","0"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["-1","1"]]},"deriv_order":0,"offset":2,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent_name":"veronese_section_2_0 of The truncated (4,4,1)-Pascal triangle, given by 4*C(n-2, k) + 4*C(n-2, k-1) + C(n-2, k-2) for n>=2."},"identifying_rows":1,"identity":{"certificate":{"certificate":{"dividend_relation":{"terms":[{"coeff":{"coeffs":[["-72","216","-212","56","20","-8"],["-120","266","-28","-18","18","-4"],["-64","-36","-15","23","-4","0"],["-16","-8","7","-1","0","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-72","232","-200","-60","160","-68","8"],["-120","170","4","100","-44","4","0"],["-64","-68","33","5","-2","0","0"],["-16","-8","7","-1","0","0","0"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","16","12","-116","140","-60","8"],["0","-96","32","118","-62","8","0"],["0","-32","48","-18","2","0","0"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["40","-136","168","-88","16"],["56","-130","40","-18","4"],["32","28","-25","4","0"],["16","-8","1","0","0"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["40","-136","168","-88","16"],["56","-130","40","-18","4"],["32","28","-25","4","0"],["16","-8","1","0","0"]]},"deriv_order":1,"shift":1}]},"exceptional_bases":[],"gauge":{"kind":"none"},"identifying_indices":[0],"index_shift":0,"input":{"first_index":0,"initial_polynomials":[["5","1"]],"recurrence":{"denominator":{"coeffs":[["0","30","102","-66","12"],["40","-210","93","-26","4"],["-16","52","-28","4","0"],["16","-8","1","0","0"]]},"terms":[{"coeff":{"coeffs":[["0","78","206","-98","2","4"],["40","-314","-23","67","-26","4"],["16","12","36","-26","4","0"],["16","8","-7","1","0","0"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","-80","-28","252","-204","68","-8"],["0","32","64","-154","66","-8","0"],["0","32","-48","18","-2","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":[["4","1"],["4","5"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["2","0"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["-1","1"]]},"deriv_order":0,"offset":2,"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":[["-32","-2","-2"],["-16","16","-3"],["-16","8","-1"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["32","-80","10","2"],["0","64","-32","4"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","64","-96","36","-4"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["24"]]},"deriv_order":0,"shift":1}]},"quotient":[{"coeff":{"coeffs":[["0","0","3932160","-31064064","108380160","-219267072","283852800","-244629504","141410304","-53821440","12828672","-1720320","98304"],["0","0","13369344","-93782016","281886720","-479072256","511967232","-362311680","173826048","-56291328","11747328","-1413120","73728"],["0","0","18087936","-103415808","243990528","-313761792","248183808","-132566016","51929088","-15144960","3038208","-359424","18432"],["0","0","13369344","-55246848","85819392","-59793408","14515200","3449088","-2428416","253440","82944","-22272","1536"],["0","0","6291456","-20054016","23101440","-9977856","-1511424","3319296","-1447296","311040","-34176","1536","0"],["0","0","1572864","-5505024","7766016","-5799936","2549760","-685056","110976","-9984","384","0","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","3932160","-31064064","108380160","-219267072","283852800","-244629504","141410304","-53821440","12828672","-1720320","98304"],["0","0","13369344","-93782016","281886720","-479072256","511967232","-362311680","173826048","-56291328","11747328","-1413120","73728"],["0","0","18087936","-103415808","243990528","-313761792","248183808","-132566016","51929088","-15144960","3038208","-359424","18432"],["0","0","13369344","-55246848","85819392","-59793408","14515200","3449088","-2428416","253440","82944","-22272","1536"],["0","0","6291456","-20054016","23101440","-9977856","-1511424","3319296","-1447296","311040","-34176","1536","0"],["0","0","1572864","-5505024","7766016","-5799936","2549760","-685056","110976","-9984","384","0","0"]]},"deriv_order":1}],"step_multiplier":{"coeffs":[["0","0","0","-3623878656","24461180928","-71345111040","117379694592","-119248257024","76950798336","-31255953408","7644119040","-1019215872","56623104"],["0","0","0","-10871635968","65229815808","-167151403008","238496514048","-207283027968","113005559808","-38475399168","7898923008","-891813888","42467328"],["0","0","0","-10871635968","57076088832","-126382768128","153901596672","-113005559808","51820756992","-14906032128","2611740672","-254803968","10616832"],["0","0","0","-3623878656","16307453952","-30576476160","31255953408","-19237699584","7453016064","-1834057728","278691840","-23887872","884736"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","0","0","2415919104","-19629342720","70892126208","-149768110080","204933169152","-189956358144","121187598336","-52985069568","15500574720","-2883059712","306708480","-14155776"],["0","0","0","14495514624","-107206410240","350006280192","-663509532672","808464678912","-662323986432","371015811072","-141780713472","36196319232","-5885263872","549715968","-22413312"],["0","0","0","31406948352","-210486951936","618701783040","-1049226117120","1136991928320","-824627036160","407956193280","-137722429440","31151554560","-4509204480","377192448","-13860864"],["0","0","0","31406948352","-189951639552","501001224192","-758579724288","731315699712","-471164387328","207268872192","-62424096768","12657917952","-1651949568","125337600","-4202496"],["0","0","0","14495514624","-79121350656","187384725504","-253784752128","218423623680","-125696212992","49532829696","-13424541696","2462994432","-292515840","20312064","-626688"],["0","0","0","2415919104","-12079595520","25971130368","-31708938240","24517804032","-12683575296","4508614656","-1107689472","185241600","-20164608","1290240","-36864"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","-4831838208","35030827008","-108112379904","180740947968","-165735825408","56665571328","45680689152","-69320835072","41433956352","-14066122752","2807562240","-306708480","14155776"],["0","0","0","-14495514624","84557168640","-186327760896","143445196800","146370723840","-457939353600","506759086080","-325052006400","131949527040","-34327756800","5547884544","-507248640","20054016"],["0","0","0","-14495514624","54358179840","-8153726976","-300102451200","746575626240","-926849433600","705116897280","-350156390400","115736739840","-25259212800","3498246144","-278691840","9732096"],["0","0","0","-4831838208","-4831838208","118380036096","-368729653248","574045028352","-541147004928","332547489792","-137725083648","38802972672","-7343013888","894320640","-63406080","1990656"],["0","0","0","0","-9663676416","48318382080","-103884521472","126835752960","-98071216128","50734301184","-18034458624","4430757888","-740966400","80658432","-5160960","147456"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","-9663676416","79725330432","-293534171136","635688714240","-898608660480","870155550720","-589588070400","280709038080","-93003448320","20903362560","-3029336064","254803968","-9437184"],["0","0","0","0","-28991029248","217432719360","-722963791872","1404252979200","-1768339537920","1516083609600","-905297264640","379020902400","-110521221120","21941452800","-2824077312","212336640","-7077888"],["0","0","0","0","-28991029248","195689447424","-581632524288","1003361402880","-1116041379840","842127114240","-442191052800","163154165760","-42122280960","7449477120","-859963392","58392576","-1769472"],["0","0","0","0","-9663676416","57982058496","-152202903552","230720274432","-224906969088","148805517312","-68768759808","22465216512","-5171724288","821624832","-85819392","5308416","-147456"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","0","0","9663676416","-64021856256","185723781120","-310294609920","330678927360","-235481333760","114254807040","-37813616640","8387297280","-1191444480","97910784","-3538944"],["0","0","0","22951231488","-143747186688","393719316480","-620589219840","623915827200","-419506421760","192531824640","-60427468800","12749045760","-1728184320","135954432","-4718592"],["0","0","0","22951231488","-135593459712","348420833280","-512722206720","479526912000","-299483136000","127769149440","-37372354560","7374274560","-938557440","69599232","-2285568"],["0","0","0","12079595520","-65229815808","152806883328","-204749144064","174455783424","-99486793728","38892994560","-10468196352","1909149696","-225570816","15593472","-479232"],["0","0","0","2415919104","-12079595520","25971130368","-31708938240","24517804032","-12683575296","4508614656","-1107689472","185241600","-20164608","1290240","-36864"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","-4831838208","24159191040","-40164655104","0","98241085440","-168453734400","150882877440","-84226867200","30700339200","-7313817600","1098252288","-94371840","3538944"],["0","0","0","-9663676416","38654705664","-28387049472","-115662127104","331471650816","-419350708224","317634379776","-156070969344","50983796736","-11003756544","1508769792","-119144448","4128768"],["0","0","0","-4831838208","4831838208","62813896704","-230418284544","377902596096","-365275643904","227709812736","-95165743104","26977591296","-5127634944","626540544","-44531712","1400832"],["0","0","0","0","-9663676416","48318382080","-103884521472","126835752960","-98071216128","50734301184","-18034458624","4430757888","-740966400","80658432","-5160960","147456"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","-9663676416","72477573120","-240987930624","468084326400","-589446512640","505361203200","-301765754880","126340300800","-36840407040","7313817600","-941359104","70778880","-2359296"],["0","0","0","0","-19327352832","130459631616","-387755016192","668907601920","-744027586560","561418076160","-294794035200","108769443840","-28081520640","4966318080","-573308928","38928384","-1179648"],["0","0","0","0","-9663676416","57982058496","-152202903552","230720274432","-224906969088","148805517312","-68768759808","22465216512","-5171724288","821624832","-85819392","5308416","-147456"]]},"deriv_order":2}]]},{"annihilator":{"terms":[{"coeff":{"coeffs":[["8","-16","8"],["24","-50","14"],["32","-36","7"],["16","-8","1"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-32","56","-16","-8"],["-32","16","70","-18"],["0","-64","32","-4"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","-64","144","-96","16"],["0","-64","96","-36","4"]]},"deriv_order":2,"shift":0}]},"quotient":[{"coeff":{"coeffs":[["0","0","3342336","-27230208","92418048","-173629440","200687616","-149336064","72585216","-22855680","4497408","-503808","24576"],["0","0","12386304","-67289088","159903744","-219890688","195010560","-117276672","48599040","-13685760","2494464","-264192","12288"],["0","0","13369344","-49250304","71000064","-50731008","19318272","-4831488","1703424","-758784","207360","-28416","1536"],["0","0","5898240","-16908288","15482880","-1449984","-6600192","5050368","-1785216","346368","-35712","1536","0"],["0","0","1572864","-5505024","7766016","-5799936","2549760","-685056","110976","-9984","384","0","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","3932160","-28114944","88031232","-158330880","180338688","-135254016","67313664","-21860352","4423680","-503808","24576"],["0","0","9437184","-58589184","151683072","-217522176","194291712","-115673088","47603712","-13455360","2476032","-264192","12288"],["0","0","8650752","-38338560","65175552","-54140928","23811072","-6554880","1993728","-777216","207360","-28416","1536"],["0","0","4718592","-13369344","11501568","688128","-7194624","5133312","-1789824","346368","-35712","1536","0"],["0","0","1572864","-5505024","7766016","-5799936","2549760","-685056","110976","-9984","384","0","0"]]},"deriv_order":1}],"step_multiplier":{"coeffs":[["0","0","0","-3623878656","24461180928","-71345111040","117379694592","-119248257024","76950798336","-31255953408","7644119040","-1019215872","56623104"],["0","0","0","-10871635968","65229815808","-167151403008","238496514048","-207283027968","113005559808","-38475399168","7898923008","-891813888","42467328"],["0","0","0","-10871635968","57076088832","-126382768128","153901596672","-113005559808","51820756992","-14906032128","2611740672","-254803968","10616832"],["0","0","0","-3623878656","16307453952","-30576476160","31255953408","-19237699584","7453016064","-1834057728","278691840","-23887872","884736"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","0","0","-12079595520","98146713600","-354460631040","748840550400","-1024665845760","949781790720","-605937991680","264925347840","-77502873600","14415298560","-1533542400","70778880"],["0","0","0","-56774098944","427919671296","-1427506200576","2773399633920","-3474945736704","2937949913088","-1704560689152","676784111616","-179919912960","30497439744","-2970353664","126222336"],["0","0","0","-109924319232","766450335744","-2354992644096","4195998498816","-4802078048256","3695981101056","-1947924135936","702268932096","-169786146816","26258374656","-2343665664","91717632"],["0","0","0","-112340238336","722661801984","-2039262216192","3322473873408","-3463875919872","2422184214528","-1158585679872","379389616128","-83516424192","11802820608","-966721536","34873344"],["0","0","0","-64021856256","378997309440","-979277709312","1454364426240","-1377399472128","873379528704","-378860765184","112725762048","-22619934720","2925637632","-220262400","7335936"],["0","0","0","-19327352832","105092481024","-247933698048","334529298432","-286909267968","164589207552","-64681279488","17488576512","-3202080768","379625472","-26320896","811008"],["0","0","0","-2415919104","12079595520","-25971130368","31708938240","-24517804032","12683575296","-4508614656","1107689472","-185241600","20164608","-1290240","36864"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","9663676416","-66437775360","185421791232","-244611809280","70892126208","264840413184","-465031397376","393997713408","-202923048960","65970634752","-13188464640","1476919296","-70778880"],["0","0","0","33822867456","-193273528320","389264965632","-127439732736","-861860265984","1879660560384","-2011008466944","1324647972864","-566305357824","157209329664","-27291156480","2687238144","-114425856"],["0","0","0","43486543872","-182401892352","104790491136","827074805760","-2424318197760","3349327380480","-2815813877760","1545363947520","-564439449600","135886602240","-20692795392","1805156352","-68714496"],["0","0","0","24159191040","-41070624768","-272998858752","1218982182912","-2272964640768","2477005996032","-1737734750208","815055962112","-258143182848","54508879872","-7354073088","573603840","-19685376"],["0","0","0","4831838208","24159191040","-222264557568","610925543424","-897023213568","815089582080","-488119468032","198318882816","-55059111936","10299359232","-1242759168","87441408","-2727936"],["0","0","0","0","9663676416","-48318382080","103884521472","-126835752960","98071216128","-50734301184","18034458624","-4430757888","740966400","-80658432","5160960","-147456"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","19327352832","-166698418176","645050400768","-1477032542208","2222570078208","-2307929407488","1689888227328","-875931107328","317910417408","-78583431168","12542017536","-1160773632","47185920"],["0","0","0","0","67645734912","-536334041088","1897100476416","-3947007836160","5362774179840","-4996705812480","3263649546240","-1501857054720","482535014400","-105554903040","14941421568","-1231552512","44826624"],["0","0","0","0","86973087744","-630554886144","2027560108032","-3811867361280","4652720455680","-3874294333440","2252785582080","-921195970560","263164723200","-51332382720","6508118016","-483065856","15925248"],["0","0","0","0","48318382080","-318901321728","927712935936","-1568535478272","1712962142208","-1271641669632","658356830208","-240004104192","61334765568","-10754260992","1232437248","-83165184","2506752"],["0","0","0","0","9663676416","-57982058496","152202903552","-230720274432","224906969088","-148805517312","68768759808","-22465216512","5171724288","-821624832","85819392","-5308416","147456"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","0","0","-26575110144","186931740672","-578688122880","1036599164928","-1188674666496","912113270784","-475892416512","168259092480","-39430914048","5829820416","-489553920","17694720"],["0","0","0","-73685532672","486505709568","-1409613299712","2357672804352","-2520818122752","1803987320832","-880141565952","292663590912","-65082949632","9241362432","-756449280","27131904"],["0","0","0","-83349209088","518214647808","-1408782827520","2204054323200","-2200019927040","1469475717120","-670479482880","209387151360","-43993497600","5943214080","-466255872","16146432"],["0","0","0","-50734301184","295044120576","-747575967744","1086993727488","-1006758789120","624032612352","-264736014336","77117792256","-15172227072","1927065600","-142700544","4681728"],["0","0","0","-16911433728","91200946176","-213355855872","285493690368","-242941427712","138379788288","-54041444352","14532231168","-2648236032","312680448","-21602304","663552"],["0","0","0","-2415919104","12079595520","-25971130368","31708938240","-24517804032","12683575296","-4508614656","1107689472","-185241600","20164608","-1290240","36864"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","9663676416","-44694503424","46808432640","129100677120","-473369149440","706160885760","-623615016960","355522314240","-133966725120","33100922880","-5151522816","457703424","-17694720"],["0","0","0","24159191040","-94220845056","33520877568","461440548864","-1225267347456","1589042479104","-1263930310656","659061080064","-229647384576","52975632384","-7764443136","654704640","-24182784"],["0","0","0","19327352832","-44694503424","-134385500160","718056456192","-1371807940608","1494099689472","-1039589572608","482470428672","-151165329408","31597166592","-4223877120","326762496","-11132928"],["0","0","0","4831838208","14495514624","-166698418176","472614174720","-700880781312","639218221056","-383281790976","155759542272","-43233730560","8083980288","-974979072","68567040","-2138112"],["0","0","0","0","9663676416","-48318382080","103884521472","-126835752960","98071216128","-50734301184","18034458624","-4430757888","740966400","-80658432","5160960","-147456"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","19327352832","-152202903552","534522101760","-1103773040640","1488055173120","-1375516753920","891353825280","-407049338880","129843855360","-28217180160","3970695168","-325582848","11796480"],["0","0","0","0","48318382080","-347892350976","1110718808064","-2073160581120","2512367124480","-2077501685760","1200091299840","-487790346240","138602741760","-26907770880","3397386240","-251265024","8257536"],["0","0","0","0","38654705664","-253671505920","733835427840","-1234081677312","1340948348928","-990932631552","510959812608","-185619382272","47294005248","-8271101952","945782784","-63700992","1916928"],["0","0","0","0","9663676416","-57982058496","152202903552","-230720274432","224906969088","-148805517312","68768759808","-22465216512","5171724288","-821624832","85819392","-5308416","147456"]]},"deriv_order":2}]]}],"restart_bases":[],"row_multiplier":{"coeffs":[["0","0","2359296","-10616832","19021824","-17104896","7962624","-1769472","147456"],["0","0","4718592","-17694720","25657344","-18063360","6414336","-1105920","73728"],["0","0","2359296","-7077888","7962624","-4276224","1188864","-165888","9216"]]},"start_base":0}},"shifted_parent_relation":{"terms":[{"coeff":{"coeffs":[["1","-1"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-2"]]},"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":[["4","1"],["4","5"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["2","0"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["-1","1"]]},"deriv_order":0,"offset":2,"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), V_n(x) = 0, W_n(x) = (-1) + (1) x; open hypotheses: seed_degree_step: degrees 1 and 1 (exact); seed_strict_interlacing: the Bezout test fails or the degrees do not differ by one (exact); degree_step_positive: fails at n = 2: lambda_n = 0 = 0 there (exact); multipliers_vanish_at_zero: [x^0] c_2(n, x) = -1 is not the zero polynomial","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), B_n(x) = (-1) + (1) x: every P_n, n >= 0, is nonzero and real-rooted with every root in (-inf, 0) (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), B_n(x) = (-1) + (1) x","every P_n, n >= 0, is nonzero and real-rooted with every root in (-inf, 0) (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"}