{"certification":{"candidate":{"gauge":{"kind":"none"},"index_shift":0,"operator":{"coefficients":[{"denominator":["1"],"numerator":["0"]},{"denominator":["1"],"numerator":["1"]}],"shape":"derivative_polynomial"},"parent":{"first_index":0,"initial_polynomials":[["1"],["3","6"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["-1"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["3","3"]]},"deriv_order":0,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent_name":"basis_map_A013610 of Triangle of coefficients of polynomials v(n,x) jointly generated with A207606; see Formula section."},"identifying_rows":2,"identity":{"certificate":{"certificate":{"dividend_relation":{"terms":[{"coeff":{"coeffs":[["72","108","0"],["117","126","-54"],["36","-45","-108"],["-9","-63","-54"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["30","108","54","0"],["10","6","-90","-54"],["-5","-48","-117","-54"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["0","0"],["-27","0"],["-27","0"],["6","36"]]},"deriv_order":1,"shift":1}]},"exceptional_bases":[],"gauge":{"kind":"none"},"identifying_indices":[0,1],"index_shift":0,"input":{"first_index":0,"initial_polynomials":[["0"],["6"]],"recurrence":{"denominator":{"coeffs":[["-6","-36"],["45","108"],["-45","-108"],["6","36"]]},"terms":[{"coeff":{"coeffs":[["0","0","0"],["-18","-27","0"],["-63","-144","-54"],["9","63","54"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["-15","-54","-27","0"],["-20","-102","-144","-54"],["5","48","117","54"]]},"deriv_order":1,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"input_valid_from_base":1,"multiplier":["1"],"operator":{"coefficients":[{"denominator":["1"],"numerator":["0"]},{"denominator":["1"],"numerator":["1"]}],"shape":"derivative_polynomial"},"parent":{"first_index":0,"initial_polynomials":[["1"],["3","6"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["-1"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["3","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":[["-162","-324","0"],["-27","-162","0"],["9","108","324"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["18","126","54","-324"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["-5","-78","-405","-756","-324"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["54"]]},"deriv_order":0,"shift":1}]},"quotient":[{"coeff":{"coeffs":[["0","0","0","0","0","0","0","0"],["-6075","-43740","-100602","-78732","-19683","0","0","0"],["2025","63180","383454","831060","636417","157464","0","0"],["6750","72900","189540","-209952","-1272834","-1180980","-314928","0"],["-4500","-86400","-625320","-2118960","-3397140","-2274480","-524880","0"],["600","15120","152496","782784","2148120","3020976","1889568","419904"]]},"deriv_order":1}],"step_multiplier":{"coeffs":[["-531441000","-5739562800","-23532207480","-45457337376","-42357973464","-18596183472","-3099363912","0","0","0"],["1062882000","17856417600","115939168560","373301164512","630203995440","545488048512","229352929488","37192366944","0","0"],["-708588000","-16155806400","-148718449440","-712624117248","-1913340655008","-2884474680768","-2334854147040","-942206629248","-148769467776","0"],["157464000","4534963200","54589619520","356652180864","1375352301888","3192115246848","4364822718144","3322518113664","1289335387392","198359290368"]]},"step_quotients":[[{"coeff":{"coeffs":[["177147000","4038951600","27613674360","74843898912","54755429112","-97113402576","-178729985592","-99179645184","-18596183472","0","0","0"],["-265720500","-9778514400","-111889588140","-565882628328","-1328421810060","-1047585002256","996445497708","2116865551896","1190155742208","223154201664","0","0"],["-29524500","4286957400","102642514740","914401636128","4016335596804","8997453436536","8613993245868","-1002127664880","-7419877205328","-4611853501056","-892616806656","0"],["242757000","4944369600","26149259160","-132616495728","-2188605835368","-10818489167136","-26516282707224","-32467788429552","-15016073779872","3479552551872","5157341549568","1190155742208"],["-144342000","-4708173600","-64023287760","-463575275712","-1853946808848","-3460012529184","1330736767056","19982861844480","39567168448128","35175714158592","14777767132416","2380311484416"],["26244000","1070755200","19112980320","195831048384","1270067462496","5422636896768","15363814758048","28436089936320","33048861767424","22546839338496","8132730905088","1190155742208"]]},"deriv_order":0},{"coeff":{"coeffs":[["-177147000","-3153216600","-21767823360","-72611846712","-109281275712","-9298091736","185961834720","228319808184","108477736920","18596183472","0","0","0"],["354294000","8432197200","81374245920","406437573744","1089904711968","1329971492016","-260346568608","-2688181633008","-2956793172048","-1338925209984","-223154201664","0","0"],["-236196000","-7038640800","-87978286080","-596455366176","-2352353436288","-5246266509216","-5146321588992","2833507363104","12723921980064","12719789494848","5504470307712","892616806656","0"],["52488000","1879070400","28935584640","249850018368","1318019029632","4302308250432","8138649032064","6232093815744","-6605548035264","-19791849194496","-18182934950400","-7537653033984","-1190155742208"]]},"deriv_order":1},{"coeff":{"coeffs":[["49207500","1299078000","14455195200","88686874080","329616714312","767723920128","1122428901168","1009703887776","537739638732","154968195600","18596183472","0","0","0"],["-98415000","-3188646000","-44499326400","-350836090560","-1723475917584","-5490848412000","-11457544843872","-15488554589568","-13191925930776","-6762812055984","-1896810714144","-223154201664","0","0"],["65610000","2519424000","42420801600","411888032640","2552328307296","10554469278336","29601756877248","56155882435200","70748835645456","57276245093760","28315788700032","7736012324352","892616806656","0"],["-14580000","-647352000","-12786076800","-148091742720","-1116368111808","-5748542027136","-20650793899392","-51948094155264","-90596473390368","-107059835325888","-82660724280576","-39473498783232","-10513042389504","-1190155742208"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["-118098000","-3401222400","-40942214640","-267489135648","-1031514226416","-2394086435136","-3273617038608","-2491888585248","-967001540544","-148769467776","0","0","0"],["29524500","2090334600","45948388860","496765537632","3066514480908","11429420986152","25956311828580","34995951051696","26406580530240","10190708542656","1562079411648","0","0"],["82012500","2106081000","16575054300","-32198238720","-1419034626324","-10736974620792","-42111382714236","-96337643267952","-129125010554208","-96683624113536","-37068392387520","-5653239775488","0"],["-52488000","-1984046400","-31801429440","-276984214848","-1365148634688","-3224869018560","1808191864512","35310708675648","104518816083072","153199491927552","119015574220800","46416073946112","7140934453248"],["13122000","614109600","12768755760","155254465152","1222526876400","6521520835872","23949818069328","60309489242304","101832700692672","110420004971520","71706883468032","24993270586368","3570467226624"]]},"deriv_order":0},{"coeff":{"coeffs":[["-236196000","-7806277800","-111503407680","-903394430136","-4582339393680","-15160978608696","-33086054134368","-47174040609480","-42756758287344","-23468383541664","-7066549719360","-892616806656","0","0"],["249318000","9778514400","168700631040","1684665135648","10784612992032","46318884016032","135800810838144","271431271452384","363652500280176","316068999260544","168853345925760","49986541172736","6248317646592","0"],["-61236000","-2787112800","-56611457280","-676818693216","-5289649100928","-28386040948704","-106928514129024","-284156570927520","-528185332912608","-672071580658368","-564431360742144","-295158624067584","-86286291310080","-10711401679872"]]},"deriv_order":1},{"coeff":{"coeffs":[["-16402500","-629856000","-10605200400","-102972008160","-638082076824","-2638617319584","-7400439219312","-14038970608800","-17687208911364","-14319061273440","-7078947175008","-1934003081088","-223154201664","0","0"],["21870000","971028000","19179115200","222137614080","1674552167712","8622813040704","30976190849088","77922141232896","135894710085552","160589752988832","123991086420864","59210248174848","15769563584256","1785233613312","0"],["-7290000","-367416000","-8335094400","-112404101760","-1002459284064","-6223375348992","-27571023031104","-87926428775808","-201142519160976","-325319337834048","-362509868117952","-267718922233344","-123677017544448","-32134205039616","-3570467226624"]]},"deriv_order":2}]]},{"annihilator":{"terms":[{"coeff":{"coeffs":[["0","0"],["81","0"],["81","0"],["-18","-108"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-36","-54","0"],["-36","-36","108"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["-15","-54","-27","0"],["10","96","234","108"]]},"deriv_order":2,"shift":0}]},"quotient":[{"coeff":{"coeffs":[["-24300","-174960","-402408","-314928","-78732","0","0","0"],["20250","340200","1735020","3481704","2585034","629856","0","0"],["13500","113400","-48600","-2356128","-6184836","-4986360","-1259712","0"],["-13500","-259200","-1875960","-6356880","-10191420","-6823440","-1574640","0"],["1800","45360","457488","2348352","6444360","9062928","5668704","1259712"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","0","0","0","0","0"],["2025","38880","281394","953532","1528713","1023516","236196","0","0"],["675","4860","-61722","-807732","-3304557","-5773680","-4015332","-944784","0"],["-1800","-45360","-457488","-2348352","-6444360","-9062928","-5668704","-1259712","0"],["300","9360","121608","848880","3422412","7954848","10007712","5878656","1259712"]]},"deriv_order":1}],"step_multiplier":{"coeffs":[["-531441000","-5739562800","-23532207480","-45457337376","-42357973464","-18596183472","-3099363912","0","0","0"],["1062882000","17856417600","115939168560","373301164512","630203995440","545488048512","229352929488","37192366944","0","0"],["-708588000","-16155806400","-148718449440","-712624117248","-1913340655008","-2884474680768","-2334854147040","-942206629248","-148769467776","0"],["157464000","4534963200","54589619520","356652180864","1375352301888","3192115246848","4364822718144","3322518113664","1289335387392","198359290368"]]},"step_quotients":[[{"coeff":{"coeffs":[["-1417176000","-14242618800","-51273427680","-74155151376","-22039921152","35126124336","28927396512","6198727824","0","0","0"],["974308500","28591525800","225532931580","745683998976","1058432775948","383288003784","-378638957916","-340930030320","-74384733888","0","0"],["1564798500","14774059800","-42951061620","-873510439824","-3459521477700","-5492417225832","-2817493982892","929809173600","1264540476096","297538935552","0"],["-1351566000","-34988500800","-316923068880","-1206748038816","-1286316802512","3728419994880","11270128986576","9490481881056","1702583908992","-1157095860480","-396718580736"],["-157464000","3023308800","112070278080","1100431495296","5036224019904","11515858801920","11096181969984","-1493204658048","-9917964518400","-6149138001408","-1190155742208"],["314928000","8125142400","81969459840","385766644608","610791518592","-1867883317632","-10423046044800","-19543900081536","-17356437907200","-7339293743616","-1190155742208"],["-52488000","-1826582400","-27266466240","-228063299328","-1171755129024","-3814743019392","-7839171399744","-9837151474176","-7074814689792","-2644790538240","-396718580736"]]},"deriv_order":0},{"coeff":{"coeffs":[["708588000","8538485400","39879332640","88351003368","85175111952","4476858984","-49589822592","-32026760424","-6198727824","0","0","0"],["-1062882000","-21399357600","-163768858560","-620740094112","-1219083138720","-1081333631520","-24794911296","624005267616","390519852912","74384733888","0","0"],["236196000","10109188800","136729140480","875270572416","3004265733696","5572426731264","4837762692864","292028955264","-2467093673952","-1562079411648","-297538935552","0"],["262440000","4933872000","28469491200","-15532248960","-865837848960","-4061807814528","-8736379856640","-8904740365440","-2469389499072","2446431247872","1950533021952","396718580736"],["-104976000","-3128284800","-39101460480","-265091273856","-1045490416128","-2331674004096","-2287254039552","1259336605824","5655076435584","5653239775488","2446431247872","396718580736"]]},"deriv_order":1},{"coeff":{"coeffs":[["49207500","118098000","-4322386800","-37158354720","-133119593208","-252540763200","-267463626480","-158411933280","-49073261940","-6198727824","0","0","0"],["-196830000","-2834352000","-9636796800","49997969280","510030304992","1779723633024","3257316680256","3355577995392","1948466779344","595077871104","74384733888","0","0"],["262440000","6141096000","56309126400","241713538560","338965824384","-1179339854976","-6297295249152","-12573775017216","-13287317464512","-7777337176512","-2380311484416","-297538935552","0"],["-145800000","-4548960000","-60256224000","-440647257600","-1929589050240","-5070633053184","-7212632221440","-2577038188032","7991614187712","13433331942144","9212687041536","3041509118976","396718580736"],["29160000","1119744000","18853689600","183061347840","1134368136576","4690875234816","13156336389888","24958169971200","31443926953536","25456108930560","12584794977792","3438227699712","396718580736"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["-1358127000","-15022065600","-55461182760","-40023884592","237962273688","651555169056","657409523112","295472692944","49589822592","0","0","0"],["2450533500","45420490800","323849516580","1074433401576","1323026621028","-1447747320672","-6112117821348","-6633671892984","-3062171545056","-520693137216","0","0"],["-1236748500","-33591007800","-373556964780","-2171065448016","-6879582398268","-10570552808760","-1793594243124","17121345414912","22143922029936","10802316354624","1884413258496","0"],["19683000","3086294400","77493545640","863595876528","5223278497320","18124825065696","35115219166680","31947095292336","943584124320","-19216056254400","-12298276002816","-2380311484416"],["118098000","3637418400","44910307440","267744227328","583879346352","-1962624367584","-16694551525104","-48418951780800","-72616030215552","-57722553497088","-22910498037504","-3570467226624"],["-26244000","-1070755200","-19112980320","-195831048384","-1270067462496","-5422636896768","-15363814758048","-28436089936320","-33048861767424","-22546839338496","-8132730905088","-1190155742208"]]},"deriv_order":0},{"coeff":{"coeffs":[["-531441000","-8160571800","-34267315680","87126563304","1276070620032","4905145160136","9672770395584","10734474722328","6722520325128","2212945833168","297538935552","0","0"],["1115370000","26965710000","258823576800","1199767029840","2173160034144","-3729159760752","-27795248617824","-62069698361808","-71962408803888","-46027620335808","-15348050092224","-2082772548864","0"],["-691092000","-22134189600","-302494642560","-2297278197792","-10543199894784","-29479840060320","-46268120771712","-24527830307040","41831311181472","87672051352512","67954586891904","24894090941184","3570467226624"],["122472000","4839393600","84186552960","848518068672","5488189789824","23842943158464","70799369307264","143516926011456","195269109756480","172528502777856","93691704817152","28167019232256","3570467226624"]]},"deriv_order":1},{"coeff":{"coeffs":[["-16402500","-236196000","377913600","28258489440","244875258216","1062558883872","2696752713456","4153147642080","3859569004860","2099302489728","613674054576","74384733888","0","0"],["54675000","1509030000","16218792000","76244068800","21923712720","-1545464440224","-8276959740960","-21948700367232","-33973964499528","-31421351339856","-16980381752544","-4934187347904","-595077871104","0"],["-51030000","-1872072000","-29634724800","-263796289920","-1435960195488","-4805927251200","-8950962977856","-4207788279936","19847637744912","49783590232128","54344935580544","31737486458880","9620425582848","1190155742208"],["14580000","647352000","12786076800","148091742720","1116368111808","5748542027136","20650793899392","51948094155264","90596473390368","107059835325888","82660724280576","39473498783232","10513042389504","1190155742208"]]},"deriv_order":2}]]}],"restart_bases":[],"row_multiplier":{"coeffs":[["12150","87480","201204","157464","39366","0","0"],["-16200","-213840","-968112","-1819584","-1312200","-314928","0"],["5400","103680","750384","2542752","4076568","2729376","629856"]]},"start_base":1}},"shifted_parent_relation":{"terms":[{"coeff":{"coeffs":[["1"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-3","-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 = phi(n, D) = (1) D; 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":{"from_index":1,"justification":"the parent theorem (ThreeTermRecurrence) proves P_(m-1) strictly interlacing P_m for every m >= 1; T = phi(n, D) = (1) D is independent of n and maps every real-rooted polynomial to a real-rooted polynomial or zero, so by the Hermite--Kakeya--Obreschkoff theorem (both directions) T(P_(m-1)) and T(P_m) have weakly interlacing zeros; the nonzero gauge does not move zeros, so Q_(n-1) and Q_n interlace weakly (orientation not determined) for every n >= 1","kind":"weak","orientation":"unordered","status":"claimed"},"lean_declarations":["RealRooted.splits_add_C_mul_derivative_all","RealRooted.splits_C_mul_add_derivative","Polynomial.Splits.derivative"],"lift_summary":{"hypotheses":[{"evidence":"the polynomial with ascending coefficients [0, 1] is fixed; exact check: real-rooted = true, coefficients of one sign = true","name":"derivative_polynomial_real_rooted","statement":"the polynomial in D is real-rooted for every n >= n0","status":{"kind":"verified"}},{"evidence":"lambda(n) = 1","name":"gauge_finite_nonzero","statement":"lambda(n) is finite and nonzero for every n >= n0","status":{"kind":"verified"}},{"evidence":"delta(n) != 0 for every integer n in [0, +inf) (exact; Taylor shift: the coefficients of delta(n) at n = 0 + u have one sign)","name":"operator_coefficients_defined","sign_decision":{"certificate":{"condition":"nonzero","denominator":["1"],"method":{"kind":"taylor_shift","shifted_denominator":["1"],"shifted_numerator":["1"]},"numerator":["1"],"range":{"first":"0","last":null}},"decision":"holds"},"statement":"the operator coefficients are finite at every n >= n0 (their denominators do not vanish)","status":{"kind":"verified"}}],"identity":{"method":"forward_division","status":"certified"},"input_first_index":0,"input_interlacing":{"interlacing":{"from_index":1,"justification":{"premises":["the parent theorem (ThreeTermRecurrence) proves P_(m-1) strictly interlacing P_m for every m >= 1; T = phi(n, D) = (1) D is independent of n and maps every real-rooted polynomial to a real-rooted polynomial or zero, so by the Hermite--Kakeya--Obreschkoff theorem (both directions) T(P_(m-1)) and T(P_m) have weakly interlacing zeros; the nonzero gauge does not move zeros, so Q_(n-1) and Q_n interlace weakly (orientation not determined) for every n >= 1"],"theorem":"Hermite--Kakeya--Obreschkoff theorem (N. Obreschkoff, Verteilung und Berechnung der Nullstellen reeller Polynome, 1963; see S. Fisk, Polynomials, Roots, and Interlacing, arXiv:math/0612833): real polynomials f, g have weakly interlacing zeros iff alpha f + beta g is real-rooted or zero for all real alpha, beta; a linear T independent of n that maps every real-rooted polynomial to a real-rooted polynomial or zero therefore maps interlacing pairs to pairs with weakly interlacing zeros (orientation not determined)"},"kind":"weak","orientation":"unordered"},"status":"proved"},"lean_replay":"not_attempted","operation":{"description":"phi(n, D) = (1) D","kind":"preserver_image","operator":{"coefficients":[{"denominator":["1"],"numerator":["0"]},{"denominator":["1"],"numerator":["1"]}],"shape":"derivative_polynomial"}},"parent":{"gauge":{"kind":"none"},"index_shift":0,"recurrence":{"first_index":0,"initial_polynomials":[["1"],["3","6"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["-1"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["3","3"]]},"deriv_order":0,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"relation":"Q_n = lambda(n) T_n(P_(n+0)) with T = phi(n, D) = (1) D, for every n >= 0"},"parent_proof":{"route":"three_term_recurrence","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 (-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":"Laguerre's theorem on differential operators: if phi is a real polynomial with only real roots, then phi(D) maps every real-rooted polynomial to a real-rooted polynomial or zero (write phi(D) = C D^j prod (1 + c_i D); D preserves real-rootedness by Rolle's theorem and p + c p' is real-rooted for every real c by Rolle's theorem applied to e^(x/c) p; Polya--Schur 1914); when the coefficients of phi have one sign, coefficients of one sign stay of one sign; applied to phi(n, .) for each n"},"verdict":"proved"},"notes":["the division remainder is removed by row annihilators of the shifted parent"],"parent_interlacing_report":{"conclusion":{"first_index":0,"interlacing":"strict","interlacing_from":1,"root_region":{"upper":{"closed":false,"value":"0"}},"simple_roots":true,"statement":"every P_n, n >= 0, is nonzero and real-rooted, with simple roots from n = 0 on; P_(n-1) strictly interlaces P_n for n >= 1; every root lies in (-inf, 0)"},"hypotheses":[{"evidence":"f(n) a_n = 3 != 0 for every integer n in [2, +inf) (exact; Taylor shift: the coefficients of f(n) a_n = 3 at n = 2 + u have one sign)","name":"leading_coefficient_nonzero","sign_decision":{"certificate":{"condition":"nonzero","denominator":["1"],"method":{"kind":"taylor_shift","shifted_denominator":["1"],"shifted_numerator":["3"]},"numerator":["3"],"range":{"first":"2","last":null}},"decision":"holds"},"statement":"a_n != 0 for every n >= 2","status":{"kind":"verified"}},{"evidence":"Q_0 has degree 0, Q_1 degree 1; simple real roots and strict interlacing checked exactly","name":"seeds_interlace","statement":"Q_0 and Q_1 have simple real roots, degrees e and e + 1, and Q_0 strictly interlaces Q_1","status":{"kind":"verified"}},{"evidence":"beta_2 = 1/18 (exact)","name":"first_coefficient_positive","statement":"beta_2 = c_2 L_0 / (a_2 L_1) > 0","status":{"kind":"verified"}},{"evidence":"beta_n = 1/9 > 0 for every integer n in [3, +inf) (exact; Taylor shift: the coefficients of beta_n = 1/9 at n = 3 + u have one sign)","name":"recurrence_coefficient_positive","sign_decision":{"certificate":{"condition":"positive","denominator":["1"],"method":{"kind":"taylor_shift","shifted_denominator":["1"],"shifted_numerator":["1/9"]},"numerator":["1/9"],"range":{"first":"3","last":null}},"decision":"holds"},"statement":"beta_n = c_n / (a_n a_(n-1)) > 0 for every n >= 3","status":{"kind":"verified"}},{"evidence":"seeds checked exactly; positive-ratio induction at t = 0 with g(n) = 1/2 ((t - alpha_n)/2): g(n) > 0 for n >= 2, r_2 >= g(2) exactly, and (t - alpha_n) - beta_n/g(n-1) - g(n) >= 0 for every integer n in [3, +inf) (exact; Taylor shift: the coefficients of (t - alpha_n) - beta_n/g(n-1) - g(n) at n = 3 + u have one sign)","name":"root_upper_bound","sign_decision":{"certificate":{"condition":"nonnegative","denominator":["1"],"method":{"kind":"taylor_shift","shifted_denominator":["1"],"shifted_numerator":["5/18"]},"numerator":["5/18"],"range":{"first":"3","last":null}},"decision":"holds"},"statement":"every root of P_n is < 0 for every n >= 0 (region (-inf, 0) for P)","status":{"kind":"verified"}}],"lean_replay":"not_attempted","normal_form":"P_n = (a_n x + b_n) P_(n-1) - c_n P_(n-2) for n >= 2, with a_n = 3, b_n = 3, c_n = 1","recurrence":{"first_index":0,"initial_polynomials":[["1"],["3","6"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["-1"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["3","3"]]},"deriv_order":0,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"reference":"three-term recurrence Q_n = (a_n y + b_n) Q_(n-1) - c_n Q_(n-2) with a_n != 0 and beta_n = c_n / (a_n a_(n-1)) > 0: simple real roots and strict interlacing of consecutive rows (zero separation for orthogonal polynomials: G. Szeg\u0151, Orthogonal Polynomials, \u00a73.3; Favard, C. R. Acad. Sci. Paris 200 (1935)); root regions by a positive-ratio (chain-sequence) induction","requested_root_region":{"upper":{"closed":false,"value":"0"}},"schema":"polytool.recurrence-real-rootedness-theorem.v1","status":"proved","theorem":"three_term_recurrence"},"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":"P_n = (a_n x + b_n) P_(n-1) - c_n P_(n-2) for n >= 2, with a_n = 3, b_n = 3, c_n = 1: every P_n, n >= 0, is nonzero and real-rooted, with simple roots from n = 0 on; P_(n-1) strictly interlaces P_n for n >= 1; every root lies in (-inf, 0)","route":"three_term_recurrence","success":true,"variant":"three_term_recurrence"}],"conditional_on":[],"interlacing":{"from_index":1,"justification":{"premises":["every hypothesis of the theorem is verified exactly for every index: P_n = (a_n x + b_n) P_(n-1) - c_n P_(n-2) for n >= 2, with a_n = 3, b_n = 3, c_n = 1","every P_n, n >= 0, is nonzero and real-rooted, with simple roots from n = 0 on; P_(n-1) strictly interlaces P_n for n >= 1; every root lies in (-inf, 0)"],"theorem":"three_term_recurrence: three-term recurrence Q_n = (a_n y + b_n) Q_(n-1) - c_n Q_(n-2) with a_n != 0 and beta_n = c_n / (a_n a_(n-1)) > 0: simple real roots and strict interlacing of consecutive rows (zero separation for orthogonal polynomials: G. Szeg\u0151, Orthogonal Polynomials, \u00a73.3; Favard, C. R. Acad. Sci. Paris 200 (1935)); root regions by a positive-ratio (chain-sequence) induction"},"kind":"strict","orientation":"previous_interlaces_next"},"route":"three_term_recurrence","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 = phi(n, D) = (1) D 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 (-inf, 0]"},"kind":"preserver_image"}