{"certification":{"candidate":{"gauge":{"kind":"none"},"index_shift":0,"operator":{"a":"1","b":"0","c":"1","e":"1","schedule":{"first_degree":0,"first_index":0,"step":1},"shape":"mobius"},"parent":{"first_index":0,"initial_polynomials":[["1"],["2","3"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["3","9"]]},"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,3,1) array."},"identifying_rows":1,"identity":{"certificate":{"certificate":{"dividend_relation":{"terms":[{"coeff":{"coeffs":[["-18","63","-45","-90","180","-117","27"],["27","-108","135","0","-135","108","-27"],["-36","180","-360","360","-180","36","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-72","117","414","-1305","1260","-333","-162","81"],["48","-96","-213","825","-930","402","-9","-27"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["-16","-16","167","-62","-515","796","-399","18","27"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["9","-45","90","-90","45","-9"],["9","-45","90","-90","45","-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","0","0","0"],["9","27","27","9"]]},"terms":[{"coeff":{"coeffs":[["233","1749","5250","8170","7005","3153","584"],["-315","-2370","-7233","-11505","-10092","-4641","-876"],["100","720","2172","3488","3132","1488","292"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["184","1939","8103","17870","22790","16959","6859","1168"],["-80","-848","-3597","-8092","-10558","-8052","-3341","-584"]]},"deriv_order":1,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["16","224","1273","3857","6910","7586","5029","1853","292"]]},"deriv_order":2,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"input_valid_from_base":0,"multiplier":["1","1"],"operator":{"a":"1","b":"0","c":"1","e":"1","schedule":{"first_degree":0,"first_index":0,"step":1},"shape":"mobius"},"parent":{"first_index":0,"initial_polynomials":[["1"],["2","3"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["3","9"]]},"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"],["27","27"],["-36","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-72","-243","-81"],["48","144","27"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["-16","-96","-153","-27"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["9"],["9"]]},"deriv_order":0,"shift":1}]},"quotient":[{"coeff":{"coeffs":[["9","-45","90","-90","45","-9"],["9","-45","90","-90","45","-9"]]},"deriv_order":0}],"step_multiplier":{"coeffs":[["0","0","0","2985984","53747712","408146688","1688014080","4084301232","5748065856","4371102225","1535333049","243931419","14348907"],["0","0","0","8957952","161243136","1224440064","5064042240","12252903696","17244197568","13113306675","4605999147","731794257","43046721"],["0","0","0","8957952","161243136","1224440064","5064042240","12252903696","17244197568","13113306675","4605999147","731794257","43046721"],["0","0","0","2985984","53747712","408146688","1688014080","4084301232","5748065856","4371102225","1535333049","243931419","14348907"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","0","0","2985984","71663616","730632960","4136894208","14212385712","30253873248","38859497361","27761946399","9455929713","1477937421","86093442"],["0","0","0","-2985984","0","559312128","5658626304","26299952208","67769356320","99094083183","77144507001","27392063463","4376416635","258280326"],["0","0","0","-26873856","-429981696","-2705861376","-7845486336","-6374457648","21784829472","64125265383","64861842609","25440612111","4261625379","258280326"],["0","0","0","-32845824","-573308928","-4167127296","-16119274752","-34799229072","-38722917024","-13593729339","9337949811","6528752685","1305750537","86093442"],["0","0","0","-11943936","-214990848","-1632586752","-6752056320","-16337204928","-22992263424","-17484408900","-6141332196","-975725676","-57395628","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","-7962624","-176173056","-1697531904","-9313470720","-31908504960","-70383573648","-99390804408","-86664741075","-43765760673","-11933507655","-1621426491","-86093442"],["0","0","0","0","-17915904","-349360128","-2932609536","-13801404672","-39697934112","-71247106224","-77959206054","-48551918319","-15281585955","-2281476213","-129140163"],["0","0","0","23887872","492687360","4393875456","22075193088","68122705536","131754852720","155678200776","104075811117","34193445381","5237351055","301327047","0"],["0","0","0","15925248","334430208","3045703680","15694331904","50015605248","101069213184","127534502592","95370276096","38979603027","8585429355","961376769","43046721"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","-5308416","-127401984","-1349664768","-8277147648","-32366200320","-83705342976","-143580714048","-159324594624","-108363477105","-41841412812","-8905888278","-975725676","-43046721"],["0","0","0","-10616832","-254803968","-2699329536","-16554295296","-64732400640","-167410685952","-287161428096","-318649189248","-216726954210","-83682825624","-17811776556","-1951451352","-86093442"],["0","0","0","-5308416","-127401984","-1349664768","-8277147648","-32366200320","-83705342976","-143580714048","-159324594624","-108363477105","-41841412812","-8905888278","-975725676","-43046721"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","-7962624","-167215104","-1509414912","-7605301248","-23171142528","-42938543232","-45387895752","-21818841696","180158499","2616284043","617003001","43046721"],["0","-23887872","-513589248","-4743235584","-24448490496","-76265483904","-145152834624","-159155950680","-82940933988","-5600856699","6873126453","1793613375","129140163"],["0","-23887872","-537477120","-5173217280","-27713664000","-89769596544","-177827244480","-205140477528","-117909751788","-17883521091","4921675101","1678822119","129140163"],["0","-7962624","-203046912","-2154387456","-12503061504","-43427311488","-91950158016","-114364686024","-74272068396","-18243838089","-310892985","444816117","43046721"],["0","0","-11943936","-214990848","-1632586752","-6752056320","-16337204928","-22992263424","-17484408900","-6141332196","-975725676","-57395628","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","5308416","119439360","1173491712","6579615744","23052729600","51796838016","73197140400","59933790216","21698736030","-1924347861","-3027619377","-645700815","-43046721"],["0","10616832","254803968","2681413632","16204935168","61799791104","153609281280","247463493984","247402083024","138767748156","35130907305","2530190601","-330024861","-43046721"],["0","5308416","151289856","1842352128","12671023104","54441393408","151828048512","275335566768","315002795400","212439288222","76034858193","14143239333","1277052723","43046721"],["0","0","15925248","334430208","3045703680","15694331904","50015605248","101069213184","127534502592","95370276096","38979603027","8585429355","961376769","43046721"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","-5308416","-127401984","-1349664768","-8277147648","-32366200320","-83705342976","-143580714048","-159324594624","-108363477105","-41841412812","-8905888278","-975725676","-43046721"],["0","0","-10616832","-254803968","-2699329536","-16554295296","-64732400640","-167410685952","-287161428096","-318649189248","-216726954210","-83682825624","-17811776556","-1951451352","-86093442"],["0","0","-5308416","-127401984","-1349664768","-8277147648","-32366200320","-83705342976","-143580714048","-159324594624","-108363477105","-41841412812","-8905888278","-975725676","-43046721"]]},"deriv_order":2}]]},{"annihilator":{"terms":[{"coeff":{"coeffs":[["0","0","0"],["24","36","-27"],["0","36","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-16","-24","90","54"],["0","-48","-144","-27"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","16","96","153","27"]]},"deriv_order":2,"shift":0}]},"quotient":[],"step_multiplier":{"coeffs":[["0","0","0","2985984","53747712","408146688","1688014080","4084301232","5748065856","4371102225","1535333049","243931419","14348907"],["0","0","0","8957952","161243136","1224440064","5064042240","12252903696","17244197568","13113306675","4605999147","731794257","43046721"],["0","0","0","8957952","161243136","1224440064","5064042240","12252903696","17244197568","13113306675","4605999147","731794257","43046721"],["0","0","0","2985984","53747712","408146688","1688014080","4084301232","5748065856","4371102225","1535333049","243931419","14348907"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","0","0","7962624","167215104","1509414912","7605301248","23171142528","42938543232","45387895752","21818841696","-180158499","-2616284043","-617003001","-43046721"],["0","0","0","23887872","513589248","4743235584","24448490496","76265483904","145152834624","159155950680","82940933988","5600856699","-6873126453","-1793613375","-129140163"],["0","0","0","23887872","537477120","5173217280","27713664000","89769596544","177827244480","205140477528","117909751788","17883521091","-4921675101","-1678822119","-129140163"],["0","0","0","7962624","203046912","2154387456","12503061504","43427311488","91950158016","114364686024","74272068396","18243838089","310892985","-444816117","-43046721"],["0","0","0","0","11943936","214990848","1632586752","6752056320","16337204928","22992263424","17484408900","6141332196","975725676","57395628","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","-5308416","-119439360","-1173491712","-6579615744","-23052729600","-51796838016","-73197140400","-59933790216","-21698736030","1924347861","3027619377","645700815","43046721"],["0","0","0","-10616832","-254803968","-2681413632","-16204935168","-61799791104","-153609281280","-247463493984","-247402083024","-138767748156","-35130907305","-2530190601","330024861","43046721"],["0","0","0","-5308416","-151289856","-1842352128","-12671023104","-54441393408","-151828048512","-275335566768","-315002795400","-212439288222","-76034858193","-14143239333","-1277052723","-43046721"],["0","0","0","0","-15925248","-334430208","-3045703680","-15694331904","-50015605248","-101069213184","-127534502592","-95370276096","-38979603027","-8585429355","-961376769","-43046721"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","5308416","127401984","1349664768","8277147648","32366200320","83705342976","143580714048","159324594624","108363477105","41841412812","8905888278","975725676","43046721"],["0","0","0","0","10616832","254803968","2699329536","16554295296","64732400640","167410685952","287161428096","318649189248","216726954210","83682825624","17811776556","1951451352","86093442"],["0","0","0","0","5308416","127401984","1349664768","8277147648","32366200320","83705342976","143580714048","159324594624","108363477105","41841412812","8905888278","975725676","43046721"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","0","15925248","337416192","3090493440","15941235456","50479179264","100089472176","121029664752","82497180753","27401629401","4223361627","243931419"],["0","0","47775744","1024192512","9486471168","49456293120","158189594112","316605621456","386081257680","264975951159","88346220399","13645810557","789189885"],["0","0","47775744","1048080384","9916452864","52721466624","171693706752","349280031312","432065784528","299944768959","100628884791","15597261909","903981141"],["0","0","15925248","373248000","3735465984","20838995712","70735348224","149101086960","190006455024","134950407453","45825625989","7150538655","416118303"],["0","0","0","11943936","214990848","1632586752","6752056320","16337204928","22992263424","17484408900","6141332196","975725676","57395628"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","-10616832","-246841344","-2523156480","-14856763392","-55418929920","-135502180992","-216777854448","-219258384840","-130062213135","-39917064951","-5878268901","-330024861","0"],["0","0","-21233664","-509607936","-5380743168","-32759230464","-126532191744","-321019967232","-534624922080","-566051272272","-355494702366","-118813732929","-20341967157","-1621426491","-43046721"],["0","0","-10616832","-278691840","-3192016896","-20948170752","-86807593728","-235533391488","-418916280816","-474327390024","-320802765327","-117876271005","-23049127611","-2252778399","-86093442"],["0","0","0","-15925248","-334430208","-3045703680","-15694331904","-50015605248","-101069213184","-127534502592","-95370276096","-38979603027","-8585429355","-961376769","-43046721"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","5308416","127401984","1349664768","8277147648","32366200320","83705342976","143580714048","159324594624","108363477105","41841412812","8905888278","975725676","43046721"],["0","0","0","10616832","254803968","2699329536","16554295296","64732400640","167410685952","287161428096","318649189248","216726954210","83682825624","17811776556","1951451352","86093442"],["0","0","0","5308416","127401984","1349664768","8277147648","32366200320","83705342976","143580714048","159324594624","108363477105","41841412812","8905888278","975725676","43046721"]]},"deriv_order":2}]]}],"restart_bases":[],"row_multiplier":{"coeffs":[["9"]]},"start_base":0}},"shifted_parent_relation":{"terms":[{"coeff":{"coeffs":[["-3","-9"]]},"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 = ((1) x + (1))^(d_n) P(((1) x + (0))/((1) x + (1))), d_n = 0 + 1 (n - 0); 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":"the schedule d_n depends on n","status":"none"},"lean_declarations":["RealRooted.splits_fPolynomial"],"lean_route":"fTransform","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":"the schedule d_n depends on n","status":"not_proved"},"lean_replay":"not_attempted","operation":{"description":"((1) x + (1))^(d_n) P(((1) x + (0))/((1) x + (1))), d_n = 0 + 1 (n - 0)","kind":"preserver_image","operator":{"a":"1","b":"0","c":"1","e":"1","schedule":{"first_degree":0,"first_index":0,"step":1},"shape":"mobius"}},"parent":{"gauge":{"kind":"none"},"index_shift":0,"recurrence":{"first_index":0,"initial_polynomials":[["1"],["2","3"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["3","9"]]},"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 = ((1) x + (1))^(d_n) P(((1) x + (0))/((1) x + (1))), d_n = 0 + 1 (n - 0), 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 [-1, 0]","input_root_region":{"lower":{"closed":true,"value":"-1"},"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":"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) = (3) + (9) x; open hypotheses: multipliers_vanish_at_zero: [x^0] c_2(n, x) = 3 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 = 3 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 = 3 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) = (3) + (9) 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) = (3) + (9) 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 = ((1) x + (1))^(d_n) P(((1) x + (0))/((1) x + (1))), d_n = 0 + 1 (n - 0) 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 [-1, 0]"},"kind":"preserver_image"}