Lemma: Agent20_CollatzRound2_01a13459_E20_V2.no_one_odd_cycle_above_one

No positive exponent a and integer minimum x>=2 satisfy 2^a*x=3*x+1. A scoped one-odd-vertex cycle exclusion.

Exact formal statement

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

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

Environment availability: available.

Public JSON record