Lemma: Agent20_CollatzRound2_01a13459_E20_Rewrite.no_trailing_correction_for_rewrite

For every integer-valued function f on naturals, V(n)=floor(log2(n+1))+f(valuationTwo(n+1)) fails to strictly decrease at every G step on n>1. ValuationTwo is the recursively defined power-of-two valuation; G is the explicitly defined orbit-block rewrite. Does not rule out other potentials or variable-block decreases.

Exact formal statement

∀ (f : Nat → Int),
  Not
    (∀ (n : Nat),
      LT.lt.{0} 1 n →
        LT.lt.{0}
          (Agent20_CollatzRound2_01a13459_E20_Rewrite.trailingCorrectedRank f
            (Agent20_CollatzRound2_01a13459_E20_Rewrite.rewriteMap n))
          (Agent20_CollatzRound2_01a13459_E20_Rewrite.trailingCorrectedRank f n))

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

Environment availability: available.

Public JSON record