{"certification":{"candidate":{"gauge":{"kind":"none"},"index_shift":0,"operator":{"intercept":"1","shape":"affine","slope":"1"},"parent":{"first_index":0,"initial_polynomials":[["4"],["8","1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["2","0"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["-1","1"]]},"deriv_order":0,"offset":2,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent_name":"veronese_section_2_1 of The truncated (4,4,1)-Pascal triangle, given by 4*C(n-2, k) + 4*C(n-2, k-1) + C(n-2, k-2) for n>=2."},"identifying_rows":1,"identity":{"certificate":{"certificate":{"dividend_relation":{"terms":[{"coeff":{"coeffs":[["-16","-2"],["2","-1"],["-4","1"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["24","-42","6"],["0","16","-4"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","16","-20","4"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["8"],["2"]]},"deriv_order":0,"shift":1}]},"exceptional_bases":[],"gauge":{"kind":"none"},"identifying_indices":[0],"index_shift":0,"input":{"first_index":0,"initial_polynomials":[["4"]],"recurrence":{"denominator":{"coeffs":[["6"],["2"]]},"terms":[{"coeff":{"coeffs":[["22","0"],["-7","3"],["3","-1"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["24","38","-10"],["-12","-8","4"]]},"deriv_order":1,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","12","8","-4"]]},"deriv_order":2,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"input_valid_from_base":0,"multiplier":["1"],"operator":{"intercept":"1","shape":"affine","slope":"1"},"parent":{"first_index":0,"initial_polynomials":[["4"],["8","1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["2","0"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["-1","1"]]},"deriv_order":0,"offset":2,"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":[["-48","-6","0"],["16","0","-1"],["-16","8","-1"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["96","-176","46","-2"],["0","64","-32","4"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","64","-96","36","-4"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["24"]]},"deriv_order":0,"shift":1}]},"quotient":[{"coeff":{"coeffs":[["0","-512","1152","-768","128"],["0","-640","1056","-480","64"],["0","-128","192","-72","8"]]},"deriv_order":0}],"step_multiplier":{"coeffs":[["0","0","0","-3623878656","24461180928","-71345111040","117379694592","-119248257024","76950798336","-31255953408","7644119040","-1019215872","56623104"],["0","0","0","-10871635968","65229815808","-167151403008","238496514048","-207283027968","113005559808","-38475399168","7898923008","-891813888","42467328"],["0","0","0","-10871635968","57076088832","-126382768128","153901596672","-113005559808","51820756992","-14906032128","2611740672","-254803968","10616832"],["0","0","0","-3623878656","16307453952","-30576476160","31255953408","-19237699584","7453016064","-1834057728","278691840","-23887872","884736"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","0","0","0","-301989888","2340421632","-7983857664","15727067136","-19718995968","16349921280","-9017229312","3241672704","-721944576","89653248","-4718592"],["0","0","0","2415919104","-19629342720","70665633792","-148239286272","200474099712","-182620127232","113734582272","-48175644672","13547077632","-2405302272","243007488","-10616832"],["0","0","0","9663676416","-69155684352","217810206720","-396927959040","463035432960","-361520824320","192089456640","-69323489280","16659578880","-2545090560","223248384","-8552448"],["0","0","0","14495514624","-92710895616","258956328960","-415330467840","423540817920","-287698452480","132790026240","-41729679360","8781004800","-1183334400","92307456","-3170304"],["0","0","0","9663676416","-54962159616","135442464768","-190366875648","169388015616","-100329062400","40515600384","-11209162752","2092511232","-252186624","17731584","-552960"],["0","0","0","2415919104","-12079595520","25971130368","-31708938240","24517804032","-12683575296","4508614656","-1107689472","185241600","-20164608","1290240","-36864"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","-14495514624","114756157440","-401646551040","816429662208","-1064344485888","926821122048","-543907381248","211388203008","-51569491968","6837239808","-221773824","-51904512","4718592"],["0","0","0","-43486543872","301989888000","-909291552768","1547698176000","-1621968814080","1058144256000","-398538178560","53968896000","21428305920","-12386304000","2723807232","-294912000","12976128"],["0","0","0","-43486543872","250047627264","-589786251264","703258951680","-369465753600","-84722319360","262925844480","-187002224640","73614458880","-17809735680","2638282752","-220299264","7962624"],["0","0","0","-14495514624","53150220288","-33822867456","-138009378816","349138059264","-392341487616","263778729984","-115259867136","33631248384","-6521389056","808501248","-58097664","1843200"],["0","0","0","0","-9663676416","48318382080","-103884521472","126835752960","-98071216128","50734301184","-18034458624","4430757888","-740966400","80658432","-5160960","147456"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","-9663676416","79725330432","-293534171136","635688714240","-898608660480","870155550720","-589588070400","280709038080","-93003448320","20903362560","-3029336064","254803968","-9437184"],["0","0","0","0","-28991029248","217432719360","-722963791872","1404252979200","-1768339537920","1516083609600","-905297264640","379020902400","-110521221120","21941452800","-2824077312","212336640","-7077888"],["0","0","0","0","-28991029248","195689447424","-581632524288","1003361402880","-1116041379840","842127114240","-442191052800","163154165760","-42122280960","7449477120","-859963392","58392576","-1769472"],["0","0","0","0","-9663676416","57982058496","-152202903552","230720274432","-224906969088","148805517312","-68768759808","22465216512","-5171724288","821624832","-85819392","5308416","-147456"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","0","0","3623878656","-23857201152","68702699520","-113812439040","120111759360","-84598456320","40556298240","-13253345280","2901934080","-406978560","33030144","-1179648"],["0","0","0","9663676416","-61001957376","168661352448","-268846497792","273885954048","-186990723072","87303979008","-27915190272","6005587968","-830472192","66650112","-2359296"],["0","0","0","10871635968","-66135785472","175531622400","-267544166400","259687710720","-168436039680","74569973760","-22590627840","4605050880","-603832320","46006272","-1548288"],["0","0","0","7247757312","-41070624768","100864622592","-141331267584","125420175360","-74119643136","29875765248","-8252817408","1538666496","-185241600","13012992","-405504"],["0","0","0","2415919104","-12079595520","25971130368","-31708938240","24517804032","-12683575296","4508614656","-1107689472","185241600","-20164608","1290240","-36864"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","-14495514624","96636764160","-281152585728","468084326400","-491205427200","336907468800","-150882877440","42113433600","-6140067840","0","156893184","-23592960","1179648"],["0","0","0","-28991029248","169114337280","-416142065664","553245474816","-412555935744","142067367936","22840344576","-47301525504","22902276096","-6037438464","935460864","-80216064","2949120"],["0","0","0","-14495514624","62813896704","-89389006848","301989888","152995627008","-216470126592","158941052928","-72700526592","21805867008","-4306010112","540721152","-39223296","1253376"],["0","0","0","0","-9663676416","48318382080","-103884521472","126835752960","-98071216128","50734301184","-18034458624","4430757888","-740966400","80658432","-5160960","147456"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","-9663676416","72477573120","-240987930624","468084326400","-589446512640","505361203200","-301765754880","126340300800","-36840407040","7313817600","-941359104","70778880","-2359296"],["0","0","0","0","-19327352832","130459631616","-387755016192","668907601920","-744027586560","561418076160","-294794035200","108769443840","-28081520640","4966318080","-573308928","38928384","-1179648"],["0","0","0","0","-9663676416","57982058496","-152202903552","230720274432","-224906969088","148805517312","-68768759808","22465216512","-5171724288","821624832","-85819392","5308416","-147456"]]},"deriv_order":2}]]},{"annihilator":{"terms":[{"coeff":{"coeffs":[["0","0","0"],["8","-6","4"],["0","-20","5"],["16","-8","1"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-96","200","-112","8"],["-96","112","34","-14"],["0","-64","32","-4"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","-64","144","-96","16"],["0","-64","96","-36","4"]]},"deriv_order":2,"shift":0}]},"quotient":[{"coeff":{"coeffs":[["0","-128","288","-192","32"],["0","-128","192","-72","8"]]},"deriv_order":0}],"step_multiplier":{"coeffs":[["0","0","0","-3623878656","24461180928","-71345111040","117379694592","-119248257024","76950798336","-31255953408","7644119040","-1019215872","56623104"],["0","0","0","-10871635968","65229815808","-167151403008","238496514048","-207283027968","113005559808","-38475399168","7898923008","-891813888","42467328"],["0","0","0","-10871635968","57076088832","-126382768128","153901596672","-113005559808","51820756992","-14906032128","2611740672","-254803968","10616832"],["0","0","0","-3623878656","16307453952","-30576476160","31255953408","-19237699584","7453016064","-1834057728","278691840","-23887872","884736"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","0","0","-3623878656","29595009024","-107508400128","228644093952","-315263287296","294794035200","-189956358144","83986219008","-24871698432","4685561856","-504889344","23592960"],["0","0","0","-19327352832","148277035008","-504474107904","1001775955968","-1285939003392","1116533293056","-666772439040","272997679104","-74926522368","13116506112","-1318846464","57802752"],["0","0","0","-43486543872","311955554304","-988488400896","1820659286016","-2158840774656","1724877766656","-944943169536","354258026496","-89009750016","14284947456","-1320321024","53379072"],["0","0","0","-53150220288","354234138624","-1037637255168","1757751017472","-1907462504448","1388727631872","-691056672768","234984333312","-53573419008","7817674752","-659128320","24403968"],["0","0","0","-37446746112","229814304768","-616134868992","949626077184","-932653301760","612127604736","-274085019648","83903275008","-17264848896","2282803200","-175214592","5935104"],["0","0","0","-14495514624","80933289984","-195991437312","271111421952","-237873659904","139222056960","-55664050176","15273197568","-2831597568","339296256","-23740416","737280"],["0","0","0","-2415919104","12079595520","-25971130368","31708938240","-24517804032","12683575296","-4508614656","1107689472","-185241600","20164608","-1290240","36864"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","28991029248","-233136193536","830472192000","-1721644351488","2293462204416","-2043088994304","1224856829952","-481933393920","114987368448","-12612796416","-646447104","316145664","-23592960"],["0","0","0","101468602368","-729607569408","2286365442048","-4074447568896","4500913913856","-3117045252096","1252641079296","-177209081856","-83770343424","51654426624","-12349734912","1455685632","-69599232"],["0","0","0","130459631616","-812956778496","2132350599168","-2984792555520","2228402257920","-524966952960","-563028295680","624167976960","-301274726400","84554219520","-14184677376","1322090496","-52789248"],["0","0","0","72477573120","-359971946496","654714077184","-349553295360","-560002498560","1205364326400","-1079377920000","575051857920","-196808417280","43754618880","-6121635840","490438656","-17178624"],["0","0","0","14495514624","-33822867456","-70061654016","380205268992","-672116244480","666284064768","-419350708224","175853666304","-49887387648","9477734400","-1156939776","82132992","-2580480"],["0","0","0","0","9663676416","-48318382080","103884521472","-126835752960","98071216128","-50734301184","18034458624","-4430757888","740966400","-80658432","5160960","-147456"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","19327352832","-166698418176","645050400768","-1477032542208","2222570078208","-2307929407488","1689888227328","-875931107328","317910417408","-78583431168","12542017536","-1160773632","47185920"],["0","0","0","0","67645734912","-536334041088","1897100476416","-3947007836160","5362774179840","-4996705812480","3263649546240","-1501857054720","482535014400","-105554903040","14941421568","-1231552512","44826624"],["0","0","0","0","86973087744","-630554886144","2027560108032","-3811867361280","4652720455680","-3874294333440","2252785582080","-921195970560","263164723200","-51332382720","6508118016","-483065856","15925248"],["0","0","0","0","48318382080","-318901321728","927712935936","-1568535478272","1712962142208","-1271641669632","658356830208","-240004104192","61334765568","-10754260992","1232437248","-83165184","2506752"],["0","0","0","0","9663676416","-57982058496","152202903552","-230720274432","224906969088","-148805517312","68768759808","-22465216512","5171724288","-821624832","85819392","-5308416","147456"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","0","0","-10871635968","76705431552","-238194524160","427900796928","-491715035136","377467305984","-196368924672","68814766080","-15826157568","2261385216","-179306496","5898240"],["0","0","0","-33822867456","225586446336","-660602880000","1116947349504","-1206921461760","871999340544","-428663439360","143189213184","-31868190720","4509794304","-366280704","12976128"],["0","0","0","-42278584320","267563040768","-741234180096","1182913265664","-1205236924416","821940977664","-382839422976","121980985344","-26127138816","3594829824","-286949376","10100736"],["0","0","0","-28991029248","173644185600","-453588811776","680326594560","-649948299264","415199526912","-181239939072","54207995904","-10924830720","1418121216","-107089920","3575808"],["0","0","0","-12079595520","67041755136","-161413595136","222075813888","-193905819648","113012637696","-45024215040","12316852224","-2277752832","272351232","-19021824","589824"],["0","0","0","-2415919104","12079595520","-25971130368","31708938240","-24517804032","12683575296","-4508614656","1107689472","-185241600","20164608","-1290240","36864"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","28991029248","-196897406976","581330534400","-974672363520","1014686023680","-669355868160","267738808320","-51527024640","-4122869760","4883742720","-1180827648","132120576","-5898240"],["0","0","0","72477573120","-442113196032","1144239685632","-1611720032256","1287099777024","-488459206656","-63839010816","171270733824","-91044642816","26067861504","-4367056896","403439616","-15925248"],["0","0","0","57982058496","-298366009344","599449927680","-516025221120","-30859591680","503167057920","-528629760000","296851046400","-103871324160","23326064640","-3278094336","263061504","-9216000"],["0","0","0","14495514624","-43486543872","-14495514624","241893900288","-475973812224","490412703744","-314513031168","133294325760","-38062006272","7262355456","-889159680","63258624","-1990656"],["0","0","0","0","9663676416","-48318382080","103884521472","-126835752960","98071216128","-50734301184","18034458624","-4430757888","740966400","-80658432","5160960","-147456"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","0","0","19327352832","-152202903552","534522101760","-1103773040640","1488055173120","-1375516753920","891353825280","-407049338880","129843855360","-28217180160","3970695168","-325582848","11796480"],["0","0","0","0","48318382080","-347892350976","1110718808064","-2073160581120","2512367124480","-2077501685760","1200091299840","-487790346240","138602741760","-26907770880","3397386240","-251265024","8257536"],["0","0","0","0","38654705664","-253671505920","733835427840","-1234081677312","1340948348928","-990932631552","510959812608","-185619382272","47294005248","-8271101952","945782784","-63700992","1916928"],["0","0","0","0","9663676416","-57982058496","152202903552","-230720274432","224906969088","-148805517312","68768759808","-22465216512","5171724288","-821624832","85819392","-5308416","147456"]]},"deriv_order":2}]]}],"restart_bases":[],"row_multiplier":{"coeffs":[["0","-1536","3456","-2304","384"],["0","-1536","2304","-864","96"]]},"start_base":0}},"shifted_parent_relation":{"terms":[{"coeff":{"coeffs":[["1","-1"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-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 = P((1) x + (1)); 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":"no parent theorem report with an interlacing conclusion","status":"none"},"lean_declarations":["Polynomial.Splits.comp_of_degree_le_one"],"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":"no parent theorem report with an interlacing conclusion","status":"not_proved"},"lean_replay":"not_attempted","operation":{"description":"P((1) x + (1))","kind":"preserver_image","operator":{"intercept":"1","shape":"affine","slope":"1"}},"parent":{"gauge":{"kind":"none"},"index_shift":0,"recurrence":{"first_index":0,"initial_polynomials":[["4"],["8","1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["2","0"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["-1","1"]]},"deriv_order":0,"offset":2,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"relation":"Q_n = lambda(n) T_n(P_(n+0)) with T = P((1) x + (1)), 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, -1]","input_root_region":{"upper":{"closed":true,"value":"-1"}},"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) = (2), V_n(x) = 0, W_n(x) = (-1) + (1) x; open hypotheses: degree_step_positive: fails at n = 2: lambda_n = 0 = 0 there (exact); multipliers_vanish_at_zero: [x^0] c_2(n, x) = -1 is not the zero polynomial","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) = (2), B_n(x) = (-1) + (1) x: every P_n, n >= 0, is nonzero and real-rooted with every root in (-inf, 0) (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) = (2), B_n(x) = (-1) + (1) x","every P_n, n >= 0, is nonzero and real-rooted with every root in (-inf, 0) (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 = P((1) x + (1)) 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, -1]"},"kind":"preserver_image"}