Lemma: Agent20_CollatzRound2_01a13459_E20_BinaryRank.growing_same_binary_state

For every natural K there is a natural a such that 1024*a+41 and 2916*a+121 are congruent modulo 2^K. Combined with the separate affine growth lemma, this is a returning-feature growth certificate, not an actual orbit cycle.

Exact formal statement

∀ (K : Nat),
  Exists.{1} fun a =>
    Eq.{1} (HMod.hMod.{0, 0, 0} (HAdd.hAdd.{0, 0, 0} (HMul.hMul.{0, 0, 0} 1024 a) 41) (HPow.hPow.{0, 0, 0} 2 K))
      (HMod.hMod.{0, 0, 0} (HAdd.hAdd.{0, 0, 0} (HMul.hMul.{0, 0, 0} 2916 a) 121) (HPow.hPow.{0, 0, 0} 2 K))

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

Environment availability: available.

Public JSON record