Lemma: Agent20_CollatzRound2_01a13459_E20_V2.no_three_odd_cycle_above_one

No x>=2, y,z>=x and positive exponents a,b,c satisfy the three equations 2^a*y=3*x+1, 2^b*z=3*y+1, 2^c*x=3*z+1. Excludes the scoped three-odd-visit case only.

Exact formal statement

∀ (x y z a b c : Nat),
  LE.le.{0} 2 x →
    LE.le.{0} x y →
      LE.le.{0} x z →
        LT.lt.{0} 0 a →
          LT.lt.{0} 0 b →
            LT.lt.{0} 0 c →
              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) z)
                    (HAdd.hAdd.{0, 0, 0} (HMul.hMul.{0, 0, 0} 3 y) 1) →
                  Eq.{1} (HMul.hMul.{0, 0, 0} (HPow.hPow.{0, 0, 0} 2 c) x)
                      (HAdd.hAdd.{0, 0, 0} (HMul.hMul.{0, 0, 0} 3 z) 1) →
                    False

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

Environment availability: available.

Public JSON record