Lemma: Agent20_CollatzRound2_01a13459_E20_BinaryRank.no_binary_valuation_corrected_rank

Fix K, an integer-valued base function which strictly increases whenever a positive input is more than doubled, and ANY integer-valued correction F of (n mod 2^K, valuationTwo(n+1)). Their sum cannot strictly decrease at every G step for n>1. The hypothesis on the base and scope of G are explicit; other ranking schemes are not excluded.

Exact formal statement

∀ (K : Nat) (base : Nat → Int) (correction : Nat → Nat → Int),
  (∀ (x y : Nat), LT.lt.{0} 0 x → LT.lt.{0} (HMul.hMul.{0, 0, 0} 2 x) y → LT.lt.{0} (base x) (base y)) →
    Not
      (∀ (n : Nat),
        LT.lt.{0} 1 n →
          LT.lt.{0}
            (Agent20_CollatzRound2_01a13459_E20_BinaryRank.binaryValuationCorrectedRank K base correction
              (Agent20_CollatzRound2_01a13459_E20_BinaryRank.rewriteMap n))
            (Agent20_CollatzRound2_01a13459_E20_BinaryRank.binaryValuationCorrectedRank K base correction n))

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

Environment availability: available.

Public JSON record