{"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":[["8"],["12","18"],["16","64","32"]],"recurrence":{"denominator":{"coeffs":[["0"],["9"],["3"]]},"terms":[{"coeff":{"coeffs":[["0","0"],["8","26"],["8","5"],["2","-4"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["2","-8","8"],["7","2","-11"],["-5","2","-5"],["-4","4","8"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["0","0","0","0"],["-8","26","-28","10"],["0","3","-6","3"],["2","-8","10","-4"]]},"deriv_order":0,"offset":3,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent_name":"Triangle read by rows: T(n,k) = number of vertices of degree k in an origami flip graph OFG(A2n)."},"identifying_rows":2,"identity":{"certificate":{"certificate":{"dividend_relation":{"terms":[{"coeff":{"coeffs":[["84","-168","84"],["157","-314","157"],["94","-188","94"],["23","-46","23"],["2","-4","2"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-256","-304"],["-384","-420"],["-208","-214"],["-48","-48"],["-4","-4"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["150"],["215"],["112"],["25"],["2"]]},"deriv_order":0,"shift":2}]},"exceptional_bases":[],"gauge":{"kind":"none"},"identifying_indices":[0,1],"index_shift":0,"input":{"first_index":0,"initial_polynomials":[["8"],["18","12"]],"recurrence":{"denominator":{"coeffs":[["0"],["3"],["10"],["9"],["2"]]},"terms":[{"coeff":{"coeffs":[["6","-12","6"],["7","-14","7"],["-4","8","-4"],["-7","14","-7"],["-2","4","-2"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["0","0"],["12","0"],["22","16"],["16","16"],["4","4"]]},"deriv_order":0,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"input_valid_from_base":0,"multiplier":["1280","3456","3920","2416","872","184","21","1"],"operator":{"schedule":{"first_degree":0,"first_index":0,"step":1},"shape":"reversal"},"parent":{"first_index":0,"initial_polynomials":[["8"],["12","18"],["16","64","32"]],"recurrence":{"denominator":{"coeffs":[["0"],["9"],["3"]]},"terms":[{"coeff":{"coeffs":[["0","0"],["8","26"],["8","5"],["2","-4"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["2","-8","8"],["7","2","-11"],["-5","2","-5"],["-4","4","8"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["0","0","0","0"],["-8","26","-28","10"],["0","3","-6","3"],["2","-8","10","-4"]]},"deriv_order":0,"offset":3,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent_leader_shift":3,"parent_valid_from_base":0,"quotients":[],"row_annihilation":{"kind":"system","system":{"generators":[{"annihilator":{"terms":[{"coeff":{"coeffs":[["23","2","-65"],["13","10","-59"],["2","2","-12"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["0","16","-42","26"],["0","4","-12","8"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["-22","14"],["-12","18"],["-2","4"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["0","-6","6"]]},"deriv_order":1,"shift":1},{"coeff":{"coeffs":[["5"],["1"]]},"deriv_order":0,"shift":2}]},"quotient":[{"coeff":{"coeffs":[["0","-38400","38400"],["0","-151040","151040"],["0","-264672","264672"],["0","-271920","271920"],["0","-181264","181264"],["0","-81864","81864"],["0","-25350","25350"],["0","-5311","5311"],["0","-720","720"],["0","-57","57"],["0","-2","2"]]},"deriv_order":0}],"step_multiplier":{"coeffs":[["0","0","102400","-204800","102400"],["0","0","424960","-849920","424960"],["0","0","791296","-1582592","791296"],["0","0","872000","-1744000","872000"],["0","0","631424","-1262848","631424"],["0","0","315248","-630496","315248"],["0","0","110672","-221344","110672"],["0","0","27308","-54616","27308"],["0","0","4640","-9280","4640"],["0","0","517","-1034","517"],["0","0","34","-68","34"],["0","0","1","-2","1"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","0","-21381120","84418560","-104693760","41656320"],["0","0","-105467904","418056192","-519708672","207120384"],["0","0","-239154176","951620096","-1185777664","473311744"],["0","0","-330394368","1319533440","-1647883776","658744704"],["0","0","-310673280","1245044544","-1558069248","623697984"],["0","0","-210346688","845581856","-1060123648","424888480"],["0","0","-105763296","426275280","-535260672","214748688"],["0","0","-40123920","162046008","-203720256","81798168"],["0","0","-11543304","46680876","-58731840","23594268"],["0","0","-2506548","10141614","-12763584","5128518"],["0","0","-404454","1635813","-2058264","826905"],["0","0","-47032","189967","-238838","95903"],["0","0","-3726","15015","-18852","7563"],["0","0","-180","723","-906","363"],["0","0","-4","16","-20","8"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","-6635520","19906560","-19906560","6635520"],["0","0","0","-29528064","88584192","-88584192","29528064"],["0","0","0","-59507712","178523136","-178523136","59507712"],["0","0","0","-71771904","215315712","-215315712","71771904"],["0","0","0","-57663360","172990080","-172990080","57663360"],["0","0","0","-32492736","97478208","-97478208","32492736"],["0","0","0","-13160160","39480480","-39480480","13160160"],["0","0","0","-3858192","11574576","-11574576","3858192"],["0","0","0","-812232","2436696","-2436696","812232"],["0","0","0","-119700","359100","-359100","119700"],["0","0","0","-11718","35154","-35154","11718"],["0","0","0","-684","2052","-2052","684"],["0","0","0","-18","54","-54","18"]]},"deriv_order":1}],[{"coeff":{"coeffs":[["0","0","-21258240","133908480","-287692800","258693120","-83650560"],["0","0","-94117888","592244736","-1275289600","1150316544","-373153792"],["0","0","-190176768","1193858688","-2575532928","2330196864","-758345856"],["0","0","-232237824","1452662976","-3138456384","2847875136","-929843904"],["0","0","-191263744","1190828352","-2575620928","2343811776","-767755456"],["0","0","-112215744","694879200","-1504131552","1372488480","-451020384"],["0","0","-48273216","297158664","-643564152","588745176","-194066472"],["0","0","-15423888","94372476","-204447780","187473684","-61974492"],["0","0","-3662208","22277880","-48269808","44354808","-14700672"],["0","0","-638532","3864288","-8373180","7707624","-2560200"],["0","0","-79502","479124","-1038158","956952","-318416"],["0","0","-6696","40236","-87180","80436","-26796"],["0","0","-342","2052","-4446","4104","-1368"],["0","0","-8","48","-104","96","-32"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","-12718080","52807680","-82114560","56678400","-14653440"],["0","0","0","-46780416","197738496","-312532992","218972160","-57397248"],["0","0","0","-77395200","333489792","-536098176","381307776","-101304192"],["0","0","0","-76103808","334626240","-547255872","395048256","-106314816"],["0","0","0","-49479168","222119232","-369482688","270524352","-73681728"],["0","0","0","-22359744","102467232","-173243232","128523744","-35388000"],["0","0","0","-7173456","33529800","-57548664","43201752","-12009432"],["0","0","0","-1634664","7781100","-13535316","10265988","-2877108"],["0","0","0","-259272","1254168","-2206872","1688328","-476352"],["0","0","0","-27240","133572","-237276","182796","-51852"],["0","0","0","-1704","8448","-15120","11712","-3336"],["0","0","0","-48","240","-432","336","-96"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","-2488320","9953280","-14929920","9953280","-2488320"],["0","0","0","0","-7962624","31850496","-47775744","31850496","-7962624"],["0","0","0","0","-11117952","44471808","-66707712","44471808","-11117952"],["0","0","0","0","-8880192","35520768","-53281152","35520768","-8880192"],["0","0","0","0","-4466880","17867520","-26801280","17867520","-4466880"],["0","0","0","0","-1466208","5864832","-8797248","5864832","-1466208"],["0","0","0","0","-313848","1255392","-1883088","1255392","-313848"],["0","0","0","0","-42228","168912","-253368","168912","-42228"],["0","0","0","0","-3240","12960","-19440","12960","-3240"],["0","0","0","0","-108","432","-648","432","-108"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","0","0","106997760","-390666240","530012160","-316016640","69672960"],["0","0","0","451602432","-1665128448","2285770752","-1382565888","310321152"],["0","0","0","867632256","-3236630400","4504097664","-2768833152","633733632"],["0","0","0","1005001536","-3801653952","5374952640","-3364949568","786649344"],["0","0","0","783611520","-3013902336","4340037888","-2772814848","663067776"],["0","0","0","434815776","-1705756320","2508374304","-1638742752","401308992"],["0","0","0","176949960","-710482872","1069748856","-715848936","179632992"],["0","0","0","53593860","-221041788","341562204","-234374484","60260208"],["0","0","0","12114540","-51498108","81807084","-57578004","15154488"],["0","0","0","2024808","-8895252","14536908","-10487292","2820828"],["0","0","0","243984","-1109328","1864080","-1376112","377376"],["0","0","0","20124","-94680","163296","-123048","34308"],["0","0","0","1020","-4956","8748","-6708","1896"],["0","0","0","24","-120","216","-168","48"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","37324800","-149299200","223948800","-149299200","37324800"],["0","0","0","0","146810880","-587243520","880865280","-587243520","146810880"],["0","0","0","0","259334784","-1037339136","1556008704","-1037339136","259334784"],["0","0","0","0","271425600","-1085702400","1628553600","-1085702400","271425600"],["0","0","0","0","186921216","-747684864","1121527296","-747684864","186921216"],["0","0","0","0","88889184","-355556736","533335104","-355556736","88889184"],["0","0","0","0","29769768","-119079072","178618608","-119079072","29769768"],["0","0","0","0","7018164","-28072656","42108984","-28072656","7018164"],["0","0","0","0","1140804","-4563216","6844824","-4563216","1140804"],["0","0","0","0","121716","-486864","730296","-486864","121716"],["0","0","0","0","7668","-30672","46008","-30672","7668"],["0","0","0","0","216","-864","1296","-864","216"]]},"deriv_order":1}]]},{"annihilator":{"terms":[{"coeff":{"coeffs":[["-24","-36"],["-26","-48"],["-9","-21"],["-1","-3"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["0","-15","15"],["0","-11","11"],["0","-2","2"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["16"],["20"],["8"],["1"]]},"deriv_order":0,"shift":1}]},"quotient":[{"coeff":{"coeffs":[["0","-32320","90240","-57920"],["0","-110064","312288","-202224"],["0","-165960","477648","-311688"],["0","-145268","423240","-277972"],["0","-81234","239076","-157842"],["0","-30048","89136","-59088"],["0","-7340","21900","-14560"],["0","-1140","3414","-2274"],["0","-102","306","-204"],["0","-4","12","-8"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","-14400","28800","-14400"],["0","0","-38640","77280","-38640"],["0","0","-43752","87504","-43752"],["0","0","-27060","54120","-27060"],["0","0","-9858","19716","-9858"],["0","0","-2112","4224","-2112"],["0","0","-246","492","-246"],["0","0","-12","24","-12"]]},"deriv_order":1}],"step_multiplier":{"coeffs":[["0","-1280","1280"],["0","-3456","3456"],["0","-3920","3920"],["0","-2416","2416"],["0","-872","872"],["0","-184","184"],["0","-21","21"],["0","-1","1"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","-622080","622080"],["0","-2405376","2405376"],["0","-4175712","4175712"],["0","-4294224","4294224"],["0","-2905584","2905584"],["0","-1357704","1357704"],["0","-446910","446910"],["0","-103593","103593"],["0","-16566","16566"],["0","-1740","1740"],["0","-108","108"],["0","-3","3"]]},"deriv_order":0}],[{"coeff":{"coeffs":[["0","-596160","1607040","-1010880"],["0","-1996272","5457888","-3461616"],["0","-2970288","8235936","-5265648"],["0","-2586336","7270368","-4684032"],["0","-1459632","4157088","-2697456"],["0","-557937","1608402","-1050465"],["0","-146286","426336","-280050"],["0","-25974","76422","-50448"],["0","-2988","8862","-5874"],["0","-201","600","-399"],["0","-6","18","-12"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","-112320","224640","-112320"],["0","0","-309744","619488","-309744"],["0","0","-366096","732192","-366096"],["0","0","-241968","483936","-241968"],["0","0","-97728","195456","-97728"],["0","0","-24681","49362","-24681"],["0","0","-3804","7608","-3804"],["0","0","-327","654","-327"],["0","0","-12","24","-12"]]},"deriv_order":1}],[{"coeff":{"coeffs":[["0","0","1684800","-3369600","1684800"],["0","0","5881680","-11763360","5881680"],["0","0","9123264","-18246528","9123264"],["0","0","8276064","-16552128","8276064"],["0","0","4859760","-9719520","4859760"],["0","0","1929159","-3858318","1929159"],["0","0","524007","-1048014","524007"],["0","0","96111","-192222","96111"],["0","0","11385","-22770","11385"],["0","0","786","-1572","786"],["0","0","24","-48","24"]]},"deriv_order":0}]]},{"annihilator":{"terms":[{"coeff":{"coeffs":[["0"],["2"],["1"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-2","-1"],["0","-2"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","-1","1"]]},"deriv_order":2,"shift":0}]},"quotient":[{"coeff":{"coeffs":[["0","0","216000","-432000","216000"],["0","0","738000","-1476000","738000"],["0","0","1110120","-2220240","1110120"],["0","0","964452","-1928904","964452"],["0","0","533034","-1066068","533034"],["0","0","194238","-388476","194238"],["0","0","46638","-93276","46638"],["0","0","7110","-14220","7110"],["0","0","624","-1248","624"],["0","0","24","-48","24"]]},"deriv_order":0}],"step_multiplier":{"coeffs":[["0","0","4096","-8192","4096"],["0","0","15360","-30720","15360"],["0","0","25344","-50688","25344"],["0","0","24128","-48256","24128"],["0","0","14592","-29184","14592"],["0","0","5808","-11616","5808"],["0","0","1520","-3040","1520"],["0","0","252","-504","252"],["0","0","24","-48","24"],["0","0","1","-2","1"]]},"step_quotients":[[],[{"coeff":{"coeffs":[["0","0","41472","-82944","41472"],["0","0","179712","-359424","179712"],["0","0","340128","-680256","340128"],["0","0","371280","-742560","371280"],["0","0","259296","-518592","259296"],["0","0","121176","-242352","121176"],["0","0","38394","-76788","38394"],["0","0","8145","-16290","8145"],["0","0","1107","-2214","1107"],["0","0","87","-174","87"],["0","0","3","-6","3"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","-27648","13824","55296","-41472"],["0","0","-82944","13824","221184","-152064"],["0","0","-106944","-29472","379776","-243360"],["0","0","-77280","-68304","368448","-222864"],["0","0","-34176","-60192","222912","-128544"],["0","0","-9456","-29448","87264","-48360"],["0","0","-1596","-8658","22104","-11850"],["0","0","-150","-1521","3492","-1821"],["0","0","-6","-147","312","-159"],["0","0","0","-6","12","-6"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","-13824","41472","-41472","13824"],["0","0","0","-41472","124416","-124416","41472"],["0","0","0","-53472","160416","-160416","53472"],["0","0","0","-38640","115920","-115920","38640"],["0","0","0","-17088","51264","-51264","17088"],["0","0","0","-4728","14184","-14184","4728"],["0","0","0","-798","2394","-2394","798"],["0","0","0","-75","225","-225","75"],["0","0","0","-3","9","-9","3"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","0","539136","-580608","-456192","497664"],["0","0","2128896","-2101248","-2184192","2156544"],["0","0","3771936","-3337920","-4639968","4205952"],["0","0","3955440","-3040800","-5784720","4870080"],["0","0","2725776","-1734336","-4708656","3717216"],["0","0","1295160","-628032","-2629416","1962288"],["0","0","432666","-134892","-1028214","730440"],["0","0","101547","-11538","-281565","191556"],["0","0","16398","1854","-52902","34650"],["0","0","1734","645","-6492","4113"],["0","0","108","72","-468","288"],["0","0","3","3","-15","9"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","207360","-622080","622080","-207360"],["0","0","0","774144","-2322432","2322432","-774144"],["0","0","0","1285920","-3857760","3857760","-1285920"],["0","0","0","1250736","-3752208","3752208","-1250736"],["0","0","0","788304","-2364912","2364912","-788304"],["0","0","0","336168","-1008504","1008504","-336168"],["0","0","0","98154","-294462","294462","-98154"],["0","0","0","19359","-58077","58077","-19359"],["0","0","0","2466","-7398","7398","-2466"],["0","0","0","183","-549","549","-183"],["0","0","0","6","-18","18","-6"]]},"deriv_order":1}]]}],"restart_bases":[],"row_multiplier":{"coeffs":[["0","-1","1"]]},"start_base":0}},"shifted_parent_relation":{"terms":[{"coeff":{"coeffs":[["-30","111","-132","51"],["-46","172","-206","80"],["-18","69","-84","33"],["-2","8","-10","4"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["130","-124","-146"],["131","-122","-175"],["41","-38","-67"],["4","-4","-8"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["-150","-15"],["-110","52"],["-26","31"],["-2","4"]]},"deriv_order":0,"shift":2},{"coeff":{"coeffs":[["54"],["27"],["3"]]},"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 = 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 2 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":[["8"],["12","18"],["16","64","32"]],"recurrence":{"denominator":{"coeffs":[["0"],["9"],["3"]]},"terms":[{"coeff":{"coeffs":[["0","0"],["8","26"],["8","5"],["2","-4"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["2","-8","8"],["7","2","-11"],["-5","2","-5"],["-4","4","8"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["0","0","0","0"],["-8","26","-28","10"],["0","3","-6","3"],["2","-8","10","-4"]]},"deriv_order":0,"offset":3,"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":"not applicable: the rule is not f(n) P_n = c_0(n, x) P_(n-1) + c_1(n, x) P'_(n-1) + c_2(n, x) P_(n-2) with a derivative or a lag term","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+1) is not shown to be >= 0 for n >= 3","route":"attestation","success":false,"variant":"oeis_catalog:A352880:lean_proved"}],"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"}