Lemma: Agent20_CollatzRound2_01a13459_E20_NativeRank.no_binary_valuation_corrected_rank_native

For every fixed binary modulus 2^K, integer-valued base increasing when positive input size more than doubles, and ANY integer-valued correction of (n mod 2^K, valuationTwo(n+1)), their sum cannot decrease at every genuine U step for n>1. An additive static-feature ranking exclusion, not a counterexample to Collatz or an exclusion of all termination proofs.

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_NativeRank.binaryValuationCorrectedRank K base correction
              (Agent20_CollatzRound2_01a13459_E20_NativeRank.Core.U n))
            (Agent20_CollatzRound2_01a13459_E20_NativeRank.binaryValuationCorrectedRank K base correction n))

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

Environment availability: available.

Public JSON record