{"certification":{"candidate":{"gauge":{"kind":"none"},"index_shift":0,"operator":{"coefficients":[{"denominator":["1"],"numerator":["0"]},{"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":[["-40","80","-40","0"],["-88","154","-18","-6"],["-64","28","17","-5"],["-16","-8","7","-1"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","-48","108","-72","12"],["0","-96","160","-74","10"],["0","-32","48","-18","2"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["8","-16","8"],["24","-50","14"],["32","-36","7"],["16","-8","1"]]},"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":[["0","6","0"],["8","-2","3"],["-16","-12","4"],["16","-8","1"]]},"terms":[{"coeff":{"coeffs":[["0","38","12","-2"],["8","-74","31","-1"],["16","-52","4","2"],["16","8","-7","1"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","-16","4","16","-4"],["0","32","-64","38","-6"],["0","32","-48","18","-2"]]},"deriv_order":1,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"input_valid_from_base":0,"multiplier":["1"],"operator":{"coefficients":[{"denominator":["1"],"numerator":["0"]},{"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","32768","-212992","591872","-913408","849920","-483328","161792","-28672","2048"],["0","0","163840","-1024000","2684928","-3831296","3226112","-1625088","474112","-73216","4608"],["0","0","360448","-2048000","4808704","-6056960","4447360","-1940480","491776","-66560","3712"],["0","0","425984","-2105344","4272128","-4621312","2903168","-1085344","237344","-28000","1376"],["0","0","262144","-1097728","1880064","-1710080","903680","-286656","53872","-5536","240"],["0","0","65536","-229376","323584","-241664","106240","-28544","4624","-416","16"]]},"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","73728","-331776","594432","-534528","248832","-55296","4608"],["0","0","221184","-854016","1288704","-958848","366720","-68736","4992"],["0","0","196608","-651264","832512","-521472","169152","-27264","1728"],["0","0","49152","-147456","165888","-89088","24768","-3456","192"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","32768","-188416","456704","-604672","473600","-222208","60416","-8704","512"],["0","0","131072","-737280","1699840","-2083840","1475328","-615680","148736","-19200","1024"],["0","0","229376","-1138688","2297856","-2452480","1512832","-554976","119264","-13856","672"],["0","0","196608","-819200","1396736","-1265664","666880","-211072","39600","-4064","176"],["0","0","65536","-229376","323584","-241664","106240","-28544","4624","-416","16"]]},"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","98304","-442368","792576","-712704","331776","-73728","6144"],["0","0","196608","-737280","1069056","-752640","267264","-46080","3072"],["0","0","98304","-294912","331776","-178176","49536","-6912","384"]]},"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) 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 [0, 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) D","kind":"preserver_image","operator":{"coefficients":[{"denominator":["1"],"numerator":["0"]},{"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) 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) 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"}