{"certification":{"candidate":{"gauge":{"kind":"none"},"index_shift":0,"operator":{"coefficients":[{"denominator":["1"],"numerator":["1"]},{"denominator":["1"],"numerator":["1"]}],"shape":"derivative_polynomial"},"parent":{"first_index":0,"initial_polynomials":[["1"],["1"],["1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["2","1"]]},"deriv_order":0,"offset":3,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent_name":"shift_x_plus_one of Triangle read by rows, A007318 rows repeated three times."},"identifying_rows":3,"identity":{"certificate":{"certificate":{"dividend_relation":{"terms":[{"coeff":{"coeffs":[["288","240","-114","-135","-27"],["-58","-209","-144","-27","0"],["-48","-42","-9","0","0"],["-2","-1","0","0","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["72","132","-60","-108","-27"],["50","-101","-117","-27","0"],["-48","-42","-9","0","0"],["-2","-1","0","0","0"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["-432","-432","-108"],["108","108","27"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["-216","-324","-162","-27"]]},"deriv_order":3,"shift":0},{"coeff":{"coeffs":[["-96","-48","54","27"],["20","63","27","0"],["15","9","0","0"],["1","0","0","0"]]},"deriv_order":0,"shift":3},{"coeff":{"coeffs":[["-96","-48","54","27"],["20","63","27","0"],["15","9","0","0"],["1","0","0","0"]]},"deriv_order":1,"shift":3}]},"exceptional_bases":[],"gauge":{"kind":"none"},"identifying_indices":[0,1,2],"index_shift":0,"input":{"first_index":0,"initial_polynomials":[["1"],["1"],["1"]],"recurrence":{"denominator":{"coeffs":[["-48","-156","-27","27"],["-43","9","27","0"],["6","9","0","0"],["1","0","0","0"]]},"terms":[{"coeff":{"coeffs":[["-84","-516","-237","54","27"],["-176","-16","90","27","0"],["30","33","9","0","0"],["2","1","0","0","0"]]},"deriv_order":0,"offset":3,"sign":"none"},{"coeff":{"coeffs":[["540","432","27","-27"],["-108","-108","-27","0"]]},"deriv_order":1,"offset":3,"sign":"none"},{"coeff":{"coeffs":[["216","324","162","27"]]},"deriv_order":2,"offset":3,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"input_valid_from_base":0,"multiplier":["1"],"operator":{"coefficients":[{"denominator":["1"],"numerator":["1"]},{"denominator":["1"],"numerator":["1"]}],"shape":"derivative_polynomial"},"parent":{"first_index":0,"initial_polynomials":[["1"],["1"],["1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["2","1"]]},"deriv_order":0,"offset":3,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent_leader_shift":3,"parent_valid_from_base":0,"quotients":[{"differentiations":[{"coeff":{"coeffs":[["-20736","-41472","-19440","12960","16200","5832","729"],["4320","20088","29484","19494","6075","729","0"],["3240","6804","5346","1863","243","0","0"],["216","324","162","27","0","0","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["-20736","-41472","-19440","12960","16200","5832","729"],["4320","20088","29484","19494","6075","729","0"],["3240","6804","5346","1863","243","0","0"],["216","324","162","27","0","0","0"]]},"deriv_order":1}],"shift":0}],"row_annihilation":{"kind":"system","system":{"generators":[{"annihilator":{"terms":[{"coeff":{"coeffs":[["-2","0"],["-3","-3"],["1","1"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["36","54","18"],["-12","-18","-6"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["36","72","45","9"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["2"]]},"deriv_order":0,"shift":2}]},"quotient":[],"step_multiplier":{"coeffs":[["373248","1119744","1399680","933120","349920","69984","5832"]]},"step_quotients":[[],[{"coeff":{"coeffs":[["-746496","-2612736","-3919104","-3265920","-1632960","-489888","-81648","-5832"],["-186624","-746496","-1259712","-1166400","-641520","-209952","-37908","-2916"],["186624","746496","1259712","1166400","641520","209952","37908","2916"]]},"deriv_order":0},{"coeff":{"coeffs":[["4478976","20155392","39191040","43110144","29393280","12737088","3429216","524880","34992"],["-2239488","-10077696","-19595520","-21555072","-14696640","-6368544","-1714608","-262440","-17496"]]},"deriv_order":1},{"coeff":{"coeffs":[["6718464","33592320","73903104","94058496","76422528","41150592","14696640","3359232","446148","26244"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["2052864","9144576","17589312","19128960","12888720","5517072","1466748","221616","14580"],["-186624","-933120","-2006208","-2426112","-1807920","-851472","-247860","-40824","-2916"]]},"deriv_order":0},{"coeff":{"coeffs":[["1119744","6158592","14836608","20575296","18125856","10532592","4041576","988524","139968","8748"]]},"deriv_order":1}]]},{"annihilator":{"terms":[{"coeff":{"coeffs":[["-2","0"],["1","1"],["-1","-1"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-24","-36","-12"],["12","18","6"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["-36","-72","-45","-9"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["2"]]},"deriv_order":0,"shift":1}]},"quotient":[],"step_multiplier":{"coeffs":[["746496","2239488","2799360","1866240","699840","139968","11664"]]},"step_quotients":[[{"coeff":{"coeffs":[["746496","2239488","2799360","1866240","699840","139968","11664"]]},"deriv_order":0}],[{"coeff":{"coeffs":[["-746496","-2239488","-2799360","-1866240","-699840","-139968","-11664","0"],["-373248","-1492992","-2519424","-2332800","-1283040","-419904","-75816","-5832"],["-373248","-1492992","-2519424","-2332800","-1283040","-419904","-75816","-5832"]]},"deriv_order":0},{"coeff":{"coeffs":[["-4478976","-20155392","-39191040","-43110144","-29393280","-12737088","-3429216","-524880","-34992"],["4478976","20155392","39191040","43110144","29393280","12737088","3429216","524880","34992"]]},"deriv_order":1},{"coeff":{"coeffs":[["-13436928","-67184640","-147806208","-188116992","-152845056","-82301184","-29393280","-6718464","-892296","-52488"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["-3359232","-14556672","-27153792","-28553472","-18545760","-7628256","-1942056","-279936","-17496"],["373248","1866240","4012416","4852224","3615840","1702944","495720","81648","5832"]]},"deriv_order":0},{"coeff":{"coeffs":[["-2239488","-12317184","-29673216","-41150592","-36251712","-21065184","-8083152","-1977048","-279936","-17496"]]},"deriv_order":1}]]},{"annihilator":{"terms":[{"coeff":{"coeffs":[["0"],["-2"],["3"],["-1"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["120","60"],["-90","-45"],["18","9"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["432","432","108"],["-108","-108","-27"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["216","324","162","27"]]},"deriv_order":3,"shift":0}]},"quotient":[{"coeff":{"coeffs":[["-216","-324","-162","-27"]]},"deriv_order":0}],"step_multiplier":{"coeffs":[["161243136","725594112","1451188224","1693052928","1269789696","634894848","211631616","45349632","5668704","314928"]]},"step_quotients":[[],[{"coeff":{"coeffs":[["0","0","0","0","0","0","0","0","0","0"],["80621568","362797056","725594112","846526464","634894848","317447424","105815808","22674816","2834352","157464"],["0","0","0","0","0","0","0","0","0","0"],["-80621568","-362797056","-725594112","-846526464","-634894848","-317447424","-105815808","-22674816","-2834352","-157464"]]},"deriv_order":0},{"coeff":{"coeffs":[["3869835264","19349176320","43535646720","58047528960","50791587840","30474952704","12697896960","3627970560","680244480","75582720","3779136"],["-4353564672","-21767823360","-48977602560","-65303470080","-57140536320","-34284321792","-14285134080","-4081466880","-765275040","-85030560","-4251528"],["1451188224","7255941120","16325867520","21767823360","19046845440","11428107264","4761711360","1360488960","255091680","28343520","1417176"]]},"deriv_order":1},{"coeff":{"coeffs":[["26121388032","143667634176","359169085440","538753628160","538753628160","377127539712","188563769856","67344203520","16836050880","2806008480","280600848","12754584"],["-8707129344","-47889211392","-119723028480","-179584542720","-179584542720","-125709179904","-62854589952","-22448067840","-5612016960","-935336160","-93533616","-4251528"]]},"deriv_order":2},{"coeff":{"coeffs":[["17414258688","104485552128","287335268352","478892113920","538753628160","431002902528","251418359808","107750725632","33672101760","7482689280","1122403392","102036672","4251528"]]},"deriv_order":3}],[{"coeff":{"coeffs":[["1854296064","9311791104","21042229248","28177238016","24760899072","14920028928","6243132672","1791310464","337287888","37633896","1889568"],["-1289945088","-6369103872","-14149085184","-18623582208","-16084002816","-9523422720","-3915184896","-1103507712","-204073344","-22359888","-1102248"],["80621568","443418624","1088391168","1572120576","1481421312","952342272","423263232","128490624","25509168","2991816","157464"]]},"deriv_order":0},{"coeff":{"coeffs":[["9190858752","50791587840","127583631360","192282439680","193189432320","135867497472","68251196160","24488801280","6150543840","1029814560","103453848","4723920"],["-967458816","-5804752896","-15721205760","-25395793920","-27209779200","-20316635136","-10793212416","-4081466880","-1077053760","-188956800","-19840464","-944784"]]},"deriv_order":1},{"coeff":{"coeffs":[["2902376448","18865446912","55870746624","99769190400","119723028480","101764574208","62854589952","28434219264","9353361600","2182451040","342956592","32595048","1417176"]]},"deriv_order":2}]]}],"restart_bases":[],"row_multiplier":{"coeffs":[["216","324","162","27"]]},"start_base":0}},"shifted_parent_relation":{"terms":[{"coeff":{"coeffs":[["-2","-1"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["1"]]},"deriv_order":0,"shift":3}]},"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 3 identifying rows gives Q_n = lambda(n) T_n(P_(n+0)) for every n >= 0"},"method":"operator_division"},"status":"certified"},"input_first_index":0,"interlacing":{"reason":"no parent theorem report with an interlacing conclusion","status":"none"},"lean_declarations":["RealRooted.splits_add_C_mul_derivative_all","RealRooted.splits_C_mul_add_derivative","Polynomial.Splits.derivative"],"lift_summary":{"hypotheses":[{"evidence":"the polynomial with ascending coefficients [1, 1] is fixed; exact check: real-rooted = true, coefficients of one sign = true","name":"derivative_polynomial_real_rooted","statement":"the polynomial in D is real-rooted for every n >= n0","status":{"kind":"verified"}},{"evidence":"lambda(n) = 1","name":"gauge_finite_nonzero","statement":"lambda(n) is finite and nonzero for every n >= n0","status":{"kind":"verified"}},{"evidence":"delta(n) != 0 for every integer n in [0, +inf) (exact; Taylor shift: the coefficients of delta(n) at n = 0 + u have one sign)","name":"operator_coefficients_defined","sign_decision":{"certificate":{"condition":"nonzero","denominator":["1"],"method":{"kind":"taylor_shift","shifted_denominator":["1"],"shifted_numerator":["1"]},"numerator":["1"],"range":{"first":"0","last":null}},"decision":"holds"},"statement":"the operator coefficients are finite at every n >= n0 (their denominators do not vanish)","status":{"kind":"verified"}}],"identity":{"method":"forward_division","status":"certified"},"input_first_index":0,"input_interlacing":{"reason":"no parent theorem report with an interlacing conclusion","status":"not_proved"},"lean_replay":"not_attempted","operation":{"description":"phi(n, D) = 1 + (1) D","kind":"preserver_image","operator":{"coefficients":[{"denominator":["1"],"numerator":["1"]},{"denominator":["1"],"numerator":["1"]}],"shape":"derivative_polynomial"}},"parent":{"gauge":{"kind":"none"},"index_shift":0,"recurrence":{"first_index":0,"initial_polynomials":[["1"],["1"],["1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["2","1"]]},"deriv_order":0,"offset":3,"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":"periodic_product","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":"c and the seeds are nonzero, real-rooted and of one sign, so P_(n0 + k m + i) = c^m P_(n0 + i) is too","route":"periodic_product","success":true,"variant":"P_(n+k) = c(x) P_n"}],"conditional_on":[],"route":"periodic_product","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"}