From daa3e6fa32d4be90ddecfedcc336b41ac9a889ab Mon Sep 17 00:00:00 2001 From: Oliver Nash Date: Thu, 24 Oct 2024 14:44:22 +0000 Subject: [PATCH] Fix 2017 A2 This was disprovable because of division-by-zero silliness. The fix is to guard `Q n x` to be non-zero in `hQn` (an alternative would be to rewrite the quotient as a multiplication). I have included some other minor style improvements which are unrelated. --- lean4/src/putnam_2017_a2.lean | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/lean4/src/putnam_2017_a2.lean b/lean4/src/putnam_2017_a2.lean index ec3b697b..35a5fa43 100644 --- a/lean4/src/putnam_2017_a2.lean +++ b/lean4/src/putnam_2017_a2.lean @@ -1,11 +1,14 @@ import Mathlib +open Polynomial + /-- Let $Q_0(x)=1$, $Q_1(x)=x$, and $Q_n(x)=\frac{(Q_{n-1}(x))^2-1}{Q_{n-2}(x)}$ for all $n \geq 2$. Show that, whenever $n$ is a positive integer, $Q_n(x)$ is equal to a polynomial with integer coefficients. -/ theorem putnam_2017_a2 -(Q : ℕ → ℝ → ℝ) -(hQbase : ∀ x : ℝ, Q 0 x = 1 ∧ Q 1 x = x) -(hQn : ∀ n ≥ 2, ∀ x : ℝ, Q n x = ((Q (n - 1) x) ^ 2 - 1) / Q (n - 2) x) -: ∀ n > 0, ∃ P : Polynomial ℝ, (∀ i : ℕ, P.coeff i = round (P.coeff i)) ∧ Q n = P.eval := -sorry + (Q : ℕ → RatFunc ℚ) + (hQbase : Q 0 = 1 ∧ Q 1 = (X : ℚ[X])) + (hQn : ∀ n, Q (n + 2) = (Q (n + 1) ^ 2 - 1) / Q n) + (n : ℕ) (hn : 0 < n) : + ∃ P : ℤ[X], Q n = P.map (Int.castRingHom ℚ) := + sorry