{"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":"source claim: every P_n, n >= 1, 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","route":"root_domain","success":true,"variant":"f_polynomial"}],"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","6","1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","1"],["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}