{"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":[["13","33","18"],["34","132","153","54"]],"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 u(n,x) jointly generated with A207607; see the Formula section."},"identifying_rows":1,"identity":{"certificate":{"certificate":{"dividend_relation":{"terms":[{"coeff":{"coeffs":[["96","-504","-648"],["-12","-378","-378"],["-9","-63","-54"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","-90","-324","-162"],["-5","-48","-117","-54"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["-24","180"],["0","162"],["6","36"]]},"deriv_order":1,"shift":1}]},"exceptional_bases":[],"gauge":{"kind":"none"},"identifying_indices":[0],"index_shift":0,"input":{"first_index":0,"initial_polynomials":[["33","36"]],"recurrence":{"denominator":{"coeffs":[["-18","54"],["-12","90"],["6","36"]]},"terms":[{"coeff":{"coeffs":[["-99","189","324"],["-6","252","270"],["9","63","54"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["-5","42","207","108"],["5","48","117","54"]]},"deriv_order":1,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"input_valid_from_base":0,"multiplier":["1"],"operator":{"coefficients":[{"denominator":["1"],"numerator":["0"]},{"denominator":["1"],"numerator":["1"]}],"shape":"derivative_polynomial"},"parent":{"first_index":0,"initial_polynomials":[["13","33","18"],["34","132","153","54"]],"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":[["-135","162","1944"],["18","378","1620"],["9","108","324"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["3","-63","-594","-648"]]},"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":[["-600","-17820","-107136","781164","7113096","16723260","13122000","3280500"],["-1200","-20790","95148","2962494","15585048","31088934","22963500","5576850"],["-450","7560","333558","3161916","12371130","21555072","15024690","3542940"],["300","14310","205848","1329372","4252500","6606198","4356504","997272"],["150","3780","38124","195696","537030","755244","472392","104976"]]},"deriv_order":1}],"step_multiplier":{"coeffs":[["19683000","1098311400","23723526240","250823145888","1383081579792","4149244739376","6772224938976","5764816876320","2402007031800","387420489000"],["59049000","2763493200","49487785920","437176121184","2106419547600","5746909440384","8799438519936","7202921731488","2928898896840","464904586800"],["59049000","2232052200","32587962120","245283404904","1050225201144","2632048708824","3800164529880","2997084902904","1190155742208","185961834720"],["19683000","566870400","6823702440","44581522608","171919037736","399014405856","545602839768","415314764208","161166923424","24794911296"]]},"step_quotients":[[{"coeff":{"coeffs":[["19683000","1393556400","41615373240","685754460288","6853522657392","42954734940192","168592769774640","406093812196032","576474455782872","451484341061040","178755813624600","27894275208000"],["72171000","4597948800","123915507480","1852767718416","16904679044976","97334516044224","354911222663280","805577943871584","1093980069402264","831811419187776","323000210089080","49744790787600"],["101695500","5832072900","142459255440","1942534480608","16242014633256","86371759777464","294174709948656","631873749049776","823082749477164","608336433358884","231795228250656","35239767679440"],["68890500","3578369400","79631119440","991906991568","7621259332104","37590463019808","120103336162656","244955127421008","306733198596948","220591027708776","82511266065264","12385058192352"],["22963500","1084533300","21861120780","248039103636","1752737059044","8040368585052","24172302655332","46929248256060","56584742567616","39626400736224","14554612930752","2157157282752"],["3280500","133844400","2389122540","24478881048","158758432812","677829612096","1920476844756","3554511242040","4131107720928","2818354917312","1016591363136","148769467776"]]},"deriv_order":0},{"coeff":{"coeffs":[["1093500","38053800","-179902620","-26060449464","-489927663432","-4426818499440","-22688325938808","-69819332581872","-130877586055188","-147460503083832","-96051870436140","-33085709760600","-4649045868000"],["3280500","84636900","-1124292960","-64555201152","-970543063368","-7541007489576","-34632598462704","-98358887703600","-173997429085260","-188216621965980","-119195337327696","-40260737216880","-5578855041600"],["3280500","55112400","-1443157560","-49653595512","-613070337600","-4168210805784","-17355481313400","-45822258778824","-76816873624500","-79948092110040","-49273687472976","-16327449088416","-2231542016640"],["1093500","8529300","-498767220","-11956005324","-124323890364","-750685921668","-2861293224348","-7065650521188","-11265384281328","-11302347065760","-6785540724672","-2206747105344","-297538935552"]]},"deriv_order":1},{"coeff":{"coeffs":[["-1822500","-130126500","-3930695100","-66004578540","-683784113256","-4601866661784","-20647388425464","-62303298567768","-125728968641076","-166448182134420","-139915446013836","-71122653370620","-19835929036800","-2324522934000"],["-5467500","-341172000","-9016782300","-133514512920","-1236717059688","-7562958128640","-31331393258904","-88591988478096","-169766452971612","-215969187368448","-176275805934348","-87708899345688","-24082057596240","-2789427520800"],["-5467500","-291964500","-6684346800","-87350004720","-727554066408","-4069949490648","-15659899671024","-41681852966160","-76090589347788","-93209064981300","-73954955425536","-36039403568736","-9744400139328","-1115771008320"],["-1822500","-80919000","-1598259600","-18511467840","-139546013976","-718567753392","-2581349237424","-6493511769408","-11324559173796","-13382479415736","-10332590535072","-4934187347904","-1314130298688","-148769467776"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["45927000","1952553600","36128540160","426190172832","3819700301040","26466833185056","132401459110464","447142706176608","968736839960952","1276429636062432","952174183588992","365229043390080","55788550416000"],["55768500","2393452800","54202258080","816868749456","8410836106152","58655551316688","274472933626368","850417015542768","1701743809184964","2105214009829488","1502522034715008","559298814103872","83682825624000"],["26244000","1769501700","49481881020","769443663204","7450324523100","47320176255660","201265594519284","572682613619052","1067960392800372","1251076839262272","859156073862048","311448880789056","45746611341120"],["19683000","1039262400","23971532040","318890109168","2715030032328","15497584835040","60326593139448","159601400274672","280711455752448","314349885410688","209021102225280","74087194952448","10711401679872"],["3280500","153527400","3192188940","38813616288","305631719100","1630380208968","5987454517332","15077372310576","25458175173168","27605001242880","17926720867008","6248317646592","892616806656"]]},"deriv_order":0},{"coeff":{"coeffs":[["-4374000","-552436200","-20884450320","-388104040224","-4235156782848","-29482756608528","-136315075665024","-425194158864384","-892862689526352","-1240503531463368","-1104045081519600","-597867298624800","-178151437661760","-22315420166400"],["-25150500","-1655996400","-43611229440","-634703056848","-5789678394888","-35152067159856","-146121922247616","-419385950893296","-825537790069236","-1091919681148320","-937202189651424","-494360941419648","-144529537944384","-17852336133120"],["-20776500","-955937700","-19626706620","-237086222724","-1870612090020","-10119442304556","-38341599603444","-102155551100172","-189553997494008","-239484405742560","-198590709540096","-102130239628224","-29307585151872","-3570467226624"]]},"deriv_order":1},{"coeff":{"coeffs":[["-1822500","-124659000","-3687938100","-62538402240","-679268045736","-4994420162256","-25569714010248","-92193449343840","-233772794613396","-411522635066040","-490696976715012","-381787911650592","-183445151223456","-49093924366080","-5578855041600"],["-3645000","-216513000","-5624089200","-84970723680","-834436063152","-5623515926064","-26719731076608","-90427500661536","-217454471429832","-366501734045352","-422139563542224","-319846090747968","-150653881034496","-39721447896192","-4463084033280"],["-1822500","-91854000","-2083773600","-28101025440","-250614821016","-1555843837248","-6892755757776","-21981607193952","-50285629790244","-81329834458512","-90627467029488","-66929730558336","-30919254386112","-8033551259904","-892616806656"]]},"deriv_order":2}]]},{"annihilator":{"terms":[{"coeff":{"coeffs":[["108","-810"],["36","-999"],["-27","-405"],["-9","-54"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-48","162","270"],["-3","81","108"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["5","93","279","135"],["5","48","117","54"]]},"deriv_order":2,"shift":0}]},"quotient":[{"coeff":{"coeffs":[["-3600","-98820","-705996","301320","14527512","38429964","31099140","7873200"],["-4950","-80190","34668","5506380","29394738","57837402","42357816","10235160"],["-450","29160","663228","5040792","17459550","28308528","19053144","4408992"],["900","22680","228744","1174176","3222180","4531464","2834352","629856"]]},"deriv_order":0},{"coeff":{"coeffs":[["-600","-16020","-102276","388152","6807888","28083996","48612636","33592320","7873200"],["-600","-6570","99414","2090124","14071644","44753310","68676174","44929728","10235160"],["150","10080","196884","1796904","8756262","23310504","32192640","19945440","4408992"],["150","4680","60804","424440","1711206","3977424","5003856","2939328","629856"]]},"deriv_order":1}],"step_multiplier":{"coeffs":[["19683000","1098311400","23723526240","250823145888","1383081579792","4149244739376","6772224938976","5764816876320","2402007031800","387420489000"],["59049000","2763493200","49487785920","437176121184","2106419547600","5746909440384","8799438519936","7202921731488","2928898896840","464904586800"],["59049000","2232052200","32587962120","245283404904","1050225201144","2632048708824","3800164529880","2997084902904","1190155742208","185961834720"],["19683000","566870400","6823702440","44581522608","171919037736","399014405856","545602839768","415314764208","161166923424","24794911296"]]},"step_quotients":[[{"coeff":{"coeffs":[["39366000","1369936800","1317973680","-494741810304","-7768408967712","-49790936872512","-160723829175840","-272903813684352","-237318294741840","-100109454357600","-16271660538000"],["101695500","1413239400","-76949113860","-2279062762272","-24456170802600","-130915983730320","-380862273225960","-607160798710560","-509082403440996","-210080051561880","-33666840494100"],["49207500","-3779136000","-205933387500","-3548665391040","-29930455261512","-139190367045312","-370380071420568","-557667859938624","-451777230950724","-182515342049856","-28847329610940"],["-72171000","-7294519800","-202344389280","-2613621169296","-18534723383232","-76888101598848","-189323917553232","-270618319777392","-212231010116808","-83999993864328","-13097911892112"],["-85293000","-4562519400","-93413156040","-996023887848","-6184438438392","-23331207990744","-53668853346456","-73159337230200","-55643913433440","-21592235253600","-3322518113664"],["-29524500","-1204599600","-20439220860","-189698927832","-1060345963548","-3693064288032","-8000663565060","-10443823262136","-7717416140880","-2938196988576","-446308403328"],["-3280500","-114161400","-1704154140","-14253956208","-73234695564","-238421438712","-489948212484","-614821967136","-442175918112","-165299408640","-24794911296"]]},"deriv_order":0},{"coeff":{"coeffs":[["-18589500","-948720600","-17325370260","-122444478792","-11474874072","4060897987536","21957182165592","54075176128944","71078688319572","50796852648840","18557441423100","2711943423000"],["-56862000","-2375738100","-33520542660","-147001776912","671154713136","9457239183624","40909244040360","91159639292304","113301265497120","78272541541836","27979507715580","4029173085600"],["-59049000","-1907282700","-18805925520","-13915251144","977728145688","7671882276000","27951096879720","56987315502408","67204540825200","44933028314220","15723073125576","2231542016640"],["-21870000","-482233500","-2100176100","32289174180","460769975820","2628539072460","8321109733476","15653911393836","17565759762516","11378109294720","3898999801296","545488048512"],["-1093500","-1968300","510577020","8892543204","70968631140","324874134828","912048415380","1593360028908","1705224107880","1071002418480","359526213792","49589822592"]]},"deriv_order":1},{"coeff":{"coeffs":[["3645000","254785500","7405400700","116516667780","1088869937292","6302160414360","23108734033560","54019170750600","79682732989920","72321762830796","38803175243820","11248108197300","1355971711500"],["12757500","785133000","20028764700","277360238880","2307692079432","12124272299184","41175313165656","90753303755232","128162505004524","112786885878984","59216274715788","16901864533440","2014586542800"],["16402500","875893500","19462550400","237603728160","1775365816824","8543670846984","27060661106928","56501863280784","76612315606308","65473546080348","33665290812144","9465457387248","1115771008320"],["9112500","415530000","8017542000","86872888800","588380769720","2614882455936","7771920729840","15437791345248","20151930232692","16749651327984","8441289801216","2338986632256","272744024256"],["1822500","69984000","1178355600","11441334240","70898008536","293179702176","822271024368","1559885623200","1965245434596","1591006808160","786549686112","214889231232","24794911296"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["-111537000","-4275147600","-64023287760","-584545419072","-4779576280656","-32825299419072","-148761049750560","-401155492362912","-613905818121864","-503148671231472","-204836960944080","-32543321076000"],["-167305500","-5546669400","-93885548040","-1284029480448","-13153628166552","-86753517231168","-350628743539440","-853079713516944","-1211023931614380","-945792593294184","-373352476203432","-58113073350000"],["-68890500","-3381539400","-96784853940","-1578564711468","-15033001238604","-87061623339564","-313048209963276","-695698777902708","-925471441618272","-692656694827452","-265956417288720","-40632660886320"],["-36085500","-2751683400","-72840484440","-992558892528","-8011638884592","-40631844592944","-131903226795672","-271477417537296","-341692646029236","-246435590249640","-92330050938480","-13872752870112"],["-26244000","-1218377700","-24250243320","-272517984684","-1911495491856","-8718198197148","-26092779500088","-50483759498100","-60715850288544","-42444755653536","-15571204293888","-2305926750528"],["-3280500","-133844400","-2389122540","-24478881048","-158758432812","-677829612096","-1920476844756","-3554511242040","-4131107720928","-2818354917312","-1016591363136","-148769467776"]]},"deriv_order":0},{"coeff":{"coeffs":[["-7654500","265064400","23414503140","523721642328","5782765410360","36967767222816","145981098885672","364616134610544","574790181079212","559552961944656","322754843779380","100589855763960","13017328430400"],["21870000","2404606500","76448772000","1170601547760","10307203244208","56533286324232","200230719459984","462358822851936","689052880740960","645006040923060","362078023412880","110715477664464","14133099438720"],["50301000","2823198300","62801760780","760844239236","5671023208524","27502095133404","88811692564788","191344836746988","270948057660252","244516050866808","133758215228880","40155358843872","5058161904384"],["20776500","831278700","14639034420","149252016204","975099992796","4268842347780","12728545516764","25784277999588","34848329496480","30394428763680","16224136958016","4785417880128","595077871104"]]},"deriv_order":1},{"coeff":{"coeffs":[["3645000","243850500","6936289200","110509416180","1096023133152","7122852704664","31091186178432","91833961393800","182317786298280","238437911257236","198674047991952","100358953152516","27863281568880","3254332107600"],["9112500","535815000","13473013500","191747849400","1721753103960","10276257789072","41771326372920","116379890455536","220493512536804","278108564022648","225579109551372","111735168391512","30578324355792","3533274859680"],["7290000","372883500","8282606400","105861472560","867100080384","4788517244040","18241248908448","48175364735568","87415148521584","106591544397036","84287545960608","40973590916640","11058530438016","1264540476096"],["1822500","80919000","1598259600","18511467840","139546013976","718567753392","2581349237424","6493511769408","11324559173796","13382479415736","10332590535072","4934187347904","1314130298688","148769467776"]]},"deriv_order":2}]]}],"restart_bases":[],"row_multiplier":{"coeffs":[["1350","50220","617706","2875176","5559354","4067820","984150"],["2700","76140","695952","2723544","4767660","3332988","787320"],["1350","25920","187596","635688","1019142","682344","157464"]]},"start_base":0}},"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 >= 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) 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":[["13","33","18"],["34","132","153","54"]],"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 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/9 (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":[["13","33","18"],["34","132","153","54"]],"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"}