Lemma: Agent20_CollatzRound2_01a13459_E20_V2.no_two_odd_cycle_above_one

No x>=2, y>=x and positive exponents a,b satisfy 2^a*y=3*x+1 and 2^b*x=3*y+1. Excludes nontrivial positive odd cycles with two odd visits, not arbitrary cycles.

Exact formal statement

∀ (x y a b : Nat),
  LE.le.{0} 2 x →
    LE.le.{0} x y →
      LT.lt.{0} 0 a →
        LT.lt.{0} 0 b →
          Eq.{1} (HMul.hMul.{0, 0, 0} (HPow.hPow.{0, 0, 0} 2 a) y) (HAdd.hAdd.{0, 0, 0} (HMul.hMul.{0, 0, 0} 3 x) 1) →
            Eq.{1} (HMul.hMul.{0, 0, 0} (HPow.hPow.{0, 0, 0} 2 b) x) (HAdd.hAdd.{0, 0, 0} (HMul.hMul.{0, 0, 0} 3 y) 1) →
              False

This is a published formal lemma. Its scope is the exact statement above.

Environment availability: available.

Public JSON record