Compfiles/Imo1988P6.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem Imo1988P6.constant_descent_vieta_jumping Constant descent Vieta jumping line 79 source

   Source documentation

   Constant descent Vieta jumping.

   This proof technique allows one to prove an arbitrary proposition claim, by running a descent argument on a hyperbola H in the first quadrant of the plane, under the following conditions:

   • h₀ : There exists an integral point (x,y) on the hyperbola H.
   • H_symm : The hyperbola has a symmetry along the diagonal in the plane.
   • H_zero : If an integral point (x,0) lies on the hyperbola H, then claim is true.
   • H_diag : If an integral point (x,x) lies on the hyperbola H, then claim is true.
   • H_desc : If (x,y) is an integral point on the hyperbola H, with x < y then there exists a “smaller” point on H: a point (x',y') with x' < y' ≤ x.

   For reasons of usability, the hyperbola H is implemented as an arbitrary predicate. (In question 6 of IMO1988, where this proof technique was first developped, the predicate claim would be ∃ (d : ℕ), d ^ 2 = k for some natural number k, and the predicate H would be fun a b ↦ a * a + b * b = (a * b + 1) * k.)

   To ensure that the predicate H actually describes a hyperbola, the user must provide arguments B and C that are used as coefficients for a quadratic equation. Finally, H_quad is the proof obligation that the quadratic equation (y:ℤ) * y - B x * y + C x = 0 describes the same hyperbola as the predicate H.

   For extra flexibility, one must provide a predicate base on the integral points in the plane. In the descent step H_desc this will give the user the additional assumption that the point (x,y) does not lie in this base locus. The user must provide a proof that the proposition claim is true if there exists an integral point (x,y) on the hyperbola H that lies in the base locus. If such a base locus is not necessary, once can simply let it be fun x y ↦ False.

   L4DEL explanation

   Constant descent Vieta jumping. This proof technique allows one to prove an arbitrary proposition claim, by running a descent argument on a hyperbola H in the first quadrant of the plane, under the following conditions: * h₀ : There exists an integral point (x,y) on the hyperbola H. * H_symm : The hyperbola has a symmetry along the diagonal in the plane. * H_zero : If an integral point (x,0) lies on the hyperbola H, then claim is true. * H_diag : If an integral point (x,x) lies on the hyperbola H, then claim is true. * H_desc : If (x,y) is an integral point on the hyperbola H, with x < y then there exists a “smaller” point on H: a point (x',y') with x' < y' ≤ x. For reasons of usability, the hyperbola H is implemented as an arbitrary predicate. (In question 6 of IMO1988, where this proof technique was first developped, the predicate claim would be ∃ (d : ℕ), d ^ 2 = k for some natural number k, and the predicate H would be fun a b ↦ a * a + b * b = (a * b + 1) * k.) To ensure that the predicate H actually describes a hyperbola, the user must provide arguments B and C that are used as coefficients for a quadratic equation. Finally, H_quad is the proof obligation that the quadratic equation (y:ℤ) * y - B x * y + C x = 0 describes the same hyperbola as the predicate H. For extra flexibility, one must provide a predicate base on the integral points in the plane. In the descent step H_desc this will give the user the additional assumption that the point (x,y) does not lie in this base locus. The user must provide a proof that the proposition claim is true if there exists an integral point (x,y) on the hyperbola H that lies in the base locus.

   Sources and attribution: Pinned Lean source (47b19bbfe5f3)

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Nat, Int, Iff, Eq, HAdd.hAdd, HSub.hSub, HMul.hMul, OfNat.ofNat, LT.lt, Not, And, LE.le

   Proof uses: Or, Classical.em, dite, lt_of_le_of_ne, Set, Prod, Set.ofPred, Prod.fst, Prod.snd, Prod.mk, Membership.mem, And.intro, Set.image, SDiff.sdiff, Set.Nonempty, Eq.mpr, Ne, EmptyCollection.emptyCollection, id, congrArg and 28 more

   78 instances, coercions and auxiliary constants left out.

   Tactic trace: 75 steps

   Open to load the checked before-and-after goal states.

   theorem constant_descent_vieta_jumping (x y : ℕ) {claim : Prop} {H : ℕ → ℕ → Prop} (h₀ : H x y)
       (B : ℕ → ℤ) (C : ℕ → ℤ) (base : ℕ → ℕ → Prop)
       (H_quad : ∀ {x y}, H x y ↔ (y : ℤ) * y - B x * y + C x = 0) (H_symm : ∀ {x y}, H x y ↔ H y x)
       (H_zero : ∀ {x}, H x 0 → claim) (H_diag : ∀ {x}, H x x → claim)
       (H_desc : ∀ {x y}, 0 < x → x < y → ¬base x y → H x y →
         ∀ y', y' * y' - B x * y' + C x = 0 → y' = B x - y → y' * y = C x → 0 ≤ y' ∧ y' ≤ x)
       (H_base : ∀ {x y}, H x y → base x y → claim) : claim := by
   …

   Mentions: base

2. problem Imo1988P6.imo1988_p6 IMO 1988 Problem 6: Vieta jumping line 201 source

   L4DEL explanation

   If ab+1 divides a^2+b^2 for natural numbers a and b, then the quotient is a perfect square.

   1. Problem: given natural a, b with (ab+1) dividing a^2 + b^2, show the quotient (a^2+b^2)/(ab+1) is a perfect square. The formal conclusion is exists d, d^2 = (a^2+b^2)/(ab+1).
   2. Solution (complete, no sorry): call the quotient k, so a^2 + b^2 = (ab+1)k. For fixed a this is a quadratic in b, whose other root is k*a - b.
   3. The file proves a general lemma, constant_descent_vieta_jumping, that runs a descent on such a hyperbola, and applies it with B x = k * x and C x = x * x - k.
   4. The base cases are b = 0 (then k = a^2) and a = b (then k is at most 1, so k is 0 or 1); the descent step produces a smaller solution.

   Prerequisites: Imo1988P6.constant_descent_vieta_jumping

   Sources and attribution: Pinned Lean source (47b19bbfe5f3)

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Nat, Dvd.dvd, HAdd.hAdd, HMul.hMul, OfNat.ofNat, HPow.hPow, Exists, Eq, HDiv.hDiv

   Proof uses: Eq.mpr, id, congrArg, Nat.succ, Nat.mul_div_cancel_left, Nat.succ_pos, Imo1988P6.constant_descent_vieta_jumping, Eq.mp, congrFun', congr, sq, Int, HSub.hSub, False, of_eq_true, Iff, Eq.trans, True, mul_comm, add_comm and 107 more

   154 instances, coercions and auxiliary constants left out.

   Vieta jumping: a descent technique for integer solutions of a quadratic equation in two variables: given one solution, the second root of the quadratic (by Vieta's formulas) gives another, smaller solution, until a base case is reached.

   Tactic trace: 113 steps

   Open to load the checked before-and-after goal states.

   problem imo1988_p6 {a b : ℕ} (h : a * b + 1 ∣ a ^ 2 + b ^ 2) :
       ∃ d, d ^ 2 = (a ^ 2 + b ^ 2) / (a * b + 1) := by
   …

   Mentions: h

3. example Imo1988P6.(example at line 259) line 259 source

   Source comment

   The following example illustrates the use of constant descent Vieta jumping in the presence of a non-trivial base case.

   example {a b : ℕ} (h : a * b ∣ a ^ 2 + b ^ 2 + 1) : 3 * a * b = a ^ 2 + b ^ 2 + 1 := by
   …

   Mentions: h