{"certification":{"candidate":{"gauge":{"kind":"none"},"index_shift":0,"operator":{"intercept":"0","shape":"affine","slope":"1"},"parent":{"first_index":0,"initial_polynomials":[["1"],["5","4"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["2","2"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["3","2"]]},"deriv_order":0,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent_name":"existing definition"},"identifying_rows":2,"identity":{"certificate":{"certificate":{"dividend_relation":{"terms":[{"coeff":{"coeffs":[["0"],["-6"],["-4"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-13","-22","-8"],["17","20","4"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["-17","-37","-24","-4"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["0"],["2"]]},"deriv_order":0,"shift":1}]},"exceptional_bases":[],"gauge":{"kind":"none"},"identifying_indices":[0,1],"index_shift":0,"input":{"first_index":0,"initial_polynomials":[["1"],["5","4"]],"recurrence":{"denominator":{"coeffs":[["-2"],["2"]]},"terms":[{"coeff":{"coeffs":[["-2"],["-2"],["4"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["30","42","12"],["-17","-20","-4"]]},"deriv_order":1,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["17","37","24","4"]]},"deriv_order":2,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"input_valid_from_base":1,"multiplier":["1"],"operator":{"intercept":"0","shape":"affine","slope":"1"},"parent":{"first_index":0,"initial_polynomials":[["1"],["5","4"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["2","2"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["3","2"]]},"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":[["-20","-16"],["-20","-24"],["-4","-8"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["21","26","-4","-8"],["17","54","44","8"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["-17","-71","-98","-52","-8"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["4"]]},"deriv_order":0,"shift":1}]},"quotient":[{"coeff":{"coeffs":[["0","0","0","0","0"],["-68","-148","-96","-16","0"],["34","142","196","104","16"]]},"deriv_order":0}],"step_multiplier":{"coeffs":[["-2515456","-16424448","-46401024","-74084864","-73236480","-46159872","-18407424","-4448256","-589824","-32768","0","0","0"],["3773184","32183040","118874880","250330368","332109312","288949248","166090752","61894656","14229504","1818624","98304","0","0"],["-1886592","-19864704","-91620480","-244040064","-416385024","-476583936","-371994624","-197038080","-69009408","-15138816","-1867776","-98304","0"],["314432","3939648","21891648","71213504","150744192","218225664","220860416","156837888","77180928","25526272","5357568","638976","32768"]]},"step_quotients":[[{"coeff":{"coeffs":[["20123648","156550144","535452672","1056689152","1326740480","1101643776","608858112","219660288","49201152","6160384","327680","0","0","0"],["-12577280","-155070464","-783777792","-2208787456","-3906674176","-4577203200","-3627767808","-1940852736","-684171264","-150716416","-18644992","-983040","0","0"],["-8804096","-63774208","-143093760","94350848","1164818176","2825416704","3800395776","3243343872","1813389312","657391616","147521536","18481152","983040","0"],["6917504","83527936","442219776","1347780608","2604237184","3293522688","2676672512","1241829376","129601536","-210231296","-137396224","-39518208","-5668864","-327680"],["-314432","-7083968","-61288128","-290129984","-862879232","-1725667584","-2403117056","-2365442048","-1645559808","-797335552","-260620288","-54214656","-6422528","-327680"],["-314432","-4568512","-29770944","-114996800","-293171200","-519714048","-657311744","-598558720","-390856704","-179888128","-56410112","-11354112","-1310720","-65536"]]},"deriv_order":0},{"coeff":{"coeffs":[["-23896832","-206341376","-794453248","-1796071168","-2641454080","-2644097024","-1830432768","-872005632","-278642688","-56590336","-6553600","-327680","0","0","0","0"],["25154560","277440000","1364099584","3950492160","7495733760","9797900288","9022779392","5877669888","2676621312","826966016","163774464","18612224","917504","0","0","0"],["-1886592","-38730624","-305360256","-1319162496","-3589749504","-6592754688","-8468914176","-7729655808","-5015347200","-2281537536","-705331200","-139886592","-15925248","-786432","0","0"],["-5030912","-66178688","-388405120","-1342573952","-3036475520","-4714198528","-5113046528","-3845107712","-1919832064","-552878080","-32260096","38305792","14516224","2228224","131072","0"],["1336336","20988336","149683504","642159632","1850732544","3789637504","5685316352","6350147328","5311246336","3317366784","1530040320","510193664","118751232","18186240","1638400","65536"]]},"deriv_order":1},{"coeff":{"coeffs":[["10690688","114453248","550366976","1573578752","2981635200","3947268352","3747768320","2576797696","1278996480","451207168","109674496","17367040","1605632","65536","0","0","0"],["-16036032","-203751936","-1168910208","-4011469056","-9193189056","-14865808128","-17463457536","-15108501504","-9648887808","-4513800192","-1518133248","-355074048","-54509568","-4915200","-196608","0","0"],["8018016","117912000","788207040","3174644736","8608063584","16626093120","23597536896","25017708288","19932945408","11905787904","5272866816","1695670272","382328832","56967168","5013504","196608","0"],["-1336336","-22324672","-170671840","-791843136","-2492892176","-5640370048","-9474953856","-12035463680","-11661393664","-8628613120","-4847407104","-2040233984","-628944896","-136937472","-19824640","-1703936","-65536"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["-1257728","-11985408","-47837184","-101613056","-114896640","-40132608","69726208","116637696","85352448","35913728","8847360","1179648","65536","0"],["3144320","41283072","237523456","790512384","1690401664","2435948288","2407598080","1622650880","720850944","192913408","22708224","-1835008","-819200","-65536"],["1886592","19864704","84074112","164581248","49903104","-499576320","-1293545472","-1709297664","-1418969088","-773013504","-274169856","-60456960","-7471104","-393216"],["-943296","-14963264","-105071424","-432556992","-1164367616","-2162118912","-2844837888","-2679117824","-1799921664","-848388096","-271335424","-55492608","-6488064","-327680"],["-314432","-4568512","-29770944","-114996800","-293171200","-519714048","-657311744","-598558720","-390856704","-179888128","-56410112","-11354112","-1310720","-65536"]]},"deriv_order":0},{"coeff":{"coeffs":[["1257728","12614272","53201024","118910080","135163008","16234240","-188454912","-310362112","-267669504","-144269312","-49807360","-10649600","-1277952","-65536","0","0"],["-1257728","-20475072","-141001536","-552376896","-1383074752","-2340865024","-2744978176","-2232915968","-1227585536","-420708352","-65937408","8503296","5980160","1048576","65536","0"],["-2358240","-29547360","-162300768","-510463392","-999231552","-1209411456","-751987968","133069824","746305536","749580288","422903808","148365312","31899648","3833856","196608","0"],["1336336","20988336","149683504","642159632","1850732544","3789637504","5685316352","6350147328","5311246336","3317366784","1530040320","510193664","118751232","18186240","1638400","65536"]]},"deriv_order":1},{"coeff":{"coeffs":[["-5345344","-67917312","-389636736","-1337156352","-3064396352","-4955269376","-5821152512","-5036167168","-3216295936","-1504600064","-506044416","-118358016","-18169856","-1638400","-65536","0","0"],["5345344","78608000","525471360","2116429824","5738709056","11084062080","15731691264","16678472192","13288630272","7937191936","3515244544","1130446848","254885888","37978112","3342336","131072","0"],["-1336336","-22324672","-170671840","-791843136","-2492892176","-5640370048","-9474953856","-12035463680","-11661393664","-8628613120","-4847407104","-2040233984","-628944896","-136937472","-19824640","-1703936","-65536"]]},"deriv_order":2}]]},{"annihilator":{"terms":[{"coeff":{"coeffs":[["0","0"],["8","16"],["12","24"],["4","8"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-26","-44","-16","0"],["13","14","12","8"],["-17","-54","-44","-8"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["-34","-74","-48","-8","0"],["17","71","98","52","8"]]},"deriv_order":2,"shift":0}]},"quotient":[{"coeff":{"coeffs":[["-68","-148","-96","-16","0"],["34","142","196","104","16"]]},"deriv_order":0}],"step_multiplier":{"coeffs":[["-2515456","-16424448","-46401024","-74084864","-73236480","-46159872","-18407424","-4448256","-589824","-32768","0","0","0"],["3773184","32183040","118874880","250330368","332109312","288949248","166090752","61894656","14229504","1818624","98304","0","0"],["-1886592","-19864704","-91620480","-244040064","-416385024","-476583936","-371994624","-197038080","-69009408","-15138816","-1867776","-98304","0"],["314432","3939648","21891648","71213504","150744192","218225664","220860416","156837888","77180928","25526272","5357568","638976","32768"]]},"step_quotients":[[{"coeff":{"coeffs":[["-15092736","-128732160","-475499520","-1001321472","-1328437248","-1155796992","-664363008","-247578624","-56918016","-7274496","-393216","0","0","0"],["-5030912","2367488","227696640","1092724736","2561152000","3600046080","3245936640","1910562816","723763200","168329216","21692416","1179648","0","0"],["15092736","166464000","752051712","1803873792","2405242368","1472925696","-431456256","-1558904832","-1317224448","-593166336","-152174592","-20840448","-1179648","0"],["1257728","-15684608","-246027264","-1248516608","-3414875392","-5758235136","-6279708672","-4436754432","-1930174464","-424951808","7208960","27131904","5701632","393216"],["-4087616","-51844288","-277377984","-810641216","-1369137664","-1186101504","23443456","1332058112","1658929152","1090101248","431374336","102088704","13238272","720896"],["0","3773184","47275776","262699776","854562048","1808930304","2618707968","2650324992","1882054656","926171136","306315264","64290816","7667712","393216"],["314432","4568512","29770944","114996800","293171200","519714048","657311744","598558720","390856704","179888128","56410112","11354112","1310720","65536"]]},"deriv_order":0},{"coeff":{"coeffs":[["18865920","176007936","723106560","1727151360","2661868032","2773183488","1986250752","973836288","318726144","66011136","7766016","393216","0","0","0","0"],["-15092736","-175268096","-935310080","-2963581696","-6134301952","-8681568256","-8577867776","-5940068352","-2849906688","-919830528","-188809216","-22085632","-1114112","0","0","0"],["5030912","34735488","121470848","392863104","1252509312","3023974144","4976982016","5547982848","4213813248","2168922112","738459648","157843456","19038208","983040","0","0"],["-8489664","-75241728","-248214144","-255882240","649802304","2747339520","4743403776","4883189760","3190032384","1281761280","263135232","-3342336","-14598144","-2949120","-196608","0"],["6367248","81821680","464825968","1532524880","3222986944","4429348096","3788788736","1473137920","-725276672","-1462030336","-1042616320","-438439936","-115884032","-18808832","-1703936","-65536"],["-1336336","-20988336","-149683504","-642159632","-1850732544","-3789637504","-5685316352","-6350147328","-5311246336","-3317366784","-1530040320","-510193664","-118751232","-18186240","-1638400","-65536"]]},"deriv_order":1},{"coeff":{"coeffs":[["10690688","71690496","178079488","116685824","-398893952","-1218214144","-1710340096","-1498058752","-878481408","-349822976","-93093888","-15794176","-1540096","-65536","0","0","0"],["-26726720","-254061056","-1032557696","-2282845952","-2733351744","-923265280","2472384256","4801310720","4532901888","2708971520","1079435264","285605888","48087040","4653056","196608","0","0"],["24054048","289591872","1549613376","4848293376","9778314528","13105523136","11329378176","5199294720","-635169792","-2878187520","-2236600320","-985522176","-273309696","-47136768","-4620288","-196608","0"],["-9354352","-134891328","-880270880","-3441016512","-8984525936","-16527754112","-21988428672","-21321480704","-14915866880","-7245770752","-2183081984","-220659712","119173120","60981248","13139968","1441792","65536"],["1336336","22324672","170671840","791843136","2492892176","5640370048","9474953856","12035463680","11661393664","8628613120","4847407104","2040233984","628944896","136937472","19824640","1703936","65536"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["16350464","130655744","467700736","983028224","1332598528","1199323136","702943232","241950720","27402240","-13205504","-6225920","-1048576","-65536","0"],["-628864","-32404992","-255488512","-974300928","-2249221504","-3425215232","-3559768064","-2536275968","-1213329408","-368599040","-61931520","-3080192","557056","65536"],["-9432960","-101838976","-494650496","-1408058752","-2552668672","-2971648000","-2045947904","-480464896","490389504","553058304","262635520","68059136","9306112","524288"],["314432","6455104","63470656","352291776","1209094784","2725726208","4187385856","4465502208","3315855360","1693843456","577617920","124239872","15106048","786432"],["628864","11652480","91059072","405126784","1156050432","2245381632","3060428800","2964000768","2036416512","977223680","317030400","65568768","7733248","393216"],["314432","4568512","29770944","114996800","293171200","519714048","657311744","598558720","390856704","179888128","56410112","11354112","1310720","65536"]]},"deriv_order":0},{"coeff":{"coeffs":[["-20123648","-178560384","-715640704","-1703368064","-2659191424","-2830245632","-2055968768","-975110144","-254717952","-1908736","23199744","7831552","1146880","65536","0","0"],["18865920","200848064","978369856","2896199744","5813881792","8332038144","8713272064","6662436864","3666950144","1398571008","340860928","42352640","-475136","-786432","-65536","0"],["-6445856","-67556640","-311612448","-844686816","-1539811648","-2108372608","-2421402880","-2475748352","-2163550208","-1477242880","-729661440","-245194752","-52314112","-6324224","-327680","0"],["3694576","45190352","238721616","700414320","1185742976","924561024","-572269824","-2505039616","-3391414272","-2764488704","-1497780224","-548499456","-133267456","-20414464","-1769472","-65536"],["-1336336","-20988336","-149683504","-642159632","-1850732544","-3789637504","-5685316352","-6350147328","-5311246336","-3317366784","-1530040320","-510193664","-118751232","-18186240","-1638400","-65536"]]},"deriv_order":1},{"coeff":{"coeffs":[["-5345344","-46535936","-160730240","-236422400","82761152","1008001024","2073384192","2459369472","1937299456","1053392896","396369920","100990976","16564224","1572864","65536","0","0"],["10690688","125143936","643438848","1895039232","3454480000","3781746048","1731766272","-1569970688","-3639742464","-3423391744","-1997111296","-775372800","-200376320","-33062912","-3145728","-131072","0"],["-6681680","-95587328","-617535200","-2382801600","-6115171408","-10985723072","-14122583040","-12982244608","-8271551744","-3277174784","-425459712","344563712","246616064","79970304","14811136","1507328","65536"],["1336336","22324672","170671840","791843136","2492892176","5640370048","9474953856","12035463680","11661393664","8628613120","4847407104","2040233984","628944896","136937472","19824640","1703936","65536"]]},"deriv_order":2}]]}],"restart_bases":[],"row_multiplier":{"coeffs":[["-136","-296","-192","-32","0"],["68","284","392","208","32"]]},"start_base":1}},"shifted_parent_relation":{"terms":[{"coeff":{"coeffs":[["-2","-2"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-3","-2"]]},"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 + (0)); so the candidate rows satisfy the input rule at every base n >= 1 (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":"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 + (0))","kind":"preserver_image","operator":{"intercept":"0","shape":"affine","slope":"1"}},"parent":{"gauge":{"kind":"none"},"index_shift":0,"recurrence":{"first_index":0,"initial_polynomials":[["1"],["5","4"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["2","2"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["3","2"]]},"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 + (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 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":"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) = (3) + (2) x, V_n(x) = 0, W_n(x) = (2) + (2) x; open hypotheses: multipliers_vanish_at_zero: [x^0] c_2(n, x) = 2 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 = 2 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 = 2 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"}],"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 = P((1) x + (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":"definition_equality"}