{"certification":{"candidate":{"gauge":{"kind":"none"},"index_shift":0,"operator":{"intercept":"1","shape":"affine","slope":"1"},"parent":{"first_index":0,"initial_polynomials":[["1"],["3","4"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","4"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["3","4"]]},"deriv_order":0,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent_name":"basis_map_A013611 of Riordan array (1/(1-2*x), x*(1+x)/(1-2*x))."},"identifying_rows":1,"identity":{"certificate":{"certificate":{"dividend_relation":{"terms":[{"coeff":{"coeffs":[["-48","-64"],["0","64"],["-48","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-60","-288","-192"],["52","160","64"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["-13","-92","-176","-64"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["16"],["16"]]},"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":[["0"],["16"]]},"terms":[{"coeff":{"coeffs":[["224","128"],["-160","-64"],["48","0"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["816","960","256"],["-276","-288","-64"]]},"deriv_order":1,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["345","636","368","64"]]},"deriv_order":2,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"input_valid_from_base":0,"multiplier":["1","1"],"operator":{"intercept":"1","shape":"affine","slope":"1"},"parent":{"first_index":0,"initial_polynomials":[["1"],["3","4"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","4"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["3","4"]]},"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":[["-48","-64"],["0","64"],["-48","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-60","-288","-192"],["52","160","64"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["-13","-92","-176","-64"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["16"],["16"]]},"deriv_order":0,"shift":1}]},"quotient":[{"coeff":{"coeffs":[["16"],["16"]]},"deriv_order":0}],"step_multiplier":{"coeffs":[["-8998912","-83066880","143130624","3520593920","6596591616","-41523609600","-167906377728","-12079595520","910801502208","1814623682560","1443109011456","515396075520","68719476736"],["-26996736","-249200640","429391872","10561781760","19789774848","-124570828800","-503719133184","-36238786560","2732404506624","5443871047680","4329327034368","1546188226560","206158430208"],["-26996736","-249200640","429391872","10561781760","19789774848","-124570828800","-503719133184","-36238786560","2732404506624","5443871047680","4329327034368","1546188226560","206158430208"],["-8998912","-83066880","143130624","3520593920","6596591616","-41523609600","-167906377728","-12079595520","910801502208","1814623682560","1443109011456","515396075520","68719476736"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","-71991296","-664535040","1145044992","28164751360","52772732928","-332188876800","-1343251021824","-96636764160","7286412017664","14516989460480","11544872091648","4123168604160","549755813888"],["26996736","33226752","-2422996992","-7126646784","64704479232","282889027584","-492847497216","-3993514278912","-3022314799104","16415365005312","39221641347072","33088428048384","12163347382272","1649267441664"],["80990208","531628032","-3281780736","-28250210304","25124929536","532030685184","514590769152","-3921036705792","-8487123812352","5527622909952","30562987278336","29996051595264","11751030521856","1649267441664"],["80990208","675610624","-1952710656","-30540300288","-31204573184","426485219328","1178968522752","-1234534662144","-8293850284032","-9045201125376","1529008357376","6906307411968","3504693313536","549755813888"],["26996736","249200640","-429391872","-10561781760","-19789774848","124570828800","503719133184","36238786560","-2732404506624","-5443871047680","-4329327034368","-1546188226560","-206158430208","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["4499456","113524736","664961024","-2240806912","-32608092160","-60175679488","363369332736","1681479696384","984487034880","-8097087094784","-22524955983872","-26319559589888","-15702400434176","-4672924418048","-549755813888"],["-20247552","-132907008","928432128","8059355136","-7998799872","-175254798336","-207806791680","1478542491648","4136657485824","-1236950581248","-18570364846080","-29274497089536","-20255065767936","-6597069766656","-824633720832"],["-53993472","-606388224","-138018816","22841131008","81826676736","-169982558208","-1505721581568","-2087354105856","5319853867008","21817360121856","30434138259456","20409684590592","6597069766656","824633720832","0"],["-29246464","-359956480","-401489920","12540968960","57217384448","-54903439360","-934545457152","-1884416901120","2167683416064","14957223608320","26479547121664","23364622090240","11149735100416","2748779069440","274877906944"]]},"deriv_order":1},{"coeff":{"coeffs":[["7311616","119235584","460328960","-2733752320","-26845315072","-43491524608","288539803648","1405649682432","1342496047104","-5906989318144","-21577110388736","-32320702644224","-26152055865344","-11836929867776","-2817498546176","-274877906944"],["14623232","238471168","920657920","-5467504640","-53690630144","-86983049216","577079607296","2811299364864","2684992094208","-11813978636288","-43154220777472","-64641405288448","-52304111730688","-23673859735552","-5634997092352","-549755813888"],["7311616","119235584","460328960","-2733752320","-26845315072","-43491524608","288539803648","1405649682432","1342496047104","-5906989318144","-21577110388736","-32320702644224","-26152055865344","-11836929867776","-2817498546176","-274877906944"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["44994560","1063256064","9584640000","36152803328","-7483686912","-585457729536","-2290089984000","-4184371888128","-3687497859072","-962072674304","592705486848","412316860416","68719476736"],["107986944","2832580608","27754561536","115022757888","23596105728","-1696755351552","-7135517736960","-13650345590784","-12719008776192","-4068407771136","1378684502016","1185410973696","206158430208"],["53993472","2118205440","25755844608","128151453696","115690438656","-1577519677440","-7666013306880","-15844805443584","-16032039174144","-6432787267584","579820584960","1082331758592","206158430208"],["-35995648","-8306688","6586564608","55845847040","130657812480","-406604218368","-3085833338880","-7476061667328","-8657043456000","-4508641918976","-605590388736","257698037760","68719476736"],["-26996736","-357187584","-999358464","6564347904","46047166464","59617837056","-265247784960","-1097229926400","-1656515198976","-1182189748224","-399431958528","-51539607552","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["-33745920","-842436608","-8251736064","-36699242496","-30540038144","446576984064","2303025217536","5428368900096","6949995282432","4409052364800","517543559168","-901943132160","-463856467968","-68719476736"],["-38245376","-1207930880","-14194212864","-76702416896","-131513188352","666324959232","4633279856640","12850072387584","19705645498368","17083500855296","7617124499456","1159641169920","-223338299392","-68719476736"],["24747008","111448064","-3633217536","-43307106304","-171406262272","-7081033728","2357484060672","9415038074880","18561305149440","20939844616192","13681618321408","5025111736320","944892805120","68719476736"],["29246464","476942336","2309259264","-3303931904","-70433112064","-226829008896","27229421568","1993334587392","5805654933504","8265396125696","6582037381120","2963527434240","704374636544","68719476736"]]},"deriv_order":1},{"coeff":{"coeffs":[["-7311616","-148482048","-1054257152","-1483276288","20912209920","127140364288","220021653504","-525563068416","-3444748320768","-7872003964928","-9910905470976","-7322919239680","-3139621093376","-721554505728","-68719476736"],["-14623232","-296964096","-2108514304","-2966552576","41824419840","254280728576","440043307008","-1051126136832","-6889496641536","-15744007929856","-19821810941952","-14645838479360","-6279242186752","-1443109011456","-137438953472"],["-7311616","-148482048","-1054257152","-1483276288","20912209920","127140364288","220021653504","-525563068416","-3444748320768","-7872003964928","-9910905470976","-7322919239680","-3139621093376","-721554505728","-68719476736"]]},"deriv_order":2}]]},{"annihilator":{"terms":[{"coeff":{"coeffs":[["0","0","0"],["128","320","-256"],["-48","192","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-112","-416","256","512"],["52","-48","-576","-256"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["-13","-40","192","640","256"]]},"deriv_order":2,"shift":0}]},"quotient":[],"step_multiplier":{"coeffs":[["-8998912","-83066880","143130624","3520593920","6596591616","-41523609600","-167906377728","-12079595520","910801502208","1814623682560","1443109011456","515396075520","68719476736"],["-26996736","-249200640","429391872","10561781760","19789774848","-124570828800","-503719133184","-36238786560","2732404506624","5443871047680","4329327034368","1546188226560","206158430208"],["-26996736","-249200640","429391872","10561781760","19789774848","-124570828800","-503719133184","-36238786560","2732404506624","5443871047680","4329327034368","1546188226560","206158430208"],["-8998912","-83066880","143130624","3520593920","6596591616","-41523609600","-167906377728","-12079595520","910801502208","1814623682560","1443109011456","515396075520","68719476736"]]},"step_quotients":[[{"coeff":{"coeffs":[["-44994560","-703299584","-1798504448","23512219648","143351873536","-52856619008","-2273832861696","-4769024311296","6853962498048","38412040011776","50710678863872","19722489823232","-6253472382976","-6047313952768","-1099511627776"],["-107986944","-1968685056","-6821707776","61692444672","452512972800","45160071168","-6816062767104","-16285710680064","17684527841280","120721867014144","169578193747968","74938589380608","-12781822672896","-17317308137472","-3298534883328"],["-53993472","-1686257664","-9674096640","44004016128","497427677184","452619927552","-6805191131136","-20242986172416","11929808535552","131693360971776","204470508060672","106480829202432","-824633720832","-15668040695808","-3298534883328"],["35995648","-279658496","-6077087744","-3020423168","210723930112","558333165568","-2257525407744","-10704937549824","-1778116460544","54869280948224","103049150332928","67035849555968","11682311045120","-3573412790272","-1099511627776"],["26996736","141213696","-1426194432","-8844214272","22457352192","203729928192","5435817984","-1978637746176","-2877359652864","5485746978816","17446157156352","15771119910912","5978594476032","824633720832","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["33745920","572469248","2052177920","-15835660288","-131026124800","-103709409280","1758231265280","5850601095168","-371447562240","-35662992506880","-76445049159680","-65502546231296","-15032385536000","10788957847552","6871947673600","1099511627776"],["38245376","901967872","5142691840","-17524391936","-254998740992","-491191795712","2801530830848","13554967117824","8962455896064","-65039495069696","-186239445630976","-213558658859008","-112373524332544","-20272245637120","3023656976384","1099511627776"],["-24747008","86528000","4128849920","12458196992","-116919107584","-671255363584","328367865856","9558130950144","19039254478848","-23090012618752","-143143743782912","-230609679024128","-179649892057088","-72911364816896","-14568529068032","-1099511627776"],["-29246464","-242970624","1038336000","14146928640","7053508608","-283772977152","-714931699712","1853764927488","9705351020544","6286489944064","-33349347311616","-82553566396416","-82308753260544","-41850161332224","-10720238370816","-1099511627776"]]},"deriv_order":1},{"coeff":{"coeffs":[["7311616","89989120","-16613376","-4575068160","-15910305792","63889735680","462505902080","251490467840","-4280102682624","-11276973506560","2050846883840","53987738910720","103130754711552","92771293593600","44530220924928","10995116277760","1099511627776"],["14623232","179978240","-33226752","-9150136320","-31820611584","127779471360","925011804160","502980935680","-8560205365248","-22553947013120","4101693767680","107975477821440","206261509423104","185542587187200","89060441849856","21990232555520","2199023255552"],["7311616","89989120","-16613376","-4575068160","-15910305792","63889735680","462505902080","251490467840","-4280102682624","-11276973506560","2050846883840","53987738910720","103130754711552","92771293593600","44530220924928","10995116277760","1099511627776"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["89989120","1694564352","9998696448","-3226468352","-276025049088","-1058273230848","-228707008512","8608725073920","26003342622720","34862249541632","23398981828608","7627861917696","962072674304"],["242970624","4834492416","30425481216","882376704","-808285372416","-3299390521344","-1189840158720","25789936435200","80742432374784","110030619672576","74526272520192","24429773979648","3092376453120"],["188977152","4336091136","31284264960","22005940224","-768705822720","-3548532178944","-2197278425088","25717458862080","86207241388032","120918361767936","83184926588928","27522150432768","3504693313536"],["8998912","946962432","11286872064","28458876928","-216655724544","-1431985717248","-1739864408064","8500008714240","34200556142592","51193862684672","36386962931712","12266426597376","1580547964928"],["-26996736","-249200640","429391872","10561781760","19789774848","-124570828800","-503719133184","-36238786560","2732404506624","5443871047680","4329327034368","1546188226560","206158430208"]]},"deriv_order":0},{"coeff":{"coeffs":[["-62992384","-1301381120","-9099018240","-9625403392","199905771520","1077298593792","1396803895296","-5885984243712","-28542473601024","-54878944624640","-56762287783936","-32263794327552","-9414568312832","-1099511627776","0"],["-96738304","-2242805760","-17796546560","-31791775744","342594158592","2209500626944","3728153247744","-9887551586304","-59252630618112","-124715112857600","-140004122689536","-87892210745344","-29978871726080","-4947802324992","-274877906944"],["-4499456","-581468160","-8296038400","-34707341312","85471002624","1187105472512","3265894809600","-2117150441472","-32877840433152","-84793391841280","-109721382027264","-78993038508032","-31714038513664","-6597069766656","-549755813888"],["29246464","359956480","401489920","-12540968960","-57217384448","54903439360","934545457152","1884416901120","-2167683416064","-14957223608320","-26479547121664","-23364622090240","-11149735100416","-2748779069440","-274877906944"]]},"deriv_order":1},{"coeff":{"coeffs":[["-7311616","-119235584","-460328960","2733752320","26845315072","43491524608","-288539803648","-1405649682432","-1342496047104","5906989318144","21577110388736","32320702644224","26152055865344","11836929867776","2817498546176","274877906944"],["-14623232","-238471168","-920657920","5467504640","53690630144","86983049216","-577079607296","-2811299364864","-2684992094208","11813978636288","43154220777472","64641405288448","52304111730688","23673859735552","5634997092352","549755813888"],["-7311616","-119235584","-460328960","2733752320","26845315072","43491524608","-288539803648","-1405649682432","-1342496047104","5906989318144","21577110388736","32320702644224","26152055865344","11836929867776","2817498546176","274877906944"]]},"deriv_order":2}]]}],"restart_bases":[],"row_multiplier":{"coeffs":[["16"]]},"start_base":0}},"shifted_parent_relation":{"terms":[{"coeff":{"coeffs":[["-1","-4"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-3","-4"]]},"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"],["3","4"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","4"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["3","4"]]},"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) + (4) x, V_n(x) = 0, W_n(x) = (1) + (4) 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) + (4) x, B_n(x) = (1) + (4) x: every P_n, n >= 0, is nonzero and real-rooted with every root in (-inf, -1/4] (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) + (4) x, B_n(x) = (1) + (4) x","every P_n, n >= 0, is nonzero and real-rooted with every root in (-inf, -1/4] (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"}