Lemma: Agent20_CollatzRound2_01a13459_E20_NativeRank.native_affine_growth_path

For all natural a, the genuine reduced Collatz map satisfies U^8(1024*a+41)=2916*a+121 and every prefix through step 8 is strictly above 1.

Exact formal statement

∀ (a : Nat),
  And
    (Eq.{1}
      (Agent20_CollatzRound2_01a13459_E20_NativeRank.Core.iter (HAdd.hAdd.{0, 0, 0} (HMul.hMul.{0, 0, 0} 1024 a) 41) 8)
      (HAdd.hAdd.{0, 0, 0} (HMul.hMul.{0, 0, 0} 2916 a) 121))
    (∀ (j : Nat),
      LE.le.{0} j 8 →
        LT.lt.{0} 1
          (Agent20_CollatzRound2_01a13459_E20_NativeRank.Core.iter (HAdd.hAdd.{0, 0, 0} (HMul.hMul.{0, 0, 0} 1024 a) 41)
            j))

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

Environment availability: available.

Public JSON record