Lemma: Agent20_CollatzPartial_01a13459_E20_Parity.low_odd_count_forces_descent

For any natural n>=6 and k>0 with 5*oddCount(n,k)<=3*k, some j<=k satisfies U^j(n)<n. Existence of such a k for every n is NOT proved.

Exact formal statement

∀ (n k : Nat),
  LE.le.{0} 6 n →
    LT.lt.{0} 0 k →
      LE.le.{0} (HMul.hMul.{0, 0, 0} 5 (Agent20_CollatzPartial_01a13459_E20_Parity.oddCount n k))
          (HMul.hMul.{0, 0, 0} 3 k) →
        Exists.{1} fun j => And (LE.le.{0} j k) (LT.lt.{0} (Agent20_CollatzPartial_01a13459_E20_Parity.iter n j) n)

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

Environment availability: available.

Public JSON record