{"certification":{"candidate":{"gauge":{"kind":"none"},"index_shift":0,"operator":{"intercept":"0","shape":"affine","slope":"1"},"parent":{"first_index":0,"initial_polynomials":[["1"],["4","3"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","1"]]},"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"],["-5"],["-3"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-11","-20","-8"],["13","16","4"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["-13","-29","-20","-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"],["4","3"]],"recurrence":{"denominator":{"coeffs":[["-2"],["2"]]},"terms":[{"coeff":{"coeffs":[["-2"],["-1"],["3"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["24","36","12"],["-13","-16","-4"]]},"deriv_order":1,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["13","29","20","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"],["4","3"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","1"]]},"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":[["-16","-12"],["-15","-18"],["-3","-6"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["15","16","-8","-8"],["13","42","36","8"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["-13","-55","-78","-44","-8"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["4"]]},"deriv_order":0,"shift":1}]},"quotient":[{"coeff":{"coeffs":[["0","0","0","0","0"],["-52","-116","-80","-16","0"],["26","110","156","88","16"]]},"deriv_order":0}],"step_multiplier":{"coeffs":[["-1124864","-7527936","-21984768","-36688384","-38455296","-26179584","-11542528","-3170304","-491520","-32768","0","0","0"],["1687296","14666496","55560960","120986880","167748096","154635264","95852544","39383040","10248192","1523712","98304","0","0"],["-843648","-9020544","-42446976","-116054400","-204860928","-245065728","-202561536","-115544064","-44507136","-11010048","-1572864","-98304","0"],["140608","1784640","10081344","33491392","72828288","109131264","115448832","86777856","45932544","16670720","3932160","540672","32768"]]},"step_quotients":[[{"coeff":{"coeffs":[["6186752","49277696","173611776","355679488","468322816","413174784","246740992","98234368","24895488","3620864","229376","0","0","0"],["-3374592","-44518656","-236371200","-696854784","-1292469504","-1598873088","-1352690688","-784361472","-305688576","-76259328","-10960896","-688128","0","0"],["-3374592","-26802048","-77311104","-55966848","234910848","789259776","1214484480","1147459584","709545984","288006144","73826304","10813440","688128","0"],["2390336","29354624","158890368","498784256","1003641152","1345433472","1198711296","667081728","173408256","-38125568","-49848320","-18333696","-3227648","-229376"],["-105456","-2393040","-20945808","-100728624","-305806656","-628060608","-905071104","-930949632","-685283328","-356997120","-127979520","-29896704","-4079616","-245760"],["-105456","-1549392","-10237968","-40240560","-104858304","-191090880","-250283520","-238256640","-164616192","-81401856","-27955200","-6303744","-835584","-49152"]]},"deriv_order":0},{"coeff":{"coeffs":[["-7874048","-69006080","-270922496","-628293376","-955062016","-997677568","-729588736","-372815872","-130207744","-29548544","-3915776","-229376","0","0","0","0"],["8155264","90854400","452784384","1335129088","2594346624","3498673152","3355542528","2303963136","1122631680","378060800","83410944","10813440","622592","0","0","0"],["-421824","-9993984","-84075264","-379035264","-1069018944","-2034400896","-2718512640","-2599750656","-1786097664","-872521728","-294887424","-65323008","-8503296","-491520","0","0"],["-1757600","-23643776","-142830272","-512630528","-1218440480","-2022518144","-2407029120","-2072355840","-1283097600","-557965312","-161591296","-27443200","-1613824","229376","32768","0"],["456976","7276464","52768560","231044112","682652928","1440958848","2243524352","2622078720","2317750272","1548369920","774770688","284946432","74514432","13074432","1376256","65536"]]},"deriv_order":1},{"coeff":{"coeffs":[["3655808","39932672","196894464","580696064","1143204992","1586155776","1594902528","1175900160","635154432","248012800","67993600","12386304","1343488","65536","0","0","0"],["-5483712","-70866432","-415139712","-1461727488","-3456895680","-5808848640","-7150821120","-6548557824","-4480432128","-2277482496","-846028800","-222560256","-39174144","-4128768","-196608","0","0"],["2741856","40916928","278436288","1146003456","3190175328","6361320000","9384259200","10425100032","8788773888","5619173376","2700496896","957308928","242147328","41238528","4227072","196608","0"],["-456976","-7733440","-60045024","-283812672","-913697040","-2123611776","-3684483200","-4865603072","-4939828992","-3866120192","-2323140608","-1059717120","-359460864","-87588864","-14450688","-1441792","-65536"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["-281216","-2444416","-8135296","-10386816","9082624","54885376","95856640","96526336","62193664","26001408","6815744","1015808","65536","0"],["984256","13054912","76020672","256724032","558869632","823123200","834945024","579108864","263516160","69337088","5193728","-2506752","-753664","-65536"],["632736","6765408","29304288","59979168","26304768","-164363904","-462661632","-648539136","-574304256","-338374656","-132341760","-32956416","-4718592","-294912"],["-316368","-5070000","-36067824","-150965712","-415049088","-791757504","-1078244352","-1061116416","-754182144","-382003200","-133877760","-30707712","-4128768","-245760"],["-105456","-1549392","-10237968","-40240560","-104858304","-191090880","-250283520","-238256640","-164616192","-81401856","-27955200","-6303744","-835584","-49152"]]},"deriv_order":0},{"coeff":{"coeffs":[["281216","2444416","7572864","4373120","-37380608","-132254976","-232430592","-259903488","-197234688","-103030784","-36487168","-8355840","-1114112","-65536","0","0"],["-281216","-4834752","-34255936","-136104512","-342022464","-574625536","-657700608","-504201216","-236845056","-42090496","22978560","18890752","6078464","983040","65536","0"],["-843648","-10918752","-62743200","-210716448","-456962784","-663555840","-637905024","-366446592","-59415552","91410432","89198592","40869888","10788864","1572864","98304","0"],["456976","7276464","52768560","231044112","682652928","1440958848","2243524352","2622078720","2317750272","1548369920","774770688","284946432","74514432","13074432","1376256","65536"]]},"deriv_order":1},{"coeff":{"coeffs":[["-1827904","-23622144","-138379904","-487242496","-1152298560","-1936282880","-2383607040","-2182852608","-1493477376","-759160832","-282009600","-74186752","-13058048","-1376256","-65536","0","0"],["1827904","27277952","185624192","764002304","2126783552","4240880000","6256172800","6950066688","5859182592","3746115584","1800331264","638205952","161431552","27492352","2818048","131072","0"],["-456976","-7733440","-60045024","-283812672","-913697040","-2123611776","-3684483200","-4865603072","-4939828992","-3866120192","-2323140608","-1059717120","-359460864","-87588864","-14450688","-1441792","-65536"]]},"deriv_order":2}]]},{"annihilator":{"terms":[{"coeff":{"coeffs":[["0","0"],["6","12"],["9","18"],["3","6"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-22","-40","-16","0"],["11","16","16","8"],["-13","-42","-36","-8"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["-26","-58","-40","-8","0"],["13","55","78","44","8"]]},"deriv_order":2,"shift":0}]},"quotient":[{"coeff":{"coeffs":[["-52","-116","-80","-16","0"],["26","110","156","88","16"]]},"deriv_order":0}],"step_multiplier":{"coeffs":[["-1124864","-7527936","-21984768","-36688384","-38455296","-26179584","-11542528","-3170304","-491520","-32768","0","0","0"],["1687296","14666496","55560960","120986880","167748096","154635264","95852544","39383040","10248192","1523712","98304","0","0"],["-843648","-9020544","-42446976","-116054400","-204860928","-245065728","-202561536","-115544064","-44507136","-11010048","-1572864","-98304","0"],["140608","1784640","10081344","33491392","72828288","109131264","115448832","86777856","45932544","16670720","3932160","540672","32768"]]},"step_quotients":[[{"coeff":{"coeffs":[["-5061888","-43999488","-166682880","-362960640","-503244288","-463905792","-287557632","-118149120","-30744576","-4571136","-294912","0","0","0"],["-1687296","519168","76437504","379061760","921133824","1355097600","1295864832","823289856","344199168","90710016","13615104","884736","0","0"],["5061888","56654208","261495936","647669376","910597248","633134592","-62410752","-554674176","-536555520","-273014784","-80510976","-12976128","-884736","0"],["421824","-5191680","-83356416","-432384384","-1215976128","-2127178368","-2437888512","-1845758976","-890523648","-238460928","-12804096","11943936","3391488","294912"],["-1370928","-17611152","-95908176","-287539824","-505631040","-476945856","-60157440","451137024","637360128","461826048","203698176","54890496","8306688","540672"],["0","1265472","16061760","90732096","301422528","655454592","982181376","1039039488","781000704","413392896","150036480","35389440","4866048","294912"],["105456","1549392","10237968","40240560","104858304","191090880","250283520","238256640","164616192","81401856","27955200","6303744","835584","49152"]]},"deriv_order":0},{"coeff":{"coeffs":[["6749184","63727872","266243328","650630400","1033953024","1121785344","847315968","445089792","159141888","36839424","4964352","294912","0","0","0","0"],["-5905536","-68486912","-364382720","-1155712256","-2412068224","-3475016704","-3536241664","-2558046208","-1304289280","-456736768","-104185856","-13893632","-819200","0","0","0"],["2390336","20636928","90425088","291022208","756193728","1521580416","2255881728","2407578624","1828552704","974209024","354263040","83410944","11419648","688128","0","0"],["-3163680","-30241536","-116620608","-210545280","-71782944","489487488","1190173824","1448064000","1091902464","523026432","147886080","16859136","-2727936","-1081344","-98304","0"],["2214576","29092336","170148784","583500496","1297265248","1940521600","1932628864","1156186368","189029376","-341028864","-362389504","-189190144","-60497920","-11960320","-1343488","-65536"],["-456976","-7276464","-52768560","-231044112","-682652928","-1440958848","-2243524352","-2622078720","-2317750272","-1548369920","-774770688","-284946432","-74514432","-13074432","-1376256","-65536"]]},"deriv_order":1},{"coeff":{"coeffs":[["3655808","25309440","66410240","54086656","-126360448","-447533312","-682342400","-649220096","-418205696","-185884672","-56262656","-11075584","-1277952","-65536","0","0","0"],["-9139520","-88864256","-372438144","-861056768","-1115924288","-535774464","771211008","1844957184","1939814400","1285431296","574054400","173015040","33800192","3866624","196608","0","0"],["8225568","100815936","551843136","1777451520","3723616032","5256377280","4917383040","2672015616","172090368","-1064208384","-1008439296","-512188416","-163799040","-32980992","-3833856","-196608","0"],["-3198832","-46822464","-311203360","-1244191936","-3339870064","-6358148224","-8827862400","-9034530304","-6778536192","-3626110976","-1277521920","-216694784","36597760","32604160","8814592","1179648","65536"],["456976","7733440","60045024","283812672","913697040","2123611776","3684483200","4865603072","4939828992","3866120192","2323140608","1059717120","359460864","87588864","14450688","1441792","65536"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["5343104","44194176","164261760","359489664","508723968","478863360","293163008","103256064","8380416","-9732096","-4620288","-884736","-65536","0"],["140608","-8339136","-80729792","-336692032","-826252160","-1325778688","-1451545600","-1095694336","-561184768","-185065472","-34078720","-1654784","491520","65536"],["-3444896","-37677536","-185439072","-535912736","-990876800","-1186591104","-855453696","-230956032","197074944","253693952","134438912","39641088","6324224","425984"],["175760","3144752","27576432","143475152","478517312","1074015552","1673107968","1839152640","1431717888","781576192","291303424","70275072","9846784","606208"],["210912","3942432","31183776","140969184","410664960","819151488","1155354624","1169206272","849899520","438398976","155934720","36200448","4915200","294912"],["105456","1549392","10237968","40240560","104858304","191090880","250283520","238256640","164616192","81401856","27955200","6303744","835584","49152"]]},"deriv_order":0},{"coeff":{"coeffs":[["-7030400","-63922560","-263259776","-645645184","-1041246464","-1147312384","-863100928","-420640768","-106455040","8323072","16941056","5963776","983040","65536","0","0"],["6749184","73711040","369049408","1123759680","2320495808","3420575488","3681768192","2903838720","1654831104","656080896","165584896","19841024","-1327104","-720896","-65536","0"],["-2390336","-26331552","-129941344","-384733280","-778615392","-1174609024","-1410796416","-1399507968","-1141441536","-737210368","-358330368","-123920384","-28401664","-3833856","-229376","0"],["1300624","16367312","90061712","281586416","535787552","581559296","163504768","-549722880","-1034652672","-990404608","-613179392","-257503232","-72900608","-13303808","-1409024","-65536"],["-456976","-7276464","-52768560","-231044112","-682652928","-1440958848","-2243524352","-2622078720","-2317750272","-1548369920","-774770688","-284946432","-74514432","-13074432","-1376256","-65536"]]},"deriv_order":1},{"coeff":{"coeffs":[["-1827904","-16310528","-58514560","-93453568","9093568","350127104","788704512","1006952448","858322944","511148032","214016000","61800448","11714560","1310720","65536","0","0"],["3655808","43588480","229515520","697725184","1330112128","1567968640","894648320","-401508864","-1378750464","-1468633088","-954302464","-415645696","-122257408","-23363584","-2621440","-131072","0"],["-2284880","-33183488","-218391264","-862190784","-2276478288","-4237708224","-5699776000","-5559496960","-3848944896","-1753053184","-377356288","102408192","117313536","46350336","10223616","1245184","65536"],["456976","7733440","60045024","283812672","913697040","2123611776","3684483200","4865603072","4939828992","3866120192","2323140608","1059717120","359460864","87588864","14450688","1441792","65536"]]},"deriv_order":2}]]}],"restart_bases":[],"row_multiplier":{"coeffs":[["-104","-232","-160","-32","0"],["52","220","312","176","32"]]},"start_base":1}},"shifted_parent_relation":{"terms":[{"coeff":{"coeffs":[["-1","-1"]]},"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"],["4","3"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","1"]]},"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) = (1) + (1) x; open hypotheses: multipliers_vanish_at_zero: [x^0] c_2(n, x) = 1 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 = 1 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 = 1 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"}