Documentation

Archive.Imo.Imo2024Q2

IMO 2024 Q2 #

Determine all pairs $(a,b)$ of positive integers for which there exist positive integers $g$ and $N$ such that [ \gcd(a^n + b, b^n + a) = g ] holds for all integers $n \ge N$.

We consider the sequence modulo ab+1; if the exponent is -1 modulo φ(ab+1), the terms are zero modulo ab+1, so ab+1 divides g, and all sufficiently large terms, so all terms, from which we conclude that a=b=1.

def Imo2024Q2.Condition (a : ) (b : ) :

The condition of the problem.

Equations
Instances For
    theorem Imo2024Q2.dvd_pow_iff_of_dvd_sub {a : } {b : } {d : } {n : } {z : } (ha : a.Coprime d) (hd : d.totient n - z) :
    d a ^ n + b (ZMod.unitOfCoprime a ha ^ z) + b = 0
    theorem Imo2024Q2.Condition.a_pos {a : } {b : } (h : Imo2024Q2.Condition a b) :
    0 < a
    theorem Imo2024Q2.Condition.b_pos {a : } {b : } (h : Imo2024Q2.Condition a b) :
    0 < b
    noncomputable def Imo2024Q2.Condition.g {a : } {b : } (h : Imo2024Q2.Condition a b) :

    The value of g in the problem (determined by a and b).

    Equations
    • h.g = .choose
    Instances For
      theorem Imo2024Q2.Condition.g_spec {a : } {b : } (h : Imo2024Q2.Condition a b) :
      ∃ (N : ), 0 < h.g 0 < N ∀ (n : ), N n(a ^ n + b).gcd (b ^ n + a) = h.g
      noncomputable def Imo2024Q2.Condition.N {a : } {b : } (h : Imo2024Q2.Condition a b) :

      The value of N in the problem (any sufficiently large value).

      Equations
      • h.N = .choose
      Instances For
        theorem Imo2024Q2.Condition.N_spec {a : } {b : } (h : Imo2024Q2.Condition a b) :
        0 < h.g 0 < h.N ∀ (n : ), h.N n(a ^ n + b).gcd (b ^ n + a) = h.g
        theorem Imo2024Q2.Condition.g_pos {a : } {b : } (h : Imo2024Q2.Condition a b) :
        0 < h.g
        theorem Imo2024Q2.Condition.N_pos {a : } {b : } (h : Imo2024Q2.Condition a b) :
        0 < h.N
        theorem Imo2024Q2.Condition.gcd_eq_g {a : } {b : } (h : Imo2024Q2.Condition a b) {n : } (hn : h.N n) :
        (a ^ n + b).gcd (b ^ n + a) = h.g
        theorem Imo2024Q2.Condition.dvd_g_of_le_N_of_dvd {a : } {b : } (h : Imo2024Q2.Condition a b) {n : } (hn : h.N n) {d : } (hab : d a ^ n + b) (hba : d b ^ n + a) :
        d h.g
        theorem Imo2024Q2.Condition.a_coprime_ab_add_one {a : } {b : } :
        a.Coprime (a * b + 1)
        noncomputable def Imo2024Q2.Condition.large_n {a : } {b : } (h : Imo2024Q2.Condition a b) :

        A sufficiently large value of n, congruent to -1 mod φ (a * b + 1).

        Equations
        • h.large_n = (max h.N .N + 1) * (a * b + 1).totient - 1
        Instances For
          theorem Imo2024Q2.Condition.symm_large_n {a : } {b : } (h : Imo2024Q2.Condition a b) :
          .large_n = h.large_n
          theorem Imo2024Q2.Condition.N_le_large_n {a : } {b : } (h : Imo2024Q2.Condition a b) :
          h.N h.large_n
          theorem Imo2024Q2.Condition.dvd_large_n_sub_neg_one {a : } {b : } (h : Imo2024Q2.Condition a b) :
          (a * b + 1).totient h.large_n - -1
          noncomputable def Imo2024Q2.Condition.large_n_0 {a : } {b : } (h : Imo2024Q2.Condition a b) :

          A sufficiently large value of n, congruent to 0 mod φ (a * b + 1).

          Equations
          • h.large_n_0 = max h.N .N * (a * b + 1).totient
          Instances For
            theorem Imo2024Q2.Condition.symm_large_n_0 {a : } {b : } (h : Imo2024Q2.Condition a b) :
            .large_n_0 = h.large_n_0
            theorem Imo2024Q2.Condition.N_le_large_n_0 {a : } {b : } (h : Imo2024Q2.Condition a b) :
            h.N h.large_n_0
            theorem Imo2024Q2.Condition.dvd_large_n_0_sub_zero {a : } {b : } (h : Imo2024Q2.Condition a b) :
            (a * b + 1).totient h.large_n_0 - 0

            This is to be determined by the solver of the original problem.

            Equations
            Instances For