{"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":"Q_0 = 1, Q_n = Q_(n-1) + w(n) t Q_(max(0, n-1)), w(n) = n (paper_proof_not_lean_checked): For every n >= 1: Q_n has nonnegative coefficients and constant term 1, is real-rooted, and Q_i << Q_n (oriented weak interlacing) for p(n) <= i <= n. Hence Q_A << Q_B whenever 0 <= A <= B and B - A <= 1.; the identifying seeds equal the canonical rows (Canonical), so every parent row is a canonical row","route":"paper_theorem","success":true,"variant":"fixed_delay_predecessor_window"}],"conditional_on":[],"interlacing":{"from_index":1,"justification":{"premises":["p(n) = max(0, n-1) with 1 >= 1 is nondecreasing and 0 <= p(n) < n for n >= 1 (exact_structural)","w(n) >= 0 for every integer n >= 1: w(1+m) has nonnegative coefficients [1, 1] in m (exact_symbolic_certificate)","window: Q_A << Q_B for 0 <= A <= B with B - A <= 1 (B - A <= 1)","the identifying parent seeds equal the canonical rows (Canonical), so every parent row is a canonical row and consecutive parent rows are consecutive canonical rows"],"theorem":"fixed_delay_predecessor_window (paper_proof_not_lean_checked; https://github.com/PerAlexandersson/RealRooted/issues/2037): For every n >= 1: Q_n has nonnegative coefficients and constant term 1, is real-rooted, and Q_i << Q_n (oriented weak interlacing) for p(n) <= i <= n. Hence Q_A << Q_B whenever 0 <= A <= B and B - A <= 1."},"kind":"weak","orientation":"previous_interlaces_next"},"route":"paper_theorem","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":[["1","0"],["0","1"]]},"deriv_order":0,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"try_root_domain":true}