{"certification":{"candidate":{"gauge":{"kind":"none"},"index_shift":0,"operator":{"schedule":{"first_degree":2,"first_index":0,"step":1},"shape":"reversal"},"parent":{"first_index":0,"initial_polynomials":[["13","22","8"],["34","88","68","16"]],"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 u(n,x) jointly generated with A207607; see the Formula section."},"identifying_rows":1,"identity":{"certificate":{"certificate":{"dividend_relation":{"terms":[{"coeff":{"coeffs":[["-244","-240"],["-184","-176"],["-36","-32"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-154","-276","-80"],["-40","-96","-32"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["-15","-36","-12"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["200"],["160"],["32"]]},"deriv_order":0,"shift":1}]},"exceptional_bases":[],"gauge":{"kind":"none"},"identifying_indices":[0],"index_shift":0,"input":{"first_index":0,"initial_polynomials":[["8","22","13"]],"recurrence":{"denominator":{"coeffs":[["72"],["96"],["32"]]},"terms":[{"coeff":{"coeffs":[["144","276","114","0"],["192","400","190","15"],["64","144","76","15"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","-48","-180","-114","0"],["0","-32","-120","-112","-30"]]},"deriv_order":1,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","0","0","12","36","15"]]},"deriv_order":2,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"input_valid_from_base":0,"multiplier":["1"],"operator":{"schedule":{"first_degree":2,"first_index":0,"step":1},"shape":"reversal"},"parent":{"first_index":0,"initial_polynomials":[["13","22","8"],["34","88","68","16"]],"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":[["-60","48","384"],["8","112","320"],["4","32","64"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["2","-28","-176","-128"]]},"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":[["1000","12400","24800","8000"],["1800","16320","30240","9600"],["960","7104","12288","3840"],["160","1024","1664","512"]]},"deriv_order":0}],"step_multiplier":{"coeffs":[["1728000","64281600","925655040","6524485632","23984750592","47969501184","52195885056","29620961280","8228044800","884736000"],["5184000","161740800","1930936320","11371954176","36528537600","66440134656","67820322816","37010276352","10032906240","1061683200"],["5184000","130636800","1271531520","6380384256","18212511744","30429167616","29289185280","15399714816","4076863488","424673280"],["1728000","33177600","266250240","1159667712","2981339136","4613013504","4205150208","2133983232","552075264","56623104"]]},"step_quotients":[[{"coeff":{"coeffs":[["1728000","81561600","1623767040","17838047232","118850568192","496600547328","1299402915840","2086603849728","1974705979392","1031035944960","272144793600","28311552000"],["6336000","269107200","4834990080","48194740224","293152997376","1125286281216","2735423815680","4139245633536","3747414933504","1899573018624","491748065280","50488934400"],["8928000","341337600","5558538240","50529779712","281661382656","998545637376","2267306459136","3246713339904","2819459579904","1389232521216","352894058496","35766927360"],["6048000","209433600","3107082240","25801777152","132164296704","434584092672","925678043136","1258636050432","1050710704128","503754522624","125618356224","12570329088"],["2016000","63475200","852986880","6452066304","30395142144","92954861568","186304315392","241133322240","193830322176","90493157376","22158508032","2189426688"],["288000","7833600","93219840","636751872","2753114112","7836401664","14801780736","18263900160","14151057408","6436159488","1547698176","150994944"]]},"deriv_order":0},{"coeff":{"coeffs":[["144000","3340800","-10529280","-1016838144","-12744142848","-76767805440","-262300188672","-538121797632","-672479281152","-505124093952","-219349647360","-50370969600","-4718592000"],["432000","7430400","-65802240","-2518843392","-25246052352","-130772606976","-400388161536","-758086041600","-894038999040","-644733665280","-272201416704","-61294510080","-5662310400"],["432000","4838400","-84464640","-1937405952","-15947366400","-72283152384","-200647065600","-353168031744","-394702848000","-273861181440","-112524263424","-24857542656","-2264924160"],["144000","748800","-29191680","-466504704","-3233949696","-13018042368","-33079468032","-54457417728","-57884147712","-38716047360","-15495856128","-3359637504","-301989888"]]},"deriv_order":1},{"coeff":{"coeffs":[["-360000","-17136000","-345081600","-3863093760","-26680190976","-119705112576","-358057304064","-720289677312","-969036742656","-855249223680","-479278596096","-162419834880","-30198988800","-2359296000"],["-1080000","-44928000","-791596800","-7814292480","-48254773248","-196729896960","-543334293504","-1024213745664","-1308448899072","-1109699592192","-603830550528","-200297152512","-36663459840","-2831155200"],["-1080000","-38448000","-586828800","-5112391680","-28388026368","-105868726272","-271566618624","-481884733440","-586456547328","-478929715200","-253331767296","-82301681664","-14835253248","-1132462080"],["-360000","-10656000","-140313600","-1083432960","-5444868096","-18691596288","-44764545024","-75071619072","-87282302976","-68762271744","-35394158592","-11267997696","-2000683008","-150994944"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["4032000","114278400","1409679360","11086184448","66239447040","305983586304","1020463939584","2297522552832","3318395830272","2914929082368","1449626959872","370692587520","37748736000"],["4896000","140083200","2114887680","21248630784","145856765952","678117998592","2115458039808","4369639145472","5829301960704","4807589363712","2287497904128","567665491968","56623104000"],["2304000","103564800","1930705920","20014995456","129200025600","547069501440","1551223701504","2942575607808","3658284859392","2857031958528","1308012576768","316107915264","30953963520"],["1728000","60825600","935331840","8295063552","47082774528","179167887360","464957964288","820068876288","961573552128","717867712512","318221844480","75195482112","7247757312"],["288000","8985600","124554240","1009631232","5300121600","18848858112","46147387392","77471023104","87206658048","63040389120","27292336128","6341787648","603979776"]]},"deriv_order":0},{"coeff":{"coeffs":[["-576000","-48499200","-1222318080","-15143215104","-110166147072","-511276105728","-1575941308416","-3277118767104","-4587734827008","-4249329205248","-2521261670400","-910216396800","-180816445440","-15099494400"],["-3312000","-145382400","-2552463360","-24765124608","-150602821632","-609590624256","-1689318457344","-3232352894976","-4241803935744","-3740357099520","-2140249522176","-752634298368","-146691588096","-12079595520"],["-2736000","-83923200","-1148705280","-9250735104","-48658913280","-175486611456","-443267997696","-787348242432","-973972242432","-820350812160","-453513314304","-155487043584","-29746003968","-2415919104"]]},"deriv_order":1},{"coeff":{"coeffs":[["-360000","-16416000","-323769600","-3660226560","-26503981056","-129916329984","-443417960448","-1065850306560","-1801767960576","-2114498396160","-1680876306432","-871873118208","-279284023296","-49828331520","-3774873600"],["-720000","-28512000","-493747200","-4973137920","-32558395392","-146280554496","-463361015808","-1045434138624","-1675996987392","-1883170603008","-1446033752064","-730419167232","-229361319936","-40315650048","-3019898880"],["-360000","-12096000","-182937600","-1644687360","-9778599936","-40471068672","-119530930176","-254129799168","-387568779264","-417891483648","-310443245568","-152844632064","-47072673792","-8153726976","-603979776"]]},"deriv_order":2}]]},{"annihilator":{"terms":[{"coeff":{"coeffs":[["48","-240"],["16","-296"],["-12","-120"],["-4","-16"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-32","72","80"],["-2","36","32"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["5","62","124","40"],["5","32","52","16"]]},"deriv_order":2,"shift":0}]},"quotient":[{"coeff":{"coeffs":[["640","9536","35712","44800","12800"],["800","8320","28800","35840","10240"],["160","1664","5760","7168","2048"]]},"deriv_order":0}],"step_multiplier":{"coeffs":[["1728000","64281600","925655040","6524485632","23984750592","47969501184","52195885056","29620961280","8228044800","884736000"],["5184000","161740800","1930936320","11371954176","36528537600","66440134656","67820322816","37010276352","10032906240","1061683200"],["5184000","130636800","1271531520","6380384256","18212511744","30429167616","29289185280","15399714816","4076863488","424673280"],["1728000","33177600","266250240","1159667712","2981339136","4613013504","4205150208","2133983232","552075264","56623104"]]},"step_quotients":[[{"coeff":{"coeffs":[["3456000","80179200","51425280","-12869369856","-134716096512","-575634014208","-1238754263040","-1402242859008","-812930826240","-228615782400","-24772608000"],["8928000","82713600","-3002434560","-59283652608","-424107417600","-1513522298880","-2935437557760","-3119732490240","-1743855353856","-479751045120","-51255705600"],["4320000","-221184000","-8035200000","-92308930560","-519039885312","-1609182609408","-2854647595008","-2865426333696","-1547557208064","-416802668544","-43918295040"],["-6336000","-426931200","-7895162880","-67986284544","-321420460032","-888904876032","-1459185057792","-1390499463168","-726994649088","-191827279872","-19940769792"],["-7488000","-267033600","-3644835840","-25908867072","-107247624192","-269732560896","-413644455936","-375909580800","-190607523840","-49309286400","-5058330624"],["-2592000","-70502400","-797506560","-4934504448","-18388021248","-42695589888","-61663887360","-53662777344","-26435911680","-6709837824","-679477248"],["-288000","-6681600","-66493440","-370778112","-1270001664","-2756395008","-3776200704","-3159097344","-1514668032","-377487360","-37748736"]]},"deriv_order":0},{"coeff":{"coeffs":[["-2448000","-83289600","-1014013440","-4777592832","-298487808","70422183936","253847420928","416776126464","365218725888","174003978240","42378854400","4128768000"],["-7488000","-208569600","-1961879040","-5735780352","17458274304","164002996224","472952586240","702598938624","582168084480","268121604096","63895633920","6134169600"],["-7776000","-167443200","-1100666880","-542951424","25432952832","133042176000","323143188480","439220994048","345312460800","153917521920","35906125824","3397386240"],["-2880000","-42336000","-122918400","1259873280","11985684480","45582888960","96200515584","120650121216","90256932864","38975569920","8903983104","830472192"],["-144000","-172800","29882880","346973184","1846056960","5633814528","10544209920","12280578048","8761835520","3668705280","821035008","75497472"]]},"deriv_order":1},{"coeff":{"coeffs":[["720000","33552000","650131200","6819448320","42486008832","163933655040","400740802560","624516710400","614142443520","371605929984","132919787520","25686835200","2064384000"],["2520000","103392000","1758355200","16233246720","90042550272","315380146176","714042925056","1049200754688","987792850944","579525083136","202844602368","38598082560","3067084800"],["3240000","115344000","1708646400","13906391040","69272008704","222240485376","469273264128","653219168256","590477672448","336418209792","115320029184","21615869952","1698693120"],["1800000","54720000","703872000","5084467200","22957701120","68019093504","134776995840","178476613632","155317911552","86063579136","28915531776","5341446144","415236096"],["360000","9216000","103449600","669634560","2766329856","7626276864","14259437568","18033868800","15146827776","8174960640","2694316032","490733568","37748736"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["-9792000","-250214400","-2498088960","-15205367808","-82885165056","-379493941248","-1146552975360","-2061229621248","-2102926639104","-1149019619328","-311851745280","-33030144000"],["-14688000","-324633600","-3663267840","-33400553472","-228104036352","-1002959142912","-2702417264640","-4383320702976","-4148347207680","-2159867068416","-568406310912","-58982400000"],["-6048000","-197913600","-3776394240","-41062090752","-260695240704","-1006521163776","-2412771065856","-3574661087232","-3170190753792","-1581791182848","-404902379520","-41240494080"],["-3168000","-161049600","-2842122240","-25818734592","-138934075392","-469745565696","-1016623890432","-1394913705984","-1170463850496","-562774671360","-140566855680","-14080278528"],["-2304000","-71308800","-946206720","-7088818176","-33148256256","-100791263232","-201106096128","-259397222400","-207981379584","-96929316864","-23706206208","-2340421632"],["-288000","-7833600","-93219840","-636751872","-2753114112","-7836401664","-14801780736","-18263900160","-14151057408","-6436159488","-1547698176","-150994944"]]},"deriv_order":0},{"coeff":{"coeffs":[["-1008000","23270400","1370396160","20434802688","150422999040","641077641216","1687690395648","2810222936064","2953404776448","1916741615616","737061765120","153141903360","13212057600"],["2880000","211104000","4474368000","45675048960","268114010112","980373676032","2314871341056","3563559714816","3540512931840","2209460060160","826862469120","168557543424","14344519680"],["6624000","247852800","3675640320","29686957056","147516327936","476928405504","1026753748992","1474760982528","1392193732608","837586649088","305458053120","61134077952","5133828096"],["2736000","72979200","856788480","5823581184","25364588544","74028257280","147154968576","198728368128","179058769920","104115732480","37050384384","7285506048","603979776"]]},"deriv_order":1},{"coeff":{"coeffs":[["720000","32112000","608947200","6467857920","42765115392","185281744896","539168735232","1061694259200","1405186375680","1225149087744","680555446272","229185552384","42420142080","3303014400"],["1800000","70560000","1182816000","11222553600","67180124160","267309047808","724378705920","1345470234624","1699419930624","1428986068992","772718395392","255164940288","46553628672","3586129920"],["1440000","49104000","727142400","6195824640","33832894464","124560322560","316331163648","556956352512","673738850304","547691986944","288725925888","93569679360","16835936256","1283457024"],["360000","10656000","140313600","1083432960","5444868096","18691596288","44764545024","75071619072","87282302976","68762271744","35394158592","11267997696","2000683008","150994944"]]},"deriv_order":2}]]}],"restart_bases":[],"row_multiplier":{"coeffs":[["120","1488","2976","960"],["120","768","1248","384"]]},"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 = x^(d_n) P(1/x), d_n = 2 + 1 (n - 0); so the candidate rows satisfy the input rule at every base n >= 0 (the exceptional bases checked exactly), and agreement on the 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":{"reason":"the schedule d_n depends on n","status":"none"},"interval_parent_proof":{"conclusion":{"first_index":0,"interlacing":"strict","interlacing_from":1,"root_region":{"lower":{"closed":false,"value":"-3"},"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 (-3, 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 2, Q_1 degree 3; 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/4 (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 (-3, 0) for P)","status":{"kind":"verified"}},{"evidence":"on the reflected rows (-1)^(deg) p_n(-y): seeds checked exactly; positive-ratio induction at t = 3 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_lower_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 > -3 for every n >= 0 (region (-3, 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":[["13","22","8"],["34","88","68","16"]],"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":{"lower":{"closed":false,"value":"-3"},"upper":{"closed":false,"value":"0"}},"schema":"polytool.recurrence-real-rootedness-theorem.v1","status":"proved","theorem":"three_term_recurrence"},"lean_declarations":["RealRooted.X_pow_mul_reverse_eq_zero_or_splits","RealRooted.reflect_eq_zero_or_splits"],"lean_route":"reversed","lift_summary":{"hypotheses":[{"evidence":"lambda(n) = 1","name":"gauge_finite_nonzero","statement":"lambda(n) is finite and nonzero for every n >= n0","status":{"kind":"verified"}}],"identity":{"method":"forward_division","status":"certified"},"input_first_index":0,"input_interlacing":{"reason":"the schedule d_n depends on n","status":"not_proved"},"lean_replay":"not_attempted","operation":{"description":"x^(d_n) P(1/x), d_n = 2 + 1 (n - 0)","kind":"preserver_image","operator":{"schedule":{"first_degree":2,"first_index":0,"step":1},"shape":"reversal"}},"parent":{"gauge":{"kind":"none"},"index_shift":0,"recurrence":{"first_index":0,"initial_polynomials":[["13","22","8"],["34","88","68","16"]],"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 = x^(d_n) P(1/x), d_n = 2 + 1 (n - 0), 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":"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":"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 2, Q_1 degree 3; 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/4 (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":[["13","22","8"],["34","88","68","16"]],"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 = x^(d_n) P(1/x), d_n = 2 + 1 (n - 0) 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"}