{"certification":{"candidate":{"gauge":{"kind":"none"},"index_shift":0,"operator":{"coefficients":[{"denominator":["1"],"numerator":["1"]},{"denominator":["1"],"numerator":["1"]}],"shape":"derivative_polynomial"},"parent":{"first_index":0,"initial_polynomials":[["1"],["3","4"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["-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":"basis_map_A013609 of Triangle of coefficients of polynomials v(n,x) jointly generated with A207606; see Formula section."},"identifying_rows":1,"identity":{"certificate":{"certificate":{"dividend_relation":{"terms":[{"coeff":{"coeffs":[["126","-96","-264","-96","0"],["434","660","520","304","64"],["96","-80","-128","0","0"],["-24","-112","-64","0","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["391","1020","1440","1184","464","64"],["474","676","360","240","64","0"],["76","-208","-336","-64","0","0"],["-24","-112","-64","0","0","0"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["265","1116","1704","1280","464","64"],["40","16","-160","-64","0","0"],["-20","-128","-208","-64","0","0"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["-18","24","24","0"],["-140","-160","-144","-64"],["-72","0","0","0"],["16","64","0","0"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["-18","24","24","0"],["-140","-160","-144","-64"],["-72","0","0","0"],["16","64","0","0"]]},"deriv_order":1,"shift":1}]},"exceptional_bases":[],"gauge":{"kind":"none"},"identifying_indices":[0],"index_shift":0,"input":{"first_index":0,"initial_polynomials":[["1"]],"recurrence":{"denominator":{"coeffs":[["34","120","168","64"],["52","32","-144","-64"],["-120","-192","0","0"],["16","64","0","0"]]},"terms":[{"coeff":{"coeffs":[["188","724","848","400","64"],["-170","-484","-584","-304","-64"],["-168","-256","-64","0","0"],["24","112","64","0","0"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["-205","-972","-1656","-1280","-464","-64"],["-80","-272","-256","-64","0","0"],["20","128","208","64","0","0"]]},"deriv_order":1,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"input_valid_from_base":0,"multiplier":["1"],"operator":{"coefficients":[{"denominator":["1"],"numerator":["1"]},{"denominator":["1"],"numerator":["1"]}],"shape":"derivative_polynomial"},"parent":{"first_index":0,"initial_polynomials":[["1"],["3","4"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["-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":[["-72","-96","0"],["-12","-48","0"],["4","32","64"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["12","56","16","-64"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["-5","-52","-180","-224","-64"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["24"]]},"deriv_order":0,"shift":1}]},"quotient":[{"coeff":{"coeffs":[["-97200","-336960","36288","1202688","1389312","580608","82944","0","0","0"],["-626400","-3525120","-8740224","-15137280","-19450368","-14266368","-5031936","-663552","0","0"],["576000","7660800","33212160","70502400","90961920","81506304","46854144","14450688","1769472","0"],["268800","637440","-9948672","-55044096","-117313536","-135782400","-101965824","-49840128","-13762560","-1572864"],["-288000","-3686400","-17786880","-40181760","-42946560","-19169280","-2949120","0","0","0"],["38400","645120","4337664","14843904","27156480","25460736","10616832","1572864","0","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["-97200","-336960","36288","1202688","1389312","580608","82944","0","0","0"],["-626400","-3525120","-8740224","-15137280","-19450368","-14266368","-5031936","-663552","0","0"],["576000","7660800","33212160","70502400","90961920","81506304","46854144","14450688","1769472","0"],["268800","637440","-9948672","-55044096","-117313536","-135782400","-101965824","-49840128","-13762560","-1572864"],["-288000","-3686400","-17786880","-40181760","-42946560","-19169280","-2949120","0","0","0"],["38400","645120","4337664","14843904","27156480","25460736","10616832","1572864","0","0"]]},"deriv_order":1}],"step_multiplier":{"coeffs":[["-46656000","-335923200","-918190080","-1182449664","-734552064","-214990848","-23887872","0","0","0"],["93312000","1045094400","4523765760","9710419968","10928701440","6306398208","1767702528","191102976","0","0"],["-62208000","-945561600","-5802762240","-18536988672","-33180254208","-33347469312","-17995530240","-4841275392","-509607936","0"],["13824000","265420800","2130001920","9277341696","23850713088","36904108032","33641201664","17071865856","4416602112","452984832"]]},"step_quotients":[[{"coeff":{"coeffs":[["15552000","236390400","1077442560","1946861568","949542912","-1122729984","-1377533952","-509607936","-63700992","0","0","0"],["-23328000","-572313600","-4365757440","-14719905792","-23036866560","-12111151104","7679950848","10876944384","4076863488","509607936","0","0"],["-2592000","250905600","4004951040","23785684992","69649403904","104019738624","66391031808","-5149163520","-25416695808","-10531897344","-1358954496","0"],["21312000","289382400","1020303360","-3449659392","-37953773568","-125072769024","-204370182144","-166826999808","-51437371392","7946108928","7851737088","1207959552"],["-12672000","-275558400","-2498088960","-12058656768","-32150274048","-40001273856","10256449536","102676561920","135536836608","80329310208","22498246656","2415919104"],["2304000","62668800","745758720","5094014976","22024912896","62691213312","118414245888","146111201280","113208459264","51489275904","12381585408","1207959552"]]},"deriv_order":0},{"coeff":{"coeffs":[["-23328000","-276825600","-1274019840","-2833201152","-2842656768","-161243136","2149908480","1759739904","557383680","63700992","0","0","0"],["46656000","740275200","4762644480","15858561024","28350922752","23063740416","-3009871872","-20718747648","-15192686592","-4586471424","-509607936","0","0"],["-31104000","-617932800","-5149163520","-23272759296","-61190111232","-90978287616","-59496726528","21838823424","65378451456","43571478528","12570329088","1358954496","0"],["6912000","164966400","1693532160","9748758528","34284699648","74608607232","94091083776","48032907264","-33940832256","-67796729856","-41523609600","-11475615744","-1207959552"]]},"deriv_order":1},{"coeff":{"coeffs":[["9720000","171072000","1269043200","5190635520","12861130752","19970260992","19464634368","11673206784","4144545792","796262400","63700992","0","0","0"],["-19440000","-419904000","-3906662400","-20533616640","-67247345664","-142829568000","-198691356672","-179063488512","-101674745856","-34748891136","-6497501184","-509607936","0","0"],["12960000","331776000","3724185600","24106844160","99587874816","274545967104","513339752448","649219276800","545285799936","294298583040","96995377152","17666408448","1358954496","0"],["-2880000","-85248000","-1122508800","-8667463680","-43558944768","-149532770304","-358116360192","-600572952576","-698258423808","-550098173952","-283153268736","-90143981568","-16005464064","-1207959552"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["-10368000","-199065600","-1597501440","-6958006272","-17888034816","-27678081024","-25230901248","-12803899392","-3312451584","-339738624","0","0","0"],["2592000","122342400","1792834560","12922011648","53178052608","132135763968","200054292480","179817283584","90455408640","23272095744","2378170368","0","0"],["7200000","123264000","646732800","-837550080","-24608231424","-124130377728","-324567023616","-495005073408","-442316095488","-220792356864","-56434360320","-5737807872","0"],["-4608000","-116121600","-1240842240","-7204995072","-23673765888","-37282775040","13936361472","181434580992","358027886592","349855285248","181193932800","47110422528","4831838208"],["1152000","35942400","498216960","4038524928","21200486400","75395432448","184589549568","309884092416","348826632192","252161556480","109169344512","25367150592","2415919104"]]},"deriv_order":0},{"coeff":{"coeffs":[["-31104000","-685324800","-6526033920","-35249043456","-119197163520","-262914564096","-382508531712","-363586682880","-219694104576","-80390651904","-16137584640","-1358954496","0","0"],["32832000","858470400","9873653760","65733009408","280532533248","803240312832","1569995882496","2092014895104","1868530581504","1082690371584","385603338240","76101451776","6341787648","0"],["-8064000","-244684800","-3313336320","-26408411136","-137595912192","-492257378304","-1236202684416","-2190093189120","-2713938296832","-2302172725248","-1288968339456","-449360953344","-87577067520","-7247757312"]]},"deriv_order":1},{"coeff":{"coeffs":[["-3240000","-82944000","-931046400","-6026711040","-24896968704","-68636491776","-128334938112","-162304819200","-136321449984","-73574645760","-24248844288","-4416602112","-339738624","0","0"],["4320000","127872000","1683763200","13001195520","65338417152","224299155456","537174540288","900859428864","1047387635712","825147260928","424729903104","135215972352","24008196096","1811939328","0"],["-1440000","-48384000","-731750400","-6578749440","-39114399744","-161884274688","-478123720704","-1016519196672","-1550275117056","-1671565934592","-1241772982272","-611378528256","-188290695168","-32614907904","-2415919104"]]},"deriv_order":2}]]},{"annihilator":{"terms":[{"coeff":{"coeffs":[["0","0"],["36","0"],["36","0"],["-8","-32"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-24","-24","0"],["-24","-16","32"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["-15","-36","-12","0"],["10","64","104","32"]]},"deriv_order":2,"shift":0}]},"quotient":[{"coeff":{"coeffs":[["-2127600","-13798080","-36542016","-54604800","-54459648","-37518336","-16727040","-4202496","-442368","0","0"],["2332800","27440640","119386368","267715584","365654016","341434368","222547968","94814208","23003136","2359296","0"],["211200","-3075840","-45973248","-203440128","-449083392","-593694720","-529428480","-328531968","-134086656","-31457280","-3145728"],["-691200","-9308160","-48586752","-124895232","-167362560","-114720768","-37748736","-4718592","0","0","0"],["96000","1689600","12134400","45785088","97579008","117964800","77463552","25165824","3145728","0","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["32400","371520","1404864","1299456","-3863808","-10312704","-8985600","-3317760","-442368","0","0"],["230400","3179520","17581824","51766272","94353408","120176640","109965312","63553536","19464192","2359296","0"],["-38400","-1355520","-14371584","-71528448","-194512896","-314019840","-324317184","-228851712","-106561536","-28311552","-3145728"],["-115200","-1935360","-13012992","-44531712","-81469440","-76382208","-31850496","-4718592","0","0","0"],["19200","399360","3459072","16097280","43266048","67043328","56229888","22020096","3145728","0","0"]]},"deriv_order":1}],"step_multiplier":{"coeffs":[["-46656000","-335923200","-918190080","-1182449664","-734552064","-214990848","-23887872","0","0","0"],["93312000","1045094400","4523765760","9710419968","10928701440","6306398208","1767702528","191102976","0","0"],["-62208000","-945561600","-5802762240","-18536988672","-33180254208","-33347469312","-17995530240","-4841275392","-509607936","0"],["13824000","265420800","2130001920","9277341696","23850713088","36904108032","33641201664","17071865856","4416602112","452984832"]]},"step_quotients":[[{"coeff":{"coeffs":[["-124416000","-833587200","-2000609280","-1928945664","-382205952","406093824","222953472","31850496","0","0","0"],["85536000","1673395200","8799943680","19396952064","18354843648","4431200256","-2918301696","-1751777280","-254803968","0","0"],["137376000","864691200","-1675883520","-22722011136","-59993395200","-63497945088","-21715402752","4777574400","4331667456","679477248","0"],["-118656000","-2047795200","-12365844480","-31390285824","-22306701312","43104337920","86862790656","48764289024","5832179712","-2642411520","-603979776"],["-13824000","176947200","4372807680","28624748544","87335829504","133135073280","85522120704","-7672430592","-33973862400","-14042529792","-1811939328"],["27648000","475545600","3198320640","10034675712","10592059392","-21594636288","-80334028800","-100421074944","-59454259200","-16760438784","-1811939328"],["-4608000","-106905600","-1063895040","-5932449792","-20320026624","-44102320128","-60419211264","-50545557504","-24234688512","-6039797760","-603979776"]]},"deriv_order":0},{"coeff":{"coeffs":[["93312000","749606400","2334044160","3447318528","2215600128","77635584","-573308928","-246841344","-31850496","0","0","0"],["-139968000","-1878681600","-9585008640","-24220311552","-31711150080","-18751979520","-286654464","4809424896","2006581248","254803968","0","0"],["31104000","887500800","8002437120","34151694336","78147846144","96634404864","55929470976","2250768384","-12676497408","-5350883328","-679477248","0"],["34560000","433152000","1666252800","-606044160","-22522429440","-70437961728","-101001461760","-68631920640","-12688293888","8380219392","4454350848","603979776"],["-13824000","-274636800","-2288517120","-10343448576","-27195604992","-40434794496","-26442989568","9706143744","29057089536","19365101568","5586812928","603979776"]]},"deriv_order":1},{"coeff":{"coeffs":[["9720000","15552000","-379468800","-2174791680","-5194119168","-6569164800","-4638228480","-1831403520","-378224640","-31850496","0","0","0"],["-38880000","-373248000","-846028800","2926264320","19900588032","46294695936","56486854656","38793904128","15017508864","3057647616","254803968","0","0"],["51840000","808704000","4943462400","14146928640","13225918464","-30677336064","-109204733952","-145365663744","-102409961472","-39961755648","-8153726976","-679477248","0"],["-28800000","-599040000","-5289984000","-25790054400","-75289559040","-131898802176","-125078077440","-29793189888","61594140672","69023563776","31557943296","6945767424","603979776"],["5760000","147456000","1655193600","10714152960","44261277696","122020429824","228151001088","288541900800","242349244416","130799370240","43109056512","7851737088","603979776"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["-119232000","-879206400","-2164008960","-1041113088","4126629888","7532642304","5066883072","1518206976","169869312","0","0","0"],["215136000","2658355200","12636103680","27948478464","22943305728","-16737435648","-47108210688","-34085339136","-10489430016","-1189085184","0","0"],["-108576000","-1966003200","-14575610880","-56474394624","-119302483968","-122206371840","-13823852544","87973429248","75853725696","24668798976","2868903936","0"],["1728000","180633600","3023677440","22464110592","90579640320","209541464064","270645166080","164151558144","3232235520","-43882905600","-18723373056","-2415919104"],["10368000","212889600","1752330240","6964641792","10125361152","-22689939456","-128670695424","-248787763200","-248745295872","-131818586112","-34879832064","-3623878656"],["-2304000","-62668800","-745758720","-5094014976","-22024912896","-62691213312","-118414245888","-146111201280","-113208459264","-51489275904","-12381585408","-1207959552"]]},"deriv_order":0},{"coeff":{"coeffs":[["-69984000","-716428800","-2005585920","3399542784","33193525248","85062721536","111827091456","82734317568","34541862912","7580418048","679477248","0","0"],["146880000","2367360000","15148339200","46813040640","56528879616","-64669335552","-321341423616","-478392680448","-369759485952","-157667033088","-35049701376","-3170893824","0"],["-91008000","-1943193600","-17704304640","-89636216832","-274252824576","-511225528320","-534906667008","-189044490240","214938943488","300319506432","155185053696","37899730944","3623878656"],["16128000","424857600","4927242240","33107853312","142760411136","413473112064","818512920576","1106134695936","1003337809920","590994210816","213959835648","42882564096","3623878656"]]},"deriv_order":1},{"coeff":{"coeffs":[["-3240000","-31104000","33177600","1653903360","9554651136","27639595008","46765817856","48014622720","29747036160","10786701312","2102132736","169869312","0","0"],["10800000","198720000","1423872000","4462387200","855429120","-40201076736","-143535144960","-253749362688","-261849120768","-161450164224","-58166083584","-11267997696","-905969664","0"],["-10080000","-246528000","-2601676800","-15439380480","-56028930048","-125013196800","-155223392256","-48646324224","152972623872","255799590912","186157891584","72477573120","14646509568","1207959552"],["2880000","85248000","1122508800","8667463680","43558944768","149532770304","358116360192","600572952576","698258423808","550098173952","283153268736","90143981568","16005464064","1207959552"]]},"deriv_order":2}]]}],"restart_bases":[],"row_multiplier":{"coeffs":[["129600","622080","953856","497664","82944","0","0"],["-172800","-1520640","-4589568","-5750784","-2764800","-442368","0"],["57600","737280","3557376","8036352","8589312","3833856","589824"]]},"start_base":0}},"shifted_parent_relation":{"terms":[{"coeff":{"coeffs":[["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 = phi(n, D) = 1 + (1) D; 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":{"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 + (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 [1, 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 + (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 + (1) D","kind":"preserver_image","operator":{"coefficients":[{"denominator":["1"],"numerator":["1"]},{"denominator":["1"],"numerator":["1"]}],"shape":"derivative_polynomial"}},"parent":{"gauge":{"kind":"none"},"index_shift":0,"recurrence":{"first_index":0,"initial_polynomials":[["1"],["3","4"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["-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 = phi(n, D) = 1 + (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 = 2 != 0 for every integer n in [2, +inf) (exact; Taylor shift: the coefficients of f(n) a_n = 2 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":["2"]},"numerator":["2"],"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/8 (exact)","name":"first_coefficient_positive","statement":"beta_2 = c_2 L_0 / (a_2 L_1) > 0","status":{"kind":"verified"}},{"evidence":"beta_n = 1/4 > 0 for every integer n in [3, +inf) (exact; Taylor shift: the coefficients of beta_n = 1/4 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/4"]},"numerator":["1/4"],"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) = 3/4 ((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/12"]},"numerator":["5/12"],"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 = 2, b_n = 3, c_n = 1","recurrence":{"first_index":0,"initial_polynomials":[["1"],["3","4"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["-1"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["3","2"]]},"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 = 2, 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 = 2, 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 + (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"}