{"kind":"parent_provers","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":"no theorem matched (weighted_renewal_window: coefficients must be index-independent; fixed_delay_predecessor_window: derivatives and alternating signs are unsupported)","route":"paper_theorem","success":false,"variant":"match_recurrence_theorems"},{"detail":"no unconditional all-index source claim with roots in (-inf, 0]","route":"root_domain","success":false,"variant":"identity (affine 1, 0)"},{"detail":"no affine degree schedule fits the first parent rows","route":"root_domain","success":false,"variant":"f_polynomial"},{"detail":"no affine degree schedule fits the first parent rows","route":"root_domain","success":false,"variant":"reversal"},{"detail":"no affine degree schedule fits the first parent rows","route":"root_domain","success":false,"variant":"mobius (1, 0, -1, 1)"},{"detail":"no unconditional all-index source claim with roots in (-inf, 0]","route":"root_domain","success":false,"variant":"identity (affine 1, 0), induction start moved 1 row(s)"},{"detail":"source claim: every P_n, n >= 2, is real-rooted in (-inf, 0] (CertifiedFamilyInvariant): the completed induction for Q_n and real_mobius_equivalence (target to source; every map condition certified for all indices); deg Q_n = d_n by the degree formula, so no root of P_n is added at the image of infinity (source moved 1 row(s) past the parent seeds; the earlier parent rows are among the rows checked exactly to be zero or real-rooted with coefficients of one sign)","route":"root_domain","success":true,"variant":"f_polynomial, induction start moved 1 row(s)"}],"conditional_on":[],"route":"root_domain","rows_checked":10,"statement":"every parent row P_n, n >= 1, is zero or real-rooted with coefficients of one sign","status":"proved"},"record":{"first_index":1,"initial_polynomials":[["1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","-2"],["0","1"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["0","1","-1"]]},"deriv_order":1,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"try_root_domain":true}