{"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: coefficient of P_(n-1) must be 1 (+ w(n) t) after normalization)","route":"paper_theorem","success":false,"variant":"match_recurrence_theorems"},{"detail":"source claim: every P_n, n >= 0, is real-rooted in (-inf, 0] (CertifiedFamilyInvariant): the completed induction for Q_n and real_affine_equivalence (target to source; every map condition certified for all indices)","route":"root_domain","success":true,"variant":"identity (affine 1, 0)"}],"conditional_on":[],"route":"root_domain","rows_checked":10,"statement":"every parent row P_n, n >= 0, is zero or real-rooted with coefficients of one sign","status":"proved"},"record":{"first_index":0,"initial_polynomials":[["1"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["-2","1"],["3","0"]]},"deriv_order":0,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"try_root_domain":true}