Lemma: Agent20_CollatzRound2_01a13459_E20_BinaryRank.rewrite_affine_growth

For all natural a, G(1024*a+41)=768*a+31 and G(768*a+31)=2916*a+121. Both endpoints have valuationTwo(n+1)=1, and the last endpoint exceeds twice the first. G is the explicitly defined block rewrite map.

Exact formal statement

∀ (a : Nat),
  And
    (Eq.{1}
      (Agent20_CollatzRound2_01a13459_E20_BinaryRank.rewriteMap (HAdd.hAdd.{0, 0, 0} (HMul.hMul.{0, 0, 0} 1024 a) 41))
      (HAdd.hAdd.{0, 0, 0} (HMul.hMul.{0, 0, 0} 768 a) 31))
    (And
      (Eq.{1}
        (Agent20_CollatzRound2_01a13459_E20_BinaryRank.rewriteMap (HAdd.hAdd.{0, 0, 0} (HMul.hMul.{0, 0, 0} 768 a) 31))
        (HAdd.hAdd.{0, 0, 0} (HMul.hMul.{0, 0, 0} 2916 a) 121))
      (And
        (Eq.{1}
          (Agent20_CollatzRound2_01a13459_E20_BinaryRank.valuationTwo
            (HAdd.hAdd.{0, 0, 0} (HAdd.hAdd.{0, 0, 0} (HMul.hMul.{0, 0, 0} 1024 a) 41) 1))
          1)
        (And
          (Eq.{1}
            (Agent20_CollatzRound2_01a13459_E20_BinaryRank.valuationTwo
              (HAdd.hAdd.{0, 0, 0} (HAdd.hAdd.{0, 0, 0} (HMul.hMul.{0, 0, 0} 2916 a) 121) 1))
            1)
          (LT.lt.{0} (HMul.hMul.{0, 0, 0} 2 (HAdd.hAdd.{0, 0, 0} (HMul.hMul.{0, 0, 0} 1024 a) 41))
            (HAdd.hAdd.{0, 0, 0} (HMul.hMul.{0, 0, 0} 2916 a) 121)))))

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

Environment availability: available.

Public JSON record