{"certification":{"candidate":{"gauge":{"kind":"none"},"index_shift":0,"operator":{"intercept":"1","shape":"affine","slope":"1"},"parent":{"first_index":0,"initial_polynomials":[["1"],["2","3"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["4","12"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["2","3"]]},"deriv_order":0,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent_name":"basis_map_A013610 of Pascal-(1,4,1) array."},"identifying_rows":1,"identity":{"certificate":{"certificate":{"dividend_relation":{"terms":[{"coeff":{"coeffs":[["-18","-27"],["36","27"],["-45","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-90","-297","-81"],["60","180","27"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["-20","-120","-189","-27"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["9"],["9"]]},"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"],["9"]]},"terms":[{"coeff":{"coeffs":[["153","54"],["-153","-27"],["45","0"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["735","693","108"],["-267","-234","-27"]]},"deriv_order":1,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["356","579","270","27"]]},"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"],["2","3"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["4","12"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["2","3"]]},"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":[["-18","-27"],["36","27"],["-45","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-90","-297","-81"],["60","180","27"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["-20","-120","-189","-27"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["9"],["9"]]},"deriv_order":0,"shift":1}]},"quotient":[{"coeff":{"coeffs":[["9"],["9"]]},"deriv_order":0}],"step_multiplier":{"coeffs":[["0","0","0","5832000","104976000","795193200","3267378000","7798010940","10671335280","7632024201","2300608089","301327047","14348907"],["0","0","0","17496000","314928000","2385579600","9802134000","23394032820","32014005840","22896072603","6901824267","903981141","43046721"],["0","0","0","17496000","314928000","2385579600","9802134000","23394032820","32014005840","22896072603","6901824267","903981141","43046721"],["0","0","0","5832000","104976000","795193200","3267378000","7798010940","10671335280","7632024201","2300608089","301327047","14348907"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","0","0","5832000","139968000","1425049200","8038537200","27402278940","57459400920","71660035881","48092753295","14104975581","1822311189","86093442"],["0","0","0","-11664000","-104976000","299181600","7778721600","43216782120","119021526360","176819986638","132775219440","40808291508","5395189032","258280326"],["0","0","0","-69984000","-1154736000","-7652750400","-24895058400","-34763327280","12308173560","100499744628","109769138550","37795021038","5251699962","258280326"],["0","0","0","-81648000","-1434672000","-10502848800","-40972132800","-89567885160","-102610628280","-42820327134","13583631960","9585069876","1607077584","86093442"],["0","0","0","-29160000","-524880000","-3975966000","-16336890000","-38990054700","-53356676400","-38160121005","-11503040445","-1506635235","-71744535","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","-19440000","-425736000","-4050324000","-21858627600","-73240443000","-156549527820","-210955504950","-170913019923","-76704473853","-17768729835","-1994498073","-86093442"],["0","0","0","0","-34992000","-682344000","-5715943200","-26761006800","-76194467640","-134210110140","-141834162726","-82491866343","-22513435083","-2798036865","-129140163"],["0","0","0","58320000","1207224000","10786284000","54143996400","166199315400","317259648180","364446294570","229070734317","65129688873","8279319339","387420489","0"],["0","0","0","38880000","816480000","7418304000","38001312000","119719879200","236904588000","287700899760","199991877120","70917081363","13024024587","1190959281","43046721"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","-12960000","-311040000","-3289248000","-20085408000","-77907938400","-198688075200","-332804887920","-354364858800","-223630904241","-75258422892","-13421011014","-1205308188","-43046721"],["0","0","0","-25920000","-622080000","-6578496000","-40170816000","-155815876800","-397376150400","-665609775840","-708729717600","-447261808482","-150516845784","-26842022028","-2410616376","-86093442"],["0","0","0","-12960000","-311040000","-3289248000","-20085408000","-77907938400","-198688075200","-332804887920","-354364858800","-223630904241","-75258422892","-13421011014","-1205308188","-43046721"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","-19440000","-408240000","-3682908000","-18528264000","-56281570200","-103749093000","-108759400650","-51974929800","-1114431777","3840724107","760492071","43046721"],["0","-58320000","-1253880000","-11573604000","-59560758000","-185181600600","-350237333700","-379634878350","-194084910405","-14846335776","10015537086","2209731678","129140163"],["0","-58320000","-1312200000","-12623364000","-67512690000","-217855380600","-428217443100","-486348231150","-270405152415","-37852416666","7002266616","2066242608","129140163"],["0","-19440000","-495720000","-5257548000","-30456162000","-105292240200","-220719257100","-268829429850","-166455292815","-35623553112","-679181598","545258466","43046721"],["0","0","-29160000","-524880000","-3975966000","-16336890000","-38990054700","-53356676400","-38160121005","-11503040445","-1506635235","-71744535","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","12960000","291600000","2863512000","16035084000","56049310800","125447632200","176255360100","143409353850","52717884318","-1446050961","-4347718821","-789189885","-43046721"],["0","25920000","622080000","6543504000","39488472000","150099933600","370615143600","589415308200","574519607460","305427645756","68024979441","4328586945","-387420489","-43046721"],["0","12960000","369360000","4496472000","30871692000","132051934800","364887390600","650064536100","718811153370","452701638558","140388111765","21700330353","1592728677","43046721"],["0","0","38880000","816480000","7418304000","38001312000","119719879200","236904588000","287700899760","199991877120","70917081363","13024024587","1190959281","43046721"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","-12960000","-311040000","-3289248000","-20085408000","-77907938400","-198688075200","-332804887920","-354364858800","-223630904241","-75258422892","-13421011014","-1205308188","-43046721"],["0","0","-25920000","-622080000","-6578496000","-40170816000","-155815876800","-397376150400","-665609775840","-708729717600","-447261808482","-150516845784","-26842022028","-2410616376","-86093442"],["0","0","-12960000","-311040000","-3289248000","-20085408000","-77907938400","-198688075200","-332804887920","-354364858800","-223630904241","-75258422892","-13421011014","-1205308188","-43046721"]]},"deriv_order":2}]]},{"annihilator":{"terms":[{"coeff":{"coeffs":[["0","0","0"],["30","45","-27"],["0","45","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-20","-30","108","54"],["0","-60","-180","-27"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","20","120","189","27"]]},"deriv_order":2,"shift":0}]},"quotient":[],"step_multiplier":{"coeffs":[["0","0","0","5832000","104976000","795193200","3267378000","7798010940","10671335280","7632024201","2300608089","301327047","14348907"],["0","0","0","17496000","314928000","2385579600","9802134000","23394032820","32014005840","22896072603","6901824267","903981141","43046721"],["0","0","0","17496000","314928000","2385579600","9802134000","23394032820","32014005840","22896072603","6901824267","903981141","43046721"],["0","0","0","5832000","104976000","795193200","3267378000","7798010940","10671335280","7632024201","2300608089","301327047","14348907"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","0","0","19440000","408240000","3682908000","18528264000","56281570200","103749093000","108759400650","51974929800","1114431777","-3840724107","-760492071","-43046721"],["0","0","0","58320000","1253880000","11573604000","59560758000","185181600600","350237333700","379634878350","194084910405","14846335776","-10015537086","-2209731678","-129140163"],["0","0","0","58320000","1312200000","12623364000","67512690000","217855380600","428217443100","486348231150","270405152415","37852416666","-7002266616","-2066242608","-129140163"],["0","0","0","19440000","495720000","5257548000","30456162000","105292240200","220719257100","268829429850","166455292815","35623553112","679181598","-545258466","-43046721"],["0","0","0","0","29160000","524880000","3975966000","16336890000","38990054700","53356676400","38160121005","11503040445","1506635235","71744535","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","-12960000","-291600000","-2863512000","-16035084000","-56049310800","-125447632200","-176255360100","-143409353850","-52717884318","1446050961","4347718821","789189885","43046721"],["0","0","0","-25920000","-622080000","-6543504000","-39488472000","-150099933600","-370615143600","-589415308200","-574519607460","-305427645756","-68024979441","-4328586945","387420489","43046721"],["0","0","0","-12960000","-369360000","-4496472000","-30871692000","-132051934800","-364887390600","-650064536100","-718811153370","-452701638558","-140388111765","-21700330353","-1592728677","-43046721"],["0","0","0","0","-38880000","-816480000","-7418304000","-38001312000","-119719879200","-236904588000","-287700899760","-199991877120","-70917081363","-13024024587","-1190959281","-43046721"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","12960000","311040000","3289248000","20085408000","77907938400","198688075200","332804887920","354364858800","223630904241","75258422892","13421011014","1205308188","43046721"],["0","0","0","0","25920000","622080000","6578496000","40170816000","155815876800","397376150400","665609775840","708729717600","447261808482","150516845784","26842022028","2410616376","86093442"],["0","0","0","0","12960000","311040000","3289248000","20085408000","77907938400","198688075200","332804887920","354364858800","223630904241","75258422892","13421011014","1205308188","43046721"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","0","38880000","822312000","7505784000","38481577200","120601677600","234900464940","274978202220","175609895481","50321616849","6423527367","301327047"],["0","0","116640000","2496096000","23042232000","119420697600","378141922800","743691449520","878291283060","564989807448","162467890992","20777217336","975725676"],["0","0","116640000","2554416000","24091992000","127372629600","410815702800","821671558920","985004635860","641310049458","185473971882","23790487806","1119214746"],["0","0","38880000","909792000","9080424000","50409475200","169612347600","351870629040","435048231420","290090258496","84830738184","10943433072","516560652"],["0","0","0","29160000","524880000","3975966000","16336890000","38990054700","53356676400","38160121005","11503040445","1506635235","71744535"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","-25920000","-602640000","-6152760000","-36120492000","-133957249200","-324135707400","-509060248020","-497774212650","-276348788559","-73812371931","-9073292193","-416118303","0"],["0","0","-51840000","-1244160000","-13122000000","-79659288000","-305915810400","-767991294000","-1255025084040","-1283249325060","-752689454238","-218541825225","-31170608973","-2023195887","-43046721"],["0","0","-25920000","-680400000","-7785720000","-50957100000","-209959873200","-563575465800","-982869424020","-1073176012170","-676332542799","-215646534657","-35121341367","-2798036865","-86093442"],["0","0","0","-38880000","-816480000","-7418304000","-38001312000","-119719879200","-236904588000","-287700899760","-199991877120","-70917081363","-13024024587","-1190959281","-43046721"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","12960000","311040000","3289248000","20085408000","77907938400","198688075200","332804887920","354364858800","223630904241","75258422892","13421011014","1205308188","43046721"],["0","0","0","25920000","622080000","6578496000","40170816000","155815876800","397376150400","665609775840","708729717600","447261808482","150516845784","26842022028","2410616376","86093442"],["0","0","0","12960000","311040000","3289248000","20085408000","77907938400","198688075200","332804887920","354364858800","223630904241","75258422892","13421011014","1205308188","43046721"]]},"deriv_order":2}]]}],"restart_bases":[],"row_multiplier":{"coeffs":[["9"]]},"start_base":0}},"shifted_parent_relation":{"terms":[{"coeff":{"coeffs":[["-4","-12"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-2","-3"]]},"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"],["2","3"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["4","12"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["2","3"]]},"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) = (2) + (3) x, V_n(x) = 0, W_n(x) = (4) + (12) x; open hypotheses: multipliers_vanish_at_zero: [x^0] c_2(n, x) = 4 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 = 4 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 = 4 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) = (2) + (3) x, B_n(x) = (4) + (12) x: every P_n, n >= 0, is nonzero and real-rooted with every root in (-inf, -1/3] (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) + (3) x, B_n(x) = (4) + (12) x","every P_n, n >= 0, is nonzero and real-rooted with every root in (-inf, -1/3] (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"}