Lemma: Agent20_CollatzPartial_01a13459_E20_Parity.no_descent_forces_many_odd_steps

For any natural n>=6 and k>0, if U^j(n)>=n for EVERY j<=k, then 3*k<5*oddCount(n,k). This is a deterministic necessary condition for a non-descending prefix, not a theorem that every orbit descends.

Exact formal statement

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

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

Environment availability: available.

Public JSON record