{"certification":{"candidate":{"gauge":{"kind":"none"},"index_shift":0,"operator":{"schedule":{"first_degree":0,"first_index":0,"step":1},"shape":"reversal"},"parent":{"first_index":0,"initial_polynomials":[["1"],["4","4"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","4"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["3","4"]]},"deriv_order":0,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent_name":"basis_map_A013611 of Riordan array ((1+x)/(1-2x),x(1+x)/(1-2x))."},"identifying_rows":1,"identity":{"certificate":{"certificate":{"dividend_relation":{"terms":[{"coeff":{"coeffs":[["-128","-128"],["80","128"],["-48","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-112","-448","-256"],["52","160","64"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["-13","-92","-176","-64"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["32"],["16"]]},"deriv_order":0,"shift":1}]},"exceptional_bases":[],"gauge":{"kind":"none"},"identifying_indices":[0],"index_shift":0,"input":{"first_index":0,"initial_polynomials":[["1"]],"recurrence":{"denominator":{"coeffs":[["16"],["16"]]},"terms":[{"coeff":{"coeffs":[["64","0","20","26"],["64","64","-60","-39"],["0","64","40","13"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","-64","96","204","52"],["0","-64","-192","-132","-26"]]},"deriv_order":1,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","0","64","176","92","13"]]},"deriv_order":2,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"input_valid_from_base":0,"multiplier":["1"],"operator":{"schedule":{"first_degree":0,"first_index":0,"step":1},"shape":"reversal"},"parent":{"first_index":0,"initial_polynomials":[["1"],["4","4"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","4"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["3","4"]]},"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":[["-256","-256","0"],["208","64","-512"],["-48","192","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-164","-368","832","768"],["52","-48","-576","-256"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["-13","-40","192","640","256"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["64"]]},"deriv_order":0,"shift":1}]},"quotient":[{"coeff":{"coeffs":[["832","9216","34816","49152","16384"],["0","3328","23552","45056","16384"],["-208","-640","3072","10240","4096"]]},"deriv_order":0}],"step_multiplier":{"coeffs":[["4607442944","153108873216","2274386509824","19892677902336","113536923598848","442673689264128","1199051789828096","2248776156708864","2856943525822464","2355153906696192","1174278418464768","316659348799488","35184372088832"],["-6911164416","-174373994496","-1795430547456","-9010975604736","-14905415565312","76832669958144","550133771010048","1620611419865088","2724795972059136","2709746406653952","1530520185864192","448600744132608","52776558133248"],["3455582208","59542339584","310797926400","-328564998144","-9254983434240","-31207232372736","3427383902208","276252296478720","773815667785728","999456069648384","656408441782272","211106232532992","26388279066624"],["-575930368","-5316280320","9160359936","225318010880","422181863424","-2657511014400","-10746008174592","-773094113280","58291296141312","116135915683840","92358976733184","32985348833280","4398046511104"]]},"step_quotients":[[{"coeff":{"coeffs":[["6911164416","248093081600","3987155714048","37711691907072","231681004929024","959016805072896","2660977053007872","4627981880262656","3688105596944384","-3029704290336768","-11673514952097792","-13669128556511232","-8074813394386944","-2392537302040576","-281474976710656"],["-2303721472","10986979328","1679726477312","30204827271168","275704688148480","1538011145699328","5540535729127424","12804122143096832","17317239417995264","8128826903101440","-12978085498454016","-24950117857492992","-17486632928149504","-5664683906301952","-703687441776640"],["-10366746624","-351406129152","-4877073776640","-34764572590080","-117955639640064","29610309844992","2002890352754688","8660664113430528","18553537164214272","20039630208368640","4824931900588032","-11947293347414016","-12455267719446528","-4697113673859072","-633318697598976"],["10366746624","228157030400","1753581879296","2913346781184","-35375162589184","-223209853026304","-350641666916352","1169150227513344","6249074336464896","11511371346739200","9072482757640192","713583046426624","-3021457953128448","-1592092837019648","-246290604621824"],["-3599564800","-47625011200","-71047315456","1679776808960","8198304038912","-7857441341440","-136977781358592","-252221954457600","430961313447936","2189316629463040","3014311127547904","1586045523066880","113249697660928","-153931627888640","-35184372088832"],["431947776","2259419136","-22819110912","-141507428352","359317635072","3259678851072","86973087744","-31658203938816","-46037754445824","87771951661056","279138514501632","252337918574592","95657511616512","13194139533312","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["-8063025152","-297888907264","-4956954296320","-48946403606528","-317669605638144","-1414903155916800","-4362430494801920","-9050204762275840","-11279099515371520","-4104133309104128","12054495731122176","24089200252944384","21418486509076480","10432166324338688","2674012278751232","281474976710656"],["15838085120","471022436352","5939430162432","39747321856000","132326432440320","-1591285383168","-2053034632806400","-9734221253836800","-24414647104831488","-36834051847356416","-31947547295612928","-11343661463764992","4593759580848128","6122080743456768","2216615441596416","281474976710656"],["-11662589952","-263155875840","-2182905593856","-5557217918976","31555376381952","277828281040896","716752463855616","-432314228146176","-7645862125633536","-22274387591823360","-34134269764829184","-30518044740550656","-15704324579524608","-4274901208793088","-474989023199232","0"],["3815538688","58833502208","192987791360","-1529482313728","-12517875122176","-13819728363520","150369892040704","603718856736768","354289704763392","-2939475617382400","-8975141618843648","-12138333492740096","-8965967568699392","-3703155162349568","-800444465020928","-70368744177664"],["-467943424","-3887529984","16613376000","226350858240","112856137728","-4540367634432","-11438907195392","29660238839808","155285616328704","100583839105024","-533589556985856","-1320857062342656","-1316940052168704","-669602581315584","-171523813933056","-17592186044416"]]},"deriv_order":1},{"coeff":{"coeffs":[["-935886848","-33979891712","-543855476736","-4956790718464","-27122433261568","-77844336082944","28406645260288","1336770989916160","6492238204895232","18243560784527360","34144302808432640","43831756163383296","38297089507065856","22091387625275392","7969260278120448","1618481116086272","140737488355328"],["1403830272","39739195392","452947083264","2360264884224","1501846044672","-51975479623680","-301774065893376","-627620349739008","792750031110144","8417087928139776","24576558781956096","40811947477696512","42297112808914944","27457004368822272","10766417859182592","2322168557862912","211106232532992"],["-701915136","-14254276608","-89978044416","85673902080","3626911137792","14483787350016","-10999075700736","-245741654114304","-668649098575872","51552492453888","4339686495485952","11388397843120128","14921747178455040","11178734719598592","4815860929658880","1108307720798208","105553116266496"],["116985856","1439825920","-265814016","-73201090560","-254564892672","1022235770880","7400094433280","4023847485440","-68481642921984","-180431576104960","32813550141440","863803822571520","1650092075384832","1484340697497600","712483534798848","175921860444160","17592186044416"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","4607442944","97819557888","731956379648","1219502276608","-14092324569088","-90969554812928","-161868727451648","386615776116736","2505099804934144","5459624987721728","6205643627167744","3782319999549440","1161084278931456","140737488355328"],["-3455582208","-68757225472","-432717955072","134888816640","13446334644224","52382494883840","-18927920873472","-618269132193792","-1473929696772096","-116273354637312","4932409162203136","8699335998963712","6412351813189632","2181431069507584","281474976710656"],["-2015756288","-60073967616","-594905399296","-1690572947456","9880203165696","83883664080896","165153840562176","-394329537380352","-2454393421037568","-4415982294532096","-2553478316556288","1726233255608320","2812550743851008","1213860837064704","175921860444160"],["2735669248","36195008512","52890173440","-1286837633024","-6213123178496","6404266000384","104913703010304","186586264240128","-348162933915648","-1665364979089408","-2178957168345088","-982413639417856","91259465105408","180319906955264","35184372088832"],["-431947776","-2259419136","22819110912","141507428352","-359317635072","-3259678851072","-86973087744","31658203938816","46037754445824","-87771951661056","-279138514501632","-252337918574592","-95657511616512","-13194139533312","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["-287965184","-10721165312","-148174274560","-905994829824","-1070688370688","18558419468288","115178674847744","228674796257280","-381315786473472","-3232942142783488","-8352577519353856","-11901663614861312","-10060531394150400","-4952200371503104","-1301821767286784","-140737488355328"],["4031512576","91927347200","763445116928","1865815162880","-11848741027840","-98708884553728","-234992156278784","244423367589888","2795353694797824","7291703417372672","9620864181993472","6447261307371520","1363394418442240","-734473767354368","-457396837154816","-70368744177664"],["-2879651840","-43571347456","-134065684480","1179562016768","9081674792960","8252813213696","-113436797173760","-423795697385472","-182450210734080","2183380984659968","6213271489085440","8001283554279424","5618504417935360","2188028139274240","439804651110400","35184372088832"],["467943424","3887529984","-16613376000","-226350858240","-112856137728","4540367634432","11438907195392","-29660238839808","-155285616328704","-100583839105024","533589556985856","1320857062342656","1316940052168704","669602581315584","171523813933056","17592186044416"]]},"deriv_order":1},{"coeff":{"coeffs":[["-467943424","-13246398464","-150982361088","-786754961408","-500615348224","17325159874560","100591355297792","209206783246336","-264250010370048","-2805695976046592","-8192186260652032","-13603982492565504","-14099037602971648","-9152334789607424","-3588805953060864","-774056185954304","-70368744177664"],["467943424","9502851072","59985362944","-57115934720","-2417940758528","-9655858233344","7332717133824","163827769409536","445766065717248","-34368328302592","-2893124330323968","-7592265228746752","-9947831452303360","-7452489813065728","-3210573953105920","-738871813865472","-70368744177664"],["-116985856","-1439825920","265814016","73201090560","254564892672","-1022235770880","-7400094433280","-4023847485440","68481642921984","180431576104960","-32813550141440","-863803822571520","-1650092075384832","-1484340697497600","-712483534798848","-175921860444160","-17592186044416"]]},"deriv_order":2}]]},{"annihilator":{"terms":[{"coeff":{"coeffs":[["0","0","0"],["-160","-640","-1024"],["304","448","-512"],["-48","192","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["120","1056","2688","1536"],["-268","-1104","-576","256"],["52","-48","-576","-256"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["26","288","1088","1536","512"],["-13","-40","192","640","256"]]},"deriv_order":2,"shift":0}]},"quotient":[{"coeff":{"coeffs":[["-416","-4608","-17408","-24576","-8192"],["208","640","-3072","-10240","-4096"]]},"deriv_order":0}],"step_multiplier":{"coeffs":[["4607442944","153108873216","2274386509824","19892677902336","113536923598848","442673689264128","1199051789828096","2248776156708864","2856943525822464","2355153906696192","1174278418464768","316659348799488","35184372088832"],["-6911164416","-174373994496","-1795430547456","-9010975604736","-14905415565312","76832669958144","550133771010048","1620611419865088","2724795972059136","2709746406653952","1530520185864192","448600744132608","52776558133248"],["3455582208","59542339584","310797926400","-328564998144","-9254983434240","-31207232372736","3427383902208","276252296478720","773815667785728","999456069648384","656408441782272","211106232532992","26388279066624"],["-575930368","-5316280320","9160359936","225318010880","422181863424","-2657511014400","-10746008174592","-773094113280","58291296141312","116135915683840","92358976733184","32985348833280","4398046511104"]]},"step_quotients":[[{"coeff":{"coeffs":[["6911164416","229663309824","3301001134080","26164403896320","115720109162496","186586264240128","-926308481630208","-7251004307275776","-24491827667140608","-50437896900968448","-66805226992041984","-56048704737509376","-28129905485021184","-7599824371187712","-844424930131968"],["11518607360","525602914304","10119035224064","109826273181696","745857041301504","3273626757365760","9000003037036544","12690735006482432","-4681102035779584","-58463644588965888","-118326692602183680","-122956186310934528","-69946531712598016","-20442120183611392","-2392537302040576"],["-16126050304","-372316831744","-2091888148480","22412380864512","432098808692736","3184744288223232","13488307212124160","34819729365401600","51015277944504320","24911978547904512","-44521149953998848","-87615683570958336","-62848084643676160","-20706002974277632","-2603643534573568"],["-5183373312","-327748681728","-6302409424896","-56915782533120","-250314988978176","-233140622721024","3033126842400768","16567587236216832","40446892437405696","50370380015075328","21656943093350400","-17967119509487616","-24356381578493952","-9842828091850752","-1372190511464448"],["11086659584","281452740608","2518308356096","6406421872640","-42093380632576","-340155034501120","-697910710763520","1371739539898368","9756099817242624","20145922059010048","18506292523958272","4930759894761472","-3007164301967360","-2106664278818816","-351843720888320"],["-4031512576","-56795594752","-112023568384","1931208556544","10542802534400","-6050937831424","-168954886619136","-349515848613888","467721938534400","2801040231497728","4128803601252352","2442015325290496","413416372043776","-114349209288704","-35184372088832"],["431947776","2259419136","-22819110912","-141507428352","359317635072","3259678851072","86973087744","-31658203938816","-46037754445824","87771951661056","279138514501632","252337918574592","95657511616512","13194139533312","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["-6911164416","-236574474240","-3530664443904","-29465405030400","-141884513058816","-302306373402624","739722217390080","8177312788905984","31742831974416384","74929724568109056","117243123893010432","122853931729551360","84178610222530560","35729729856208896","8444249301319680","844424930131968"],["-1439825920","-206803304448","-6034468896768","-85913338118144","-737347670900736","-4161613124861952","-16032212583448576","-42420910946254848","-75101480310276096","-81169865372598272","-35371426504507392","29614246182518784","53860676598235136","33513114414612480","9816439812784128","1125899906842624"],["16270032896","602866188288","9275968585728","76089892274176","335835857682432","479725835255808","-3059354328629248","-21383667209207808","-66698990975975424","-125202626005434368","-147583666225152000","-105899462429245440","-41523056622960640","-6016527627190272","897201488265216","281474976710656"],["-13606354944","-345026592768","-3291534065664","-11477943582720","31871735955456","431994118864896","1422748853207040","343360086736896","-11798401863647232","-41708736649101312","-73146557226024960","-75001261543391232","-45706148610834432","-16017685393440768","-2929098976395264","-211106232532992"],["4283482112","70208126976","268523274240","-1653051752448","-15841219313664","-23927011147776","175864079712256","813302254927872","681414815121408","-3594986410999808","-12270601305587712","-17596240493543424","-13630370771632128","-5887884766740480","-1332608092864512","-123145302310912"],["-467943424","-3887529984","16613376000","226350858240","112856137728","-4540367634432","-11438907195392","29660238839808","155285616328704","100583839105024","-533589556985856","-1320857062342656","-1316940052168704","-669602581315584","-171523813933056","-17592186044416"]]},"deriv_order":1},{"coeff":{"coeffs":[["935886848","48954081280","1147430502400","16072778448896","150895035678720","1006893677936640","4933300099481600","18055549664886784","49688708575657984","102604415059361792","157350628014686208","175839122194169856","139078325309014016","74656839525990400","25561446322536448","4996180836614144","422212465065984"],["-2339717120","-96180371456","-1722474823680","-17466897989632","-106987887001600","-363352823955456","-188147484852224","4719463609925632","26761702850691072","81391331066249216","161153770015686656","216138972131229696","195485470837178368","115822554869923840","42643458971664384","8796093022208000","774056185954304"],["2105745408","65224114176","815916122112","4806203670528","6630603227136","-89467171897344","-614547207487488","-1500982353592320","916850963644416","16885728348733440","53492804059398144","93012292798513152","99515972796284928","66092743457243136","26348696648024064","5752644836524032","527765581332480"],["-818900992","-17565876224","-120236539904","41030778880","4581316624384","20333952237568","-7265339834368","-323631691333632","-960013774356480","-111694919499776","5819062210789376","16048334280065024","21545754979991552","16389320323629056","7133631441010688","1653665488175104","158329674399744"],["116985856","1439825920","-265814016","-73201090560","-254564892672","1022235770880","7400094433280","4023847485440","-68481642921984","-180431576104960","32813550141440","863803822571520","1650092075384832","1484340697497600","712483534798848","175921860444160","17592186044416"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["6911164416","234270752768","3546258866176","31795844218880","189719979753472","809059632545792","2615903518720000","6752685021724672","14264445383475200","24028039918649344","30076590821998592","25521863903936512","13229323905400832","3694359069327360","422212465065984"],["8063025152","337052172288","5816065196032","55681231093760","331156876689408","1295805054976000","3511644718104576","7325942896656384","14259875538272256","27644058784497664","43489533169238016","44908452924882944","26643365764268032","8127589952520192","985162418487296"],["-11230642176","-244194476032","-1777409720320","-1664568262656","44428785876992","227087268970496","162747585134592","-1905110053552128","-6461494828990464","-6125791595200512","6938330688126976","20336567067344896","16947872230539264","6086896371367936","809240558043136"],["-1871773696","-88117346304","-1103305375744","-4333395509248","13298980356096","165262087159808","419658033266688","-517573623939072","-4939208095432704","-10479221986033664","-8824817763483648","-468941709246464","3438172860055552","1807597116063744","281474976710656"],["3167617024","45365592064","93866426368","-1538269380608","-8557621673984","4597762490368","136890808270848","283880158396416","-384923559002112","-2277088581124096","-3293449642049536","-1838383441641472","-208907209277440","140737488355328","35184372088832"],["-431947776","-2259419136","22819110912","141507428352","-359317635072","-3259678851072","-86973087744","31658203938816","46037754445824","-87771951661056","-279138514501632","-252337918574592","-95657511616512","-13194139533312","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["-7199129600","-256510525440","-4132494639104","-39967094996992","-260420409491456","-1220167862321152","-4300193734328320","-11790855606108160","-25671251456425984","-44347598915502080","-59202791280738304","-58183406562836480","-39457074274369536","-17002847811928064","-4116571534393344","-422212465065984"],["3167617024","44789661696","-104962457600","-5923191914496","-47019120918528","-140189678698496","153615947792384","2594874285096960","9035176671707136","15767701116944384","12921185771716608","-610503831322624","-10416773161549824","-8404666882719744","-2814749767106560","-351843720888320"],["5039390720","143561719808","1509060247552","5977342476288","-11766650109952","-204479601311744","-717538174435328","-260569760268288","5699700774666240","20427302546440192","35273157652774912","34769993644113920","19715342997651456","6093493441134592","879609302220800","35184372088832"],["-3347595264","-54945972224","-209601167360","1303131455488","12405018984448","18360095997952","-138930984845312","-633379095576576","-509575321092096","2838891778277376","9508731175829504","13459190555082752","10282907620868096","4372757743665152","971968278953984","87960930222080"],["467943424","3887529984","-16613376000","-226350858240","-112856137728","4540367634432","11438907195392","-29660238839808","-155285616328704","-100583839105024","533589556985856","1320857062342656","1316940052168704","669602581315584","171523813933056","17592186044416"]]},"deriv_order":1},{"coeff":{"coeffs":[["467943424","20733493248","392873115648","4170035757056","26621817913344","95169495957504","72184710037504","-1127564206669824","-6756488215265280","-21049256760573952","-42336489069084672","-57435738655948800","-52396127110037504","-31243722414882816","-11558066231181312","-2392537302040576","-211106232532992"],["-935886848","-30236344320","-392961720320","-2417380818944","-3919786803200","42319621390336","309106783027200","791448119148544","-346983965392896","-8451456256442368","-27469683112280064","-48404212706443264","-52244944261218304","-34909494181888000","-13976991812288512","-3061040371728384","-281474976710656"],["584929280","12814450688","90243858432","-12472811520","-3372346245120","-15506023120896","3598981267456","241717806628864","737130741497856","128879083651072","-4372500045627392","-12252201665691648","-16571839253839872","-12663075417096192","-5528344464457728","-1284229581242368","-123145302310912"],["-116985856","-1439825920","265814016","73201090560","254564892672","-1022235770880","-7400094433280","-4023847485440","68481642921984","180431576104960","-32813550141440","-863803822571520","-1650092075384832","-1484340697497600","-712483534798848","-175921860444160","-17592186044416"]]},"deriv_order":2}]]}],"restart_bases":[],"row_multiplier":{"coeffs":[["1664","18432","69632","98304","32768"],["-832","-2560","12288","40960","16384"]]},"start_base":0}},"shifted_parent_relation":{"terms":[{"coeff":{"coeffs":[["-1","-4"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-3","-4"]]},"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 = 0 + 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"},"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 = 0 + 1 (n - 0)","kind":"preserver_image","operator":{"schedule":{"first_degree":0,"first_index":0,"step":1},"shape":"reversal"}},"parent":{"gauge":{"kind":"none"},"index_shift":0,"recurrence":{"first_index":0,"initial_polynomials":[["1"],["4","4"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","4"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["3","4"]]},"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 = 0 + 1 (n - 0), for every n >= 0"},"parent_proof":{"route":"liu_wang_three_term","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_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":"not applicable: c_2(n, x) = gamma(n) w(x) with w neither constant nor a constant times a square (x + v_0)^2","route":"three_term_recurrence","success":false,"variant":"three_term_recurrence"},{"detail":"not applicable: the rule is not f(n) P_n = c_0(n, x) P_(n-1) + c_1(n, x) P'_(n-1)","route":"liu_wang","success":false,"variant":"liu_wang"},{"detail":"HypothesisFailed: P_n = A_n(x) P_(n-1) + V_n(x) P'_(n-1) + W_n(x) P_(n-2) for n >= 2, with A_n(x) = (3) + (4) x, V_n(x) = 0, W_n(x) = (1) + (4) x; open hypotheses: multipliers_vanish_at_zero: [x^0] c_2(n, x) = 1 is not the zero polynomial; lag_coefficient_nonpositive: W_n is not separable with a factor of one sign on (-inf, 0), and the sufficient monomial test (-1)^k [x^k] W_n <= 0 fails for k = 0 (not a disproof): fails at n = 2: [x^0] W_n = 1 there (exact); derivative_or_lag_coefficient_negative: W_n is not separable with a factor of one sign on (-inf, 0), and the sufficient monomial test (-1)^k [x^k] W_n <= 0 fails for k = 0 (not a disproof): fails at n = 2: [x^0] W_n = 1 there (exact)","route":"liu_wang_derivative_lag","success":false,"variant":"liu_wang_derivative_lag"},{"detail":"not applicable: the rule is not f(n) P_n = c_0(n, x) P_(n-1) + gamma(n) (x - L)(x - U) P'_(n-1)","route":"ma_wang_interval","success":false,"variant":"ma_wang_interval"},{"detail":"P_n = A_n(x) P_(n-1) + B_n(x) P_(n-2) for n >= 2, with A_n(x) = (3) + (4) x, B_n(x) = (1) + (4) x: every P_n, n >= 0, is nonzero and real-rooted with every root in (-inf, -1/4] (so its coefficients have one sign); for n >= 1, P_(n-1) interlaces P_n (weakly, in the sense of Liu and Wang), and deg P_n - deg P_(n-1) is 0 or 1 for n >= 2","route":"liu_wang_three_term","success":true,"variant":"liu_wang_three_term"}],"conditional_on":[],"interlacing":{"from_index":1,"justification":{"premises":["every hypothesis of the theorem is verified exactly for every index: P_n = A_n(x) P_(n-1) + B_n(x) P_(n-2) for n >= 2, with A_n(x) = (3) + (4) x, B_n(x) = (1) + (4) x","every P_n, n >= 0, is nonzero and real-rooted with every root in (-inf, -1/4] (so its coefficients have one sign); for n >= 1, P_(n-1) interlaces P_n (weakly, in the sense of Liu and Wang), and deg P_n - deg P_(n-1) is 0 or 1 for n >= 2"],"theorem":"liu_wang_three_term: L. L. Liu and Y. Wang, Adv. Appl. Math. 38 (2007) 542-560, Theorem 2.1 and Corollary 2.4 (A unified approach to polynomial sequences with only real zeros; the lag row as the interlacer, b_n = 0), weak interlacing of consecutive rows, with nonnegativity of the coefficients replaced, where a root region is certified, by an exact root-location induction"},"kind":"weak","orientation":"previous_interlaces_next"},"route":"liu_wang_three_term","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 = 0 + 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"}