{"certification":{"candidate":{"gauge":{"kind":"none"},"index_shift":0,"operator":{"schedule":{"first_degree":0,"first_index":0,"step":1},"shape":"reversal"},"parent":{"first_index":0,"initial_polynomials":[["1"],["1","1"]],"recurrence":{"denominator":{"coeffs":[["6"],["7"],["2"]]},"terms":[{"coeff":{"coeffs":[["4","-2"],["13","1"],["-2","16"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","6","-6"],["0","18","-18"]]},"deriv_order":1,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["2","4","2"],["-6","-12","-6"],["4","8","4"]]},"deriv_order":0,"offset":2,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent_name":"Square array read by antidiagonals: S(p,q) = (p+q+1)!(2p+2q+1)!/((p+1)!(2p+1)!(q+1)!(2q+1)!) (p,q>=0)."},"identifying_rows":1,"identity":{"certificate":{"certificate":{"dividend_relation":{"terms":[{"coeff":{"coeffs":[["-15","-15"],["-11","-35"],["-2","-20"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["0","-36","12"],["0","-6","30"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","0","-12","-12"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["15"],["11"],["2"]]},"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":[["6"],["7"],["2"]]},"terms":[{"coeff":{"coeffs":[["6","0"],["7","-5"],["2","20"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","30","18"],["0","6","-30"]]},"deriv_order":1,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","0","12","12"]]},"deriv_order":2,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"input_valid_from_base":0,"multiplier":["15/2","11/2","1"],"operator":{"schedule":{"first_degree":0,"first_index":0,"step":1},"shape":"reversal"},"parent":{"first_index":0,"initial_polynomials":[["1"],["1","1"]],"recurrence":{"denominator":{"coeffs":[["6"],["7"],["2"]]},"terms":[{"coeff":{"coeffs":[["4","-2"],["13","1"],["-2","16"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","6","-6"],["0","18","-18"]]},"deriv_order":1,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["2","4","2"],["-6","-12","-6"],["4","8","4"]]},"deriv_order":0,"offset":2,"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":[["-15","-15"],["-11","-35"],["-2","-20"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["0","-36","12"],["0","-6","30"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","0","-12","-12"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["15"],["11"],["2"]]},"deriv_order":0,"shift":1}]},"quotient":[{"coeff":{"coeffs":[["15"],["11"],["2"]]},"deriv_order":0}],"step_multiplier":{"coeffs":[["0","0","0","0","13500","27000","13500"],["0","0","0","0","29700","59400","29700"],["0","0","0","0","27180","54360","27180"],["0","0","0","0","13244","26488","13244"],["0","0","0","0","3624","7248","3624"],["0","0","0","0","528","1056","528"],["0","0","0","0","32","64","32"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","0","0","0","-151200","-453600","-453600","-151200"],["0","0","0","0","-554760","-1664280","-1664280","-554760"],["0","0","0","0","-856632","-2569896","-2569896","-856632"],["0","0","0","0","-731128","-2193384","-2193384","-731128"],["0","0","0","0","-378984","-1136952","-1136952","-378984"],["0","0","0","0","-122624","-367872","-367872","-122624"],["0","0","0","0","-24256","-72768","-72768","-24256"],["0","0","0","0","-2688","-8064","-8064","-2688"],["0","0","0","0","-128","-384","-384","-128"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","0","0","0","0","0"],["0","0","0","0","0","302400","907200","907200","302400"],["0","0","0","0","0","605520","1816560","1816560","605520"],["0","0","0","0","0","502464","1507392","1507392","502464"],["0","0","0","0","0","221136","663408","663408","221136"],["0","0","0","0","0","54432","163296","163296","54432"],["0","0","0","0","0","7104","21312","21312","7104"],["0","0","0","0","0","384","1152","1152","384"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","0","0","-302400","-907200","-907200","-302400"],["0","0","0","0","0","0","-605520","-1816560","-1816560","-605520"],["0","0","0","0","0","0","-502464","-1507392","-1507392","-502464"],["0","0","0","0","0","0","-221136","-663408","-663408","-221136"],["0","0","0","0","0","0","-54432","-163296","-163296","-54432"],["0","0","0","0","0","0","-7104","-21312","-21312","-7104"],["0","0","0","0","0","0","-384","-1152","-1152","-384"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","0","0","0","0","-907200","-2721600","-2721600","-907200"],["0","0","0","0","0","-909360","-2728080","-2728080","-909360"],["0","0","0","0","0","309168","927504","927504","309168"],["0","0","0","0","0","843984","2531952","2531952","843984"],["0","0","0","0","0","500112","1500336","1500336","500112"],["0","0","0","0","0","141984","425952","425952","141984"],["0","0","0","0","0","20160","60480","60480","20160"],["0","0","0","0","0","1152","3456","3456","1152"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","0","0","-1814400","-5443200","-5443200","-1814400"],["0","0","0","0","0","0","-3633120","-10899360","-10899360","-3633120"],["0","0","0","0","0","0","-3014784","-9044352","-9044352","-3014784"],["0","0","0","0","0","0","-1326816","-3980448","-3980448","-1326816"],["0","0","0","0","0","0","-326592","-979776","-979776","-326592"],["0","0","0","0","0","0","-42624","-127872","-127872","-42624"],["0","0","0","0","0","0","-2304","-6912","-6912","-2304"]]},"deriv_order":1}]]},{"annihilator":{"terms":[{"coeff":{"coeffs":[["0"],["-1"],["-3"],["-2"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["6","0"],["0","0"],["0","6"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","9","3"],["0","0","-6"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["0","0","2","2"]]},"deriv_order":3,"shift":0}]},"quotient":[],"step_multiplier":{"coeffs":[["0","0","0","0","0","0","405000","1215000","1215000","405000"],["0","0","0","0","0","0","1188000","3564000","3564000","1188000"],["0","0","0","0","0","0","1522800","4568400","4568400","1522800"],["0","0","0","0","0","0","1114080","3342240","3342240","1114080"],["0","0","0","0","0","0","508808","1526424","1526424","508808"],["0","0","0","0","0","0","148544","445632","445632","148544"],["0","0","0","0","0","0","27072","81216","81216","27072"],["0","0","0","0","0","0","2816","8448","8448","2816"],["0","0","0","0","0","0","128","384","384","128"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","0","0","0","0","0","-4536000","-13608000","-13608000","-4536000"],["0","0","0","0","0","0","-22237200","-66711600","-66711600","-22237200"],["0","0","0","0","0","0","-48493080","-145479240","-145479240","-48493080"],["0","0","0","0","0","0","-62253024","-186759072","-186759072","-62253024"],["0","0","0","0","0","0","-52380256","-157140768","-157140768","-52380256"],["0","0","0","0","0","0","-30381312","-91143936","-91143936","-30381312"],["0","0","0","0","0","0","-12411784","-37235352","-37235352","-12411784"],["0","0","0","0","0","0","-3575440","-10726320","-10726320","-3575440"],["0","0","0","0","0","0","-712384","-2137152","-2137152","-712384"],["0","0","0","0","0","0","-93568","-280704","-280704","-93568"],["0","0","0","0","0","0","-7296","-21888","-21888","-7296"],["0","0","0","0","0","0","-256","-768","-768","-256"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","0","0","4536000","18144000","27216000","18144000","4536000"],["0","0","0","0","0","0","12409200","58708800","101671200","76852800","21481200"],["0","0","0","0","0","0","14802480","88564320","176878080","147273120","44156880"],["0","0","0","0","0","0","10055184","82234896","186373584","166263216","52069344"],["0","0","0","0","0","0","4253904","51928464","130261968","121754160","39166752"],["0","0","0","0","0","0","1147584","23153328","62574480","60279312","19710576"],["0","0","0","0","0","0","192768","7320144","20803824","20418288","6741840"],["0","0","0","0","0","0","18432","1606848","4709952","4673088","1551552"],["0","0","0","0","0","0","768","232704","693504","691968","230400"],["0","0","0","0","0","0","0","19968","59904","59904","19968"],["0","0","0","0","0","0","0","768","2304","2304","768"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","0","0","0","6804000","18144000","13608000","0","-2268000"],["0","0","0","0","0","0","0","18613800","45100800","23619600","-13608000","-10740600"],["0","0","0","0","0","0","0","22203720","46800720","7179840","-37227600","-19810440"],["0","0","0","0","0","0","0","15082776","25418256","-14241888","-44407440","-19830072"],["0","0","0","0","0","0","0","6380856","6960432","-17403840","-30165552","-12182136"],["0","0","0","0","0","0","0","1721376","336432","-9318960","-12761712","-4827696"],["0","0","0","0","0","0","0","289152","-376512","-2864448","-3442752","-1243968"],["0","0","0","0","0","0","0","27648","-119040","-523008","-578304","-201984"],["0","0","0","0","0","0","0","1152","-15360","-52992","-55296","-18816"],["0","0","0","0","0","0","0","0","-768","-2304","-2304","-768"]]},"deriv_order":2},{"coeff":{"coeffs":[["0","0","0","0","0","0","0","0","1512000","6048000","9072000","6048000","1512000"],["0","0","0","0","0","0","0","0","4136400","16545600","24818400","16545600","4136400"],["0","0","0","0","0","0","0","0","4934160","19736640","29604960","19736640","4934160"],["0","0","0","0","0","0","0","0","3351728","13406912","20110368","13406912","3351728"],["0","0","0","0","0","0","0","0","1417968","5671872","8507808","5671872","1417968"],["0","0","0","0","0","0","0","0","382528","1530112","2295168","1530112","382528"],["0","0","0","0","0","0","0","0","64256","257024","385536","257024","64256"],["0","0","0","0","0","0","0","0","6144","24576","36864","24576","6144"],["0","0","0","0","0","0","0","0","256","1024","1536","1024","256"]]},"deriv_order":3}],[{"coeff":{"coeffs":[["0","0","0","0","0","0","38556000","127008000","149688000","72576000","11340000"],["0","0","0","0","0","0","118330200","412473600","527439600","290779200","57483000"],["0","0","0","0","0","0","162492480","611990640","861017040","536032080","124513200"],["0","0","0","0","0","0","131545824","547487232","853186752","590095104","152849760"],["0","0","0","0","0","0","69582032","327377696","564640896","425476832","118631600"],["0","0","0","0","0","0","25158920","136677440","259078800","208760960","61200680"],["0","0","0","0","0","0","6307984","40279792","82991472","70375504","21355840"],["0","0","0","0","0","0","1085376","8251968","18243648","16072896","4995840"],["0","0","0","0","0","0","123008","1121024","2625024","2379008","752000"],["0","0","0","0","0","0","8320","90880","222720","206080","65920"],["0","0","0","0","0","0","256","3328","8448","7936","2560"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","0","0","0","45360000","127008000","108864000","18144000","-9072000"],["0","0","0","0","0","0","0","128628000","338385600","243388800","-13867200","-47498400"],["0","0","0","0","0","0","0","160434000","389651040","206349120","-114518880","-91650960"],["0","0","0","0","0","0","0","115354320","251940192","63694656","-167013984","-94122768"],["0","0","0","0","0","0","0","52594224","98998944","-18568512","-123756960","-58783728"],["0","0","0","0","0","0","0","15729744","23624544","-23504832","-54964320","-23564688"],["0","0","0","0","0","0","0","3075264","3102336","-9144576","-15295104","-6123456"],["0","0","0","0","0","0","0","377088","130560","-1870848","-2625024","-1000704"],["0","0","0","0","0","0","0","26112","-15360","-202752","-254976","-93696"],["0","0","0","0","0","0","0","768","-1536","-9216","-10752","-3840"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","0","0","0","0","9072000","36288000","54432000","36288000","9072000"],["0","0","0","0","0","0","0","0","24818400","99273600","148910400","99273600","24818400"],["0","0","0","0","0","0","0","0","29604960","118419840","177629760","118419840","29604960"],["0","0","0","0","0","0","0","0","20110368","80441472","120662208","80441472","20110368"],["0","0","0","0","0","0","0","0","8507808","34031232","51046848","34031232","8507808"],["0","0","0","0","0","0","0","0","2295168","9180672","13771008","9180672","2295168"],["0","0","0","0","0","0","0","0","385536","1542144","2313216","1542144","385536"],["0","0","0","0","0","0","0","0","36864","147456","221184","147456","36864"],["0","0","0","0","0","0","0","0","1536","6144","9216","6144","1536"]]},"deriv_order":2}]]}],"restart_bases":[],"row_multiplier":{"coeffs":[["2"]]},"start_base":0}},"shifted_parent_relation":{"terms":[{"coeff":{"coeffs":[["-6","-12","-6"],["-10","-20","-10"],["-4","-8","-4"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-22","-64"],["-5","-65"],["2","-16"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["0","-42","42"],["0","-18","18"]]},"deriv_order":1,"shift":1},{"coeff":{"coeffs":[["28"],["15"],["2"]]},"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 = x^(d_n) P(1/x), 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.X_pow_mul_reverse_eq_zero_or_splits","RealRooted.reflect_eq_zero_or_splits"],"lean_route":"reversed","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":"x^(d_n) P(1/x), d_n = 0 + 1 (n - 0)","kind":"preserver_image","operator":{"schedule":{"first_degree":0,"first_index":0,"step":1},"shape":"reversal"}},"parent":{"gauge":{"kind":"none"},"index_shift":0,"recurrence":{"first_index":0,"initial_polynomials":[["1"],["1","1"]],"recurrence":{"denominator":{"coeffs":[["6"],["7"],["2"]]},"terms":[{"coeff":{"coeffs":[["4","-2"],["13","1"],["-2","16"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","6","-6"],["0","18","-18"]]},"deriv_order":1,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["2","4","2"],["-6","-12","-6"],["4","8","4"]]},"deriv_order":0,"offset":2,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"relation":"Q_n = lambda(n) T_n(P_(n+0)) with T = x^(d_n) P(1/x), d_n = 0 + 1 (n - 0), for every n >= 0"},"parent_proof":{"statement":"open: no route proved that every parent row P_n, n >= 0, is zero or real-rooted with coefficients of one sign; the first 10 parent rows pass the exact check (evidence only)","status":"open"},"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":"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":"open"},"notes":["the division remainder is removed by row annihilators of the shifted parent"],"parent_proof":{"attempts":[{"detail":"the leader is not a nonzero constant","route":"periodic_product","success":false,"variant":"P_(n+k) = c(x) P_n"},{"detail":"no theorem matched (weighted_renewal_window: LHS must be a nonzero constant; fixed_delay_predecessor_window: LHS must be a nonzero constant)","route":"paper_theorem","success":false,"variant":"match_recurrence_theorems"},{"detail":"not applicable: the rule is not f(n) P_n = c_1(n, x) P_(n-1) + c_2(n, x) P_(n-2) with both terms nonzero","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) = ((-n^2 + 13/2 n + 2)/(n^2 + 7/2 n + 3)) + ((8 n^2 + 1/2 n - 1)/(n^2 + 7/2 n + 3)) x, V_n(x) = ((9 n + 3)/(n^2 + 7/2 n + 3)) x + ((-9 n - 3)/(n^2 + 7/2 n + 3)) x^2, W_n(x) = ((2 n^2 - 3 n + 1)/(n^2 + 7/2 n + 3)) + ((4 n^2 - 6 n + 2)/(n^2 + 7/2 n + 3)) x + ((2 n^2 - 3 n + 1)/(n^2 + 7/2 n + 3)) x^2; open hypotheses: derivative_degree_step_nonnegative: fails at n = 7: lambda_n = (-n^2 + 13/2 n + 2)/(n^2 + 7/2 n + 3) = -1/51 there (exact); multipliers_vanish_at_zero: [x^0] c_2(n, x) = 4 n^2 - 6 n + 2 is not the zero polynomial; constant_term_positive: fails at n = 7: A_n(0) = (-n^2 + 13/2 n + 2)/(n^2 + 7/2 n + 3) = -1/51 there (exact); 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/14 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":"the parent equals the flagged entry, but the flag gives real-rootedness only and one-signed coefficients are not shown: the weight of the coefficient of x^s of P_(n-1) in the coefficient of x^(s+0) is not shown to be >= 0 for n >= 2","route":"attestation","success":false,"variant":"oeis_catalog:A111910:lean_proved"},{"detail":"no lean_proved catalog entry equals the parent; 91 with the same first index and seeds differ in the rule or in later initial rows (oeis_catalog:A001263:lean_proved, oeis_catalog:A008459:lean_proved, oeis_catalog:A008518:lean_proved, oeis_catalog:A024462:lean_proved, oeis_catalog:A026374:lean_proved, oeis_catalog:A026386:lean_proved, oeis_catalog:A028262:lean_proved, oeis_catalog:A028313:lean_proved, oeis_catalog:A030528:lean_proved, oeis_catalog:A038763:lean_proved, oeis_catalog:A046741:lean_proved, oeis_catalog:A046802:lean_proved, oeis_catalog:A054142:lean_proved, oeis_catalog:A056241:lean_proved, oeis_catalog:A056939:lean_proved, oeis_catalog:A081577:lean_proved, oeis_catalog:A081578:lean_proved, oeis_catalog:A081579:lean_proved, oeis_catalog:A081580:lean_proved, oeis_catalog:A081581:lean_proved, oeis_catalog:A081582:lean_proved, oeis_catalog:A092879:lean_proved, oeis_catalog:A097806:lean_proved, oeis_catalog:A100862:lean_proved, oeis_catalog:A100898:lean_proved, oeis_catalog:A102413:lean_proved, oeis_catalog:A103450:lean_proved, oeis_catalog:A105793:lean_proved, oeis_catalog:A109955:lean_proved, oeis_catalog:A109960:lean_proved, oeis_catalog:A111049:lean_proved, oeis_catalog:A114123:lean_proved, oeis_catalog:A124376:lean_proved, oeis_catalog:A124860:lean_proved, oeis_catalog:A128540:lean_proved, oeis_catalog:A128541:lean_proved, oeis_catalog:A129718:lean_proved, oeis_catalog:A133080:lean_proved, oeis_catalog:A136158:lean_proved, oeis_catalog:A141697:lean_proved, oeis_catalog:A143007:lean_proved, oeis_catalog:A143683:lean_proved, oeis_catalog:A143685:lean_proved, oeis_catalog:A144436:lean_proved, oeis_catalog:A144438:lean_proved, oeis_catalog:A144439:lean_proved, oeis_catalog:A144440:lean_proved, oeis_catalog:A144441:lean_proved, oeis_catalog:A144442:lean_proved, oeis_catalog:A144443:lean_proved, oeis_catalog:A144445:lean_proved, oeis_catalog:A146986:lean_proved, oeis_catalog:A146987:lean_proved, oeis_catalog:A146988:lean_proved, oeis_catalog:A147565:lean_proved, oeis_catalog:A147644:lean_proved, oeis_catalog:A154227:lean_proved, oeis_catalog:A154228:lean_proved, oeis_catalog:A154233:lean_proved, oeis_catalog:A154986:lean_proved, oeis_catalog:A157012:lean_proved, oeis_catalog:A157147:lean_proved, oeis_catalog:A157148:lean_proved, oeis_catalog:A157149:lean_proved, oeis_catalog:A157150:lean_proved, oeis_catalog:A157151:lean_proved, oeis_catalog:A157169:lean_proved, oeis_catalog:A157171:lean_proved, oeis_catalog:A157637:lean_proved, oeis_catalog:A166345:lean_proved, oeis_catalog:A169803:lean_proved, oeis_catalog:A176331:lean_proved, oeis_catalog:A181543:lean_proved, oeis_catalog:A184883:lean_proved, oeis_catalog:A190152:lean_proved, oeis_catalog:A193636:lean_proved, oeis_catalog:A208513:lean_proved, oeis_catalog:A209414:lean_proved, oeis_catalog:A228955:lean_proved, oeis_catalog:A236471:lean_proved, oeis_catalog:A249247:lean_proved, oeis_catalog:A258758:lean_proved, oeis_catalog:A267482:lean_proved, oeis_catalog:A305540:lean_proved, oeis_catalog:A321966:lean_proved, oeis_catalog:A350512:lean_proved, oeis_catalog:A358628:lean_proved, oeis_catalog:A358735:lean_proved, oeis_catalog:A367873:lean_proved, oeis_catalog:A371898:lean_proved, oeis_catalog:A376827:lean_proved)","route":"attestation","success":false,"variant":"oeis_catalog"}],"conditional_on":[],"rows_checked":10,"statement":"open: no route proved that every parent row P_n, n >= 0, is zero or real-rooted with coefficients of one sign; the first 10 parent rows pass the exact check (evidence only)","status":"not_proved"},"rows_compared":16,"schema":"polytool.recurrence-preserver-image.v1","statement":"Q_n = lambda(n) T_n(P_(n+0)) with T = x^(d_n) P(1/x), d_n = 0 + 1 (n - 0) for every n >= 0 is certified; the lift is Open (open: no route proved that every parent row P_n, n >= 0, is zero or real-rooted with coefficients of one sign; the first 10 parent rows pass the exact check (evidence only))"},"kind":"preserver_image"}