{"certification":{"candidate":{"gauge":{"kind":"none"},"index_shift":0,"operator":{"intercept":"1","shape":"affine","slope":"1"},"parent":{"first_index":0,"initial_polynomials":[["1"],["4","2"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","2"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["3","2"]]},"deriv_order":0,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent_name":"basis_map_A013609 of Riordan array ((1+x)/(1-2x),x(1+x)/(1-2x))."},"identifying_rows":1,"identity":{"certificate":{"certificate":{"dividend_relation":{"terms":[{"coeff":{"coeffs":[["-32","-16"],["20","16"],["-12","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-56","-112","-32"],["26","40","8"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["-13","-46","-44","-8"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["8"],["4"]]},"deriv_order":0,"shift":1}]},"exceptional_bases":[],"gauge":{"kind":"none"},"identifying_indices":[0],"index_shift":0,"input":{"first_index":0,"initial_polynomials":[["1"]],"recurrence":{"denominator":{"coeffs":[["4"],["4"]]},"terms":[{"coeff":{"coeffs":[["96","32"],["-60","-16"],["12","0"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["274","232","40"],["-74","-56","-8"]]},"deriv_order":1,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["111","158","68","8"]]},"deriv_order":2,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"input_valid_from_base":0,"multiplier":["1"],"operator":{"intercept":"1","shape":"affine","slope":"1"},"parent":{"first_index":0,"initial_polynomials":[["1"],["4","2"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","2"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["3","2"]]},"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":[["-64","-32","0"],["52","8","-32"],["-12","24","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-82","-92","104","48"],["26","-12","-72","-16"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["-13","-20","48","80","16"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["16"]]},"deriv_order":0,"shift":1}]},"quotient":[{"coeff":{"coeffs":[["208","1152","2176","1536","256"],["0","416","1472","1408","256"],["-52","-80","192","320","64"]]},"deriv_order":0}],"step_multiplier":{"coeffs":[["71991296","1196163072","8884322304","38852886528","110875901952","216149262336","292737253376","274508808192","174373994496","71873593344","17918066688","2415919104","134217728"],["-107986944","-1362296832","-7013400576","-17599561728","-14556069888","37515952128","134310002688","197828542464","166308347904","82694897664","23353884672","3422552064","201326592"],["53993472","465174528","1214054400","-641728512","-9038069760","-15237906432","836763648","33722204160","47229960192","30500978688","10015997952","1610612736","100663296"],["-8998912","-41533440","35782656","440074240","412286976","-1297612800","-2623537152","-94371840","3557818368","3544186880","1409286144","251658240","16777216"]]},"step_quotients":[[{"coeff":{"coeffs":[["107986944","1938227200","15574827008","73655648256","226250981376","468269924352","649652600832","564939194368","225104101376","-92459237376","-178123702272","-104287174656","-30802968576","-4563402752","-268435456"],["-35995648","85835776","6561431552","58993803264","269242859520","750982004736","1352669855744","1563003191296","1056960413696","248072110080","-198029869056","-190354292736","-66706210816","-10804527104","-671088640"],["-161980416","-2745360384","-19051069440","-67899555840","-115191054336","14458159104","488986902528","1057209974784","1132418039808","611560980480","73622618112","-91150614528","-47513075712","-8959033344","-603979776"],["161980416","1782476800","6849929216","5690130432","-34546057216","-108989186048","-85605875712","142718533632","381413228544","351299174400","138435100672","5444206592","-11525947392","-3036676096","-234881024"],["-56243200","-372070400","-277528576","3280814080","8006156288","-3836641280","-33441841152","-30788812800","26303791104","66812641280","45994737664","12100567040","432013312","-293601280","-33554432"],["6749184","17651712","-89137152","-276381696","350896128","1591640064","21233664","-3864526848","-2809921536","2678587392","4259315712","1925185536","364904448","25165824","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["-251969536","-4654514176","-38726205440","-191196889088","-620448448512","-1381741363200","-2130093015040","-2209522647040","-1376843202560","-250496417792","367874015232","367572025344","163410083840","39795556352","5100273664","268435456"],["494940160","7359725568","46401798144","155262976000","258450063360","-1553989632","-1002458316800","-2376518860800","-2980303601664","-2248172109824","-974961770496","-173090537472","35047604224","23353884672","4227858432","268435456"],["-364455936","-4111810560","-17053949952","-21707882496","61631594496","271316680704","349976788992","-105545465856","-933332779008","-1359520727040","-1041695244288","-465668407296","-119814488064","-16307453952","-905969664","0"],["119235584","919273472","1507717120","-5974540288","-24448974848","-13495828480","73422798848","147392299008","43248254976","-179411353600","-273899585536","-185216270336","-68404903936","-14126415872","-1526726656","-67108864"],["-14623232","-60742656","129792000","884183040","220422144","-4433952768","-5585403904","7241269248","18955763712","6139150336","-16283860992","-20154679296","-10047455232","-2554331136","-327155712","-16777216"]]},"deriv_order":1},{"coeff":{"coeffs":[["-58492928","-1061871616","-8497741824","-38724927488","-105947004928","-152039718912","27740864512","652720209920","1585019092992","2226997166080","2084002856960","1337639043072","584367210496","168543911936","30400315392","3087007744","134217728"],["87739392","1241849856","7077298176","18439569408","5866586112","-101514608640","-294701236224","-306455248896","193542488064","1027476553728","1500034105344","1245481795584","645402722304","209480318976","41070624768","4429185024","201326592"],["-43869696","-445446144","-1405906944","669327360","14167621632","28288647168","-10741284864","-119991042048","-163244408832","6293028864","264873443328","347546320896","227687792640","85286977536","18371051520","2113929216","100663296"],["7311616","44994560","-4153344","-571883520","-994394112","1996554240","7226654720","1964769280","-16719151104","-22025338880","2002780160","26361200640","25178406912","11324620800","2717908992","335544320","16777216"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","35995648","382107648","1429602304","1190920192","-6881017856","-22209363968","-19759366144","23597154304","76449579008","83307266048","47345303552","14428405760","2214592512","134217728"],["-53993472","-537165824","-1690304512","263454720","13131186176","25577390080","-4621074432","-75472306176","-89961529344","-3548381184","75262590976","66370666496","24461180928","4160749568","268435456"],["-31496192","-469327872","-2323849216","-3301900288","9648635904","40958820352","40320761856","-48135929856","-149804285952","-134765084672","-38962987008","13170114560","10729029632","2315255808","167772160"],["42744832","282773504","206602240","-2513354752","-6067503104","3127083008","25613697024","22776643584","-21250179072","-50822905856","-33248247808","-7495221248","348127232","343932928","33554432"],["-6749184","-17651712","89137152","276381696","-350896128","-1591640064","-21233664","3864526848","2809921536","-2678587392","-4259315712","-1925185536","-364904448","-25165824","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["-8998912","-167518208","-1157611520","-3539042304","-2091188224","18123456512","56239587328","55828807680","-46547337216","-197323128832","-254900436992","-181604974592","-76755763200","-18891145216","-2483027968","-134217728"],["125984768","1436364800","5964414976","7288340480","-23142072320","-96395395072","-114742263808","59673673728","341229699072","445050257408","293605474304","98377400320","10401873920","-2801795072","-872415232","-67108864"],["-89989120","-680802304","-1047388160","4607664128","17737646080","8059387904","-55389061120","-103465746432","-22271754240","133262999552","189613998080","122089897984","42865786880","8346664960","838860800","33554432"],["14623232","60742656","-129792000","-884183040","-220422144","4433952768","5585403904","-7241269248","-18955763712","-6139150336","16283860992","20154679296","10047455232","2554331136","327155712","16777216"]]},"deriv_order":1},{"coeff":{"coeffs":[["-29246464","-413949952","-2359099392","-6146523136","-1955528704","33838202880","98233745408","102151749632","-64514162688","-342492184576","-500011368448","-415160598528","-215134240768","-69826772992","-13690208256","-1476395008","-67108864"],["29246464","296964096","937271296","-446218240","-9445081088","-18859098112","7160856576","79994028032","108829605888","-4195352576","-176582295552","-231697547264","-151791861760","-56857985024","-12247367680","-1409286144","-67108864"],["-7311616","-44994560","4153344","571883520","994394112","-1996554240","-7226654720","-1964769280","16719151104","22025338880","-2002780160","-26361200640","-25178406912","-11324620800","-2717908992","-335544320","-16777216"]]},"deriv_order":2}]]},{"annihilator":{"terms":[{"coeff":{"coeffs":[["0","0","0"],["-40","-80","-64"],["76","56","-32"],["-12","24","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["60","264","336","96"],["-134","-276","-72","16"],["26","-12","-72","-16"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["26","144","272","192","32"],["-13","-20","48","80","16"]]},"deriv_order":2,"shift":0}]},"quotient":[{"coeff":{"coeffs":[["-104","-576","-1088","-768","-128"],["52","80","-192","-320","-64"]]},"deriv_order":0}],"step_multiplier":{"coeffs":[["71991296","1196163072","8884322304","38852886528","110875901952","216149262336","292737253376","274508808192","174373994496","71873593344","17918066688","2415919104","134217728"],["-107986944","-1362296832","-7013400576","-17599561728","-14556069888","37515952128","134310002688","197828542464","166308347904","82694897664","23353884672","3422552064","201326592"],["53993472","465174528","1214054400","-641728512","-9038069760","-15237906432","836763648","33722204160","47229960192","30500978688","10015997952","1610612736","100663296"],["-8998912","-41533440","35782656","440074240","412286976","-1297612800","-2623537152","-94371840","3557818368","3544186880","1409286144","251658240","16777216"]]},"step_quotients":[[{"coeff":{"coeffs":[["107986944","1794244608","12894535680","51102351360","113007919104","91106574336","-226149531648","-885132361728","-1494862528512","-1539242459136","-1019366866944","-427617681408","-107307073536","-14495514624","-805306368"],["179978240","4106272768","39527481344","214504439808","728376016896","1598450565120","2197266366464","1549161988096","-285711794176","-1784168841216","-1805522042880","-938081255424","-266824843264","-38990249984","-2281701376"],["-251969536","-2908725248","-8171438080","43774181376","421971492864","1555050921984","3293043752960","4250455244800","3113725460480","760253251584","-679338835968","-668454617088","-239746416640","-39493566464","-2483027968"],["-80990208","-2560536576","-24618786816","-111163637760","-244448231424","-113838194688","740509483008","2022410551296","2468682399744","1537182007296","330458726400","-137078243328","-92912222208","-18773704704","-1308622848"],["173229056","2198849536","9837142016","12512542720","-41106817024","-166091325440","-170388357120","167448674304","595465076736","614804750336","282383613952","37618712576","-11471421440","-4018143232","-335544320"],["-62992384","-443715584","-437592064","3771891712","10295705600","-2954559488","-41248751616","-42665508864","28547481600","85480964096","63000543232","18631098368","1577058304","-218103808","-33554432"],["6749184","17651712","-89137152","-276381696","350896128","1591640064","21233664","-3864526848","-2809921536","2678587392","4259315712","1925185536","364904448","25165824","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["-215973888","-3696476160","-27583315968","-115099238400","-277118189568","-295221067776","361192488960","1996414255104","3874857418752","4573347446784","3577976193024","1874602229760","642231828480","136298102784","16106127360","805306368"],["-44994560","-3231301632","-47144288256","-335598977024","-1440132169728","-4064075317248","-7828228800512","-10356667711488","-9167661170688","-4954215415808","-1079450271744","451877535744","410924351488","127842385920","18723373056","1073741824"],["508438528","9419784192","72468504576","297226141696","655929409536","468482260992","-1493825355776","-5220621877248","-8141966671872","-7641761841152","-4503896064000","-1615897559040","-316795781120","-22951231488","1711276032","268435456"],["-425198592","-5391040512","-25715109888","-44835717120","62249484288","421869256704","694701588480","83828146176","-1440234602496","-2545699258368","-2232255774720","-1144428429312","-348710240256","-61102620672","-5586812928","-201326592"],["133858816","1097001984","2097838080","-6457233408","-30939881472","-23366221824","85871132672","198560120832","83180519424","-219420557312","-374469033984","-268497321984","-103991476224","-22460497920","-2541748224","-117440512"],["-14623232","-60742656","129792000","884183040","220422144","-4433952768","-5585403904","7241269248","18955763712","6139150336","-16283860992","-20154679296","-10047455232","-2554331136","-327155712","-16777216"]]},"deriv_order":1},{"coeff":{"coeffs":[["58492928","1529815040","17928601600","125568581632","589433733120","1966589214720","4817675878400","8816186359808","12131032367104","12524953010176","9603920166912","5366184148992","2122166829056","569586483200","97509179392","9529458688","402653184"],["-146232320","-3005636608","-26913669120","-136460140544","-417921433600","-709673484288","-183737778176","2304425590784","6533618860032","9935465218048","9836045533184","6596037967872","2982871564288","883655966720","162671886336","16777216000","738197504"],["131609088","2038253568","12748689408","37548466176","25900793856","-174740570112","-600143757312","-732901539840","223840567296","2061246136320","3264941654016","2838509912064","1518493237248","504247615488","100512301056","10972299264","503316480"],["-51181312","-548933632","-1878695936","320552960","17895768064","39714750464","-7095058432","-158023286784","-234378362880","-13634633728","355167371264","489756295168","328762130432","125040590848","27212644352","3154116608","150994944"],["7311616","44994560","-4153344","-571883520","-994394112","1996554240","7226654720","1964769280","-16719151104","-22025338880","2002780160","26361200640","25178406912","11324620800","2717908992","335544320","16777216"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["107986944","1830240256","13852573696","62101258240","185273417728","395048648704","638648320000","824302370816","870632652800","733277585408","458932355072","194716368896","50465865728","7046430720","402653184"],["125984768","2633220096","22719004672","108752404480","323395387392","632717312000","857335136256","894280138752","870353731584","843629723648","663597613056","342624305152","101636374528","15502147584","939524096"],["-175478784","-1907769344","-6943006720","-3251109888","43387486208","110882455552","39733297152","-232557379584","-394378346496","-186944323584","105870524416","155155693568","64651001856","11609833472","771751936"],["-29246464","-688416768","-4309786624","-8463663104","12987285504","80694378496","102455574528","-63180374016","-301465337856","-319800475648","-134656032768","-3577741312","13115588608","3447717888","268435456"],["49494016","354418688","366665728","-3004432384","-8357052416","2245001216","33420607488","34653339648","-23493869568","-69491228672","-50254053376","-14025752576","-796917760","268435456","33554432"],["-6749184","-17651712","89137152","276381696","-350896128","-1591640064","-21233664","3864526848","2809921536","-2678587392","-4259315712","-1925185536","-364904448","-25165824","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["-224972800","-4007976960","-32285114368","-156121464832","-508633612288","-1191570178048","-2099703971840","-2878626856960","-3133697687552","-2706762629120","-1806725808128","-887808327680","-301033586688","-64860717056","-7851737088","-402653184"],["98988032","699838464","-820019200","-23137468416","-91834220544","-136903983104","75007787008","633514229760","1102926839808","962384101376","394323296256","-9315549184","-79473672192","-32061259776","-5368709120","-335544320"],["157480960","2243151872","11789533184","23348994048","-22981738496","-199687110656","-350360436736","-63615664128","695764254720","1246783602688","1076451344384","530547998720","150416130048","23244832768","1677721600","33554432"],["-104612352","-858530816","-1637509120","5090357248","24228552704","17929781248","-67837394944","-154633568256","-62204018688","173272203264","290183446528","205370949632","78452359168","16680747008","1853882368","83886080"],["14623232","60742656","-129792000","-884183040","-220422144","4433952768","5585403904","-7241269248","-18955763712","-6139150336","16283860992","20154679296","10047455232","2554331136","327155712","16777216"]]},"deriv_order":1},{"coeff":{"coeffs":[["29246464","647921664","6138642432","32578404352","103991476224","185877921792","70492880896","-550568460288","-1649533255680","-2569489350656","-2584014225408","-1752799641600","-799501451264","-238370684928","-44090523648","-4563402752","-201326592"],["-58492928","-944885760","-6140026880","-18885787648","-15311667200","82655510528","301862092800","386449276928","-84712882176","-1031671906304","-1676616400896","-1477179342848","-797194584064","-266338304000","-53317992448","-5838471168","-268435456"],["36558080","400451584","1410060288","-97443840","-13173227520","-30285201408","3514630144","118026272768","179963559936","15732310016","-266876223488","-373907521536","-252866199552","-96611598336","-21088960512","-2449473536","-117440512"],["-7311616","-44994560","4153344","571883520","994394112","-1996554240","-7226654720","-1964769280","16719151104","22025338880","-2002780160","-26361200640","-25178406912","-11324620800","-2717908992","-335544320","-16777216"]]},"deriv_order":2}]]}],"restart_bases":[],"row_multiplier":{"coeffs":[["416","2304","4352","3072","512"],["-208","-320","768","1280","256"]]},"start_base":0}},"shifted_parent_relation":{"terms":[{"coeff":{"coeffs":[["-1","-2"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-3","-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 = P((1) x + (1)); 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":["Polynomial.Splits.comp_of_degree_le_one"],"lift_summary":{"hypotheses":[{"evidence":"lambda(n) = 1","name":"gauge_finite_nonzero","statement":"lambda(n) is finite and nonzero for every n >= n0","status":{"kind":"verified"}}],"identity":{"method":"forward_division","status":"certified"},"input_first_index":0,"input_interlacing":{"reason":"no parent theorem report with an interlacing conclusion","status":"not_proved"},"lean_replay":"not_attempted","operation":{"description":"P((1) x + (1))","kind":"preserver_image","operator":{"intercept":"1","shape":"affine","slope":"1"}},"parent":{"gauge":{"kind":"none"},"index_shift":0,"recurrence":{"first_index":0,"initial_polynomials":[["1"],["4","2"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","2"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["3","2"]]},"deriv_order":0,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"relation":"Q_n = lambda(n) T_n(P_(n+0)) with T = P((1) x + (1)), for every n >= 0"},"parent_proof":{"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, -1]","input_root_region":{"upper":{"closed":true,"value":"-1"}},"parent_hypothesis":"every parent row used is zero or real-rooted with all roots in (-inf, 0] (coefficients of one sign)","parent_root_region":{"upper":{"closed":true,"value":"0"}},"theorem":"a real affine substitution x -> a x + b (a != 0), the reversal x^d p(1/x) (d >= deg p) and a real Mobius map (c x + e)^d p((a x + b)/(c x + e)) (a e - b c != 0, d >= deg p) map real roots to real roots: a root r of p gives the root (r - b)/a, 1/r (and 0) or (e r - b)/(a - c r) (and -e/c); for an input row that is a polynomial the degree condition holds automatically"},"verdict":"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) = (3) + (2) x, V_n(x) = 0, W_n(x) = (1) + (2) x; open hypotheses: 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) = (3) + (2) x, B_n(x) = (1) + (2) x: every P_n, n >= 0, is nonzero and real-rooted with every root in (-inf, -1/2] (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) = (3) + (2) x, B_n(x) = (1) + (2) x","every P_n, n >= 0, is nonzero and real-rooted with every root in (-inf, -1/2] (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 = P((1) x + (1)) 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, -1]"},"kind":"preserver_image"}
