Decomposable forms on linear recurrences
TheoremHomogeneous forms taking the values of a power on recurrence sequences#●ready to prove
Let \(\gamma_0, \dots, \gamma_{k-1} \in \mathbb{C}\) and let \(\chi(x) = x^k - \sum_{i\lt k} \gamma_i x^i\) be the characteristic polynomial of the recurrence \(G_{n+k} = \sum_{i\lt k} \gamma_i G_{n+i}\). Let \(G^{(1)}, \dots, G^{(k)} \colon \mathbb{Z} \to \mathbb{C}\) be \(\mathbb{C}\)-linearly independent sequences, each satisfying this recurrence for every \(n \in \mathbb{Z}\). Then there is a homogeneous polynomial \(F\) of degree \(k\) in \(k\) variables with complex coefficients such that \(F(G^{(1)}_n, \dots, G^{(k)}_n) = ((-1)^k \chi(0))^n\) for every \(n \in \mathbb{Z}\).
For \(k \ge 1\) we have \(\chi(0) = -\gamma_0\), so the right side is \(((-1)^{k+1} \gamma_0)^n\). The source also assumes \(\gamma_0 \neq 0\); for \(\mathbb{Z}\)-indexed solutions, linear independence already forces it.
public theorem_wanted exists_homogeneous_form_eval_eq_pow_of_linearRecurrence
(E : LinearRecurrence ℂ) (G : Fin E.order → ℤ → ℂ)
(hG : ∀ j (n : ℤ), G j (n + E.order) = ∑ i, E.coeffs i * G j (n + (i : ℕ)))
(hind : LinearIndependent ℂ G) :
∃ F : MvPolynomial (Fin E.order) ℂ, F.IsHomogeneous E.order ∧
∀ n : ℤ, MvPolynomial.eval (fun j => G j n) F =
((-1) ^ E.order * E.charPoly.coeff 0) ^ n
Sources
- Kálmán Győry, Attila Pethő and László Szalay, Decomposable Forms Generated by Linear Recurrences, Journal of Integer Sequences 27 (2024), Article 24.3.5, Theorem 1 (
jis-2024-24.3.5-thm-1).
TheoremDecomposable forms taking the values of a power on recurrence sequences#●ready to prove
Let \(\gamma_0, \dots, \gamma_{k-1} \in \mathbb{C}\), let \(\chi(x) = x^k - \sum_{i\lt k} \gamma_i x^i\), and let \(G^{(1)}, \dots, G^{(k)} \colon \mathbb{Z} \to \mathbb{C}\) be \(\mathbb{C}\)-linearly independent sequences, each satisfying \(G_{n+k} = \sum_{i\lt k} \gamma_i G_{n+i}\) for every \(n \in \mathbb{Z}\). Then there are linear forms \(L_1, \dots, L_k\) in \(k\) variables with complex coefficients whose product \(F = L_1 \cdots L_k\) satisfies \(F(G^{(1)}_n, \dots, G^{(k)}_n) = ((-1)^k \chi(0))^n\) for every \(n \in \mathbb{Z}\).
For \(k \ge 1\) we have \(\chi(0) = -\gamma_0\), so the right side is \(((-1)^{k+1} \gamma_0)^n\).
public theorem_wanted exists_decomposable_form_eval_eq_pow_of_linearRecurrence
(E : LinearRecurrence ℂ) (G : Fin E.order → ℤ → ℂ)
(hG : ∀ j (n : ℤ), G j (n + E.order) = ∑ i, E.coeffs i * G j (n + (i : ℕ)))
(hind : LinearIndependent ℂ G) :
∃ L : Fin E.order → MvPolynomial (Fin E.order) ℂ, (∀ i, (L i).IsHomogeneous 1) ∧
∀ n : ℤ, MvPolynomial.eval (fun j => G j n) (∏ i, L i) =
((-1) ^ E.order * E.charPoly.coeff 0) ^ n
Sources
- Kálmán Győry, Attila Pethő and László Szalay, Decomposable Forms Generated by Linear Recurrences, Journal of Integer Sequences 27 (2024), Article 24.3.5, Theorem 2 (
jis-2024-24.3.5-thm-2).
TheoremDecomposable forms on consecutive terms of one recurrence sequence#●ready to prove
Let \(\gamma_0, \dots, \gamma_{k-1} \in \mathbb{C}\), let \(\chi(x) = x^k - \sum_{i\lt k} \gamma_i x^i\), and let \(G \colon \mathbb{Z} \to \mathbb{C}\) satisfy \(G_{n+k} = \sum_{i\lt k} \gamma_i G_{n+i}\) for every \(n \in \mathbb{Z}\). Suppose that the \(k\) vectors \((G_j, G_{j+1}, \dots, G_{j+k-1}) \in \mathbb{C}^k\) for \(0 \le j < k\) are linearly independent. Then there are linear forms \(L_1, \dots, L_k\) in \(k\) variables with complex coefficients whose product \(F = L_1 \cdots L_k\) satisfies \(F(G_n, G_{n+1}, \dots, G_{n+k-1}) = ((-1)^k \chi(0))^n\) for every \(n \in \mathbb{Z}\).
For \(k \ge 1\) we have \(\chi(0) = -\gamma_0\), so the right side is \(((-1)^{k+1} \gamma_0)^n\).
public theorem_wanted exists_decomposable_form_eval_shifts_eq_pow
(E : LinearRecurrence ℂ) (G : ℤ → ℂ)
(hG : ∀ n : ℤ, G (n + E.order) = ∑ i, E.coeffs i * G (n + (i : ℕ)))
(hind : LinearIndependent ℂ fun j : Fin E.order => fun i : Fin E.order =>
G ((j : ℕ) + (i : ℕ))) :
∃ L : Fin E.order → MvPolynomial (Fin E.order) ℂ, (∀ i, (L i).IsHomogeneous 1) ∧
∀ n : ℤ, MvPolynomial.eval (fun j : Fin E.order => G (n + (j : ℕ))) (∏ i, L i) =
((-1) ^ E.order * E.charPoly.coeff 0) ^ n
Sources
- Kálmán Győry, Attila Pethő and László Szalay, Decomposable Forms Generated by Linear Recurrences, Journal of Integer Sequences 27 (2024), Article 24.3.5, Corollary 3 (
jis-2024-24.3.5-cor-3).
TheoremAlgebraic dependence of recurrence sequences and a power sequence#●ready to prove
Let \(k\) be a natural number, let \(\gamma_0, \dots, \gamma_{k-1} \in \mathbb{C}\) and let \(\chi(x) = x^k - \sum_{i\lt k} \gamma_i x^i\). Let \(G^{(1)}, \dots, G^{(k)} \colon \mathbb{Z} \to \mathbb{C}\) be sequences such that \(G^{(j)}_{n+k} = \sum_{i\lt k} \gamma_i G^{(j)}_{n+i}\) for every \(j\) and every \(n \in \mathbb{Z}\). Then the family of the \(k + 1\) sequences \(G^{(1)}, \dots, G^{(k)}\) and \(n \mapsto (-\chi(0))^n\) (integer powers, with \(0^n = 0\) for \(n < 0\)) is not algebraically independent over \(\mathbb{C}\) in the \(\mathbb{C}\)-algebra of all sequences \(\mathbb{Z} \to \mathbb{C}\).
For \(k \ge 1\) we have \(\chi(0) = -\gamma_0\), so the last sequence is \(n \mapsto \gamma_0^n\).
public theorem_wanted not_algebraicIndependent_linearRecurrence_solutions_pow
(E : LinearRecurrence ℂ) (G : Fin E.order → ℤ → ℂ)
(hG : ∀ j (n : ℤ), G j (n + E.order) = ∑ i, E.coeffs i * G j (n + (i : ℕ))) :
¬ AlgebraicIndependent ℂ fun o : Option (Fin E.order) =>
o.elim (fun n : ℤ => (-E.charPoly.coeff 0) ^ n) G
Sources
- Kálmán Győry, Attila Pethő and László Szalay, Decomposable Forms Generated by Linear Recurrences, Journal of Integer Sequences 27 (2024), Article 24.3.5, Corollary 4 (
jis-2024-24.3.5-cor-4).
TheoremInteger decomposable forms on integer recurrence sequences#●ready to prove
Let \(\gamma_0, \dots, \gamma_{k-1} \in \mathbb{Z}\), let \(\chi(x) = x^k - \sum_{i\lt k} \gamma_i x^i\), suppose \(\chi(0) \neq 0\), and let \(G^{(1)}, \dots, G^{(k)} \colon \mathbb{N} \to \mathbb{Z}\) each satisfy \(G_{n+k} = \sum_{i\lt k} \gamma_i G_{n+i}\) for every \(n \ge 0\). Suppose that the determinant \(\Delta\) of the \(k \times k\) matrix of initial values \((G^{(j)}_i)\), with rows \(1 \le j \le k\) and columns \(0 \le i < k\), is nonzero. Then there is a polynomial \(\tilde F\) in \(k\) variables with integer coefficients that factors over \(\mathbb{C}\) as a product of \(k\) linear forms and satisfies \(\tilde F(G^{(1)}_n, \dots, G^{(k)}_n) = \Delta^k ((-1)^k \chi(0))^n\) for every \(n \ge 0\).
For \(k \ge 1\) we have \(\chi(0) = -\gamma_0\), so the hypothesis says \(\gamma_0 \neq 0\) and the right side is \(\Delta^k ((-1)^{k+1} \gamma_0)^n\). The theorem in the source says "homogeneous form"; decomposability is the paper's description of \(\tilde F\) in the introduction and follows from Theorem 2, since \(\tilde F\) is \(\Delta^k\) times the form given there. The source's standing assumption \(k \ge 2\) is omitted (for \(k \le 1\) the claim holds with \(\tilde F\) constant or linear); definitions are read from arXiv:2308.13817v1.
public theorem_wanted exists_int_decomposable_form_eval_eq_det_pow_mul_pow
(E : LinearRecurrence ℤ) (G : Fin E.order → ℕ → ℤ) (hG : ∀ j, E.IsSolution (G j))
(hγ : E.charPoly.coeff 0 ≠ 0)
(hΔ : (Matrix.of fun j i : Fin E.order => G j i).det ≠ 0) :
∃ F : MvPolynomial (Fin E.order) ℤ,
(∃ L : Fin E.order → MvPolynomial (Fin E.order) ℂ, (∀ i, (L i).IsHomogeneous 1) ∧
MvPolynomial.map (Int.castRingHom ℂ) F = ∏ i, L i) ∧
∀ n : ℕ, MvPolynomial.eval (fun j => G j n) F =
(Matrix.of fun j i : Fin E.order => G j i).det ^ E.order *
((-1) ^ E.order * E.charPoly.coeff 0) ^ n
Sources
- Kálmán Győry, Attila Pethő and László Szalay, Decomposable Forms Generated by Linear Recurrences, Journal of Integer Sequences 27 (2024), Article 24.3.5, Theorem 6 (
jis-2024-24.3.5-thm-6).
TheoremQuadratic form identity for binary recurrences#●ready to prove
Let \(R\) be a commutative ring, let \(A, B \in R\), and let \((G_n)_{n \ge 0}\) and \((H_n)_{n \ge 0}\) be sequences in \(R\) with \(G_{n+2} = A G_{n+1} + B G_n\) and \(H_{n+2} = A H_{n+1} + B H_n\) for all \(n \ge 0\). Put \(C_G = G_1^2 - A G_0 G_1 - B G_0^2\), \(C_H = H_1^2 - A H_0 H_1 - B H_0^2\), \(E_{10} = G_1 H_1 - A G_1 H_0 - B G_0 H_0\), \(E_{01} = G_1 H_1 - A G_0 H_1 - B G_0 H_0\) and \(\Delta = G_0 H_1 - G_1 H_0\). Then for every \(n \ge 0\),
The source assumes \(\Delta \neq 0\); the identity holds without it, since it is polynomial in the initial values. The notation follows Section 6.1 of arXiv:2308.13817v1.
public theorem_wanted binary_recurrence_quadratic_form_eq_neg_pow_mul_sq {R : Type*} [CommRing R]
(A B : R) (G H : ℕ → R) (hG : ∀ n, G (n + 2) = A * G (n + 1) + B * G n)
(hH : ∀ n, H (n + 2) = A * H (n + 1) + B * H n) (n : ℕ) :
(H 1 ^ 2 - A * H 0 * H 1 - B * H 0 ^ 2) * G n ^ 2 -
((G 1 * H 1 - A * G 1 * H 0 - B * G 0 * H 0) +
(G 1 * H 1 - A * G 0 * H 1 - B * G 0 * H 0)) * G n * H n +
(G 1 ^ 2 - A * G 0 * G 1 - B * G 0 ^ 2) * H n ^ 2 =
(-B) ^ n * (G 0 * H 1 - G 1 * H 0) ^ 2
Sources
- Kálmán Győry, Attila Pethő and László Szalay, Decomposable Forms Generated by Linear Recurrences, Journal of Integer Sequences 27 (2024), Article 24.3.5, Theorem 9 (
jis-2024-24.3.5-thm-9).
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.