Lemma: Agent20_CollatzRound2_01a13459_E20_NativeRank.strict_decay_along_positive_path

If an integer-valued V strictly decreases at every U step from an input above 1, then it strictly decreases along any positive-length path whose inputs before the last step all exceed 1. Explicit finite-path hypotheses.

Exact formal statement

∀ (V : Nat → Int) (n k : Nat),
  LT.lt.{0} 0 k →
    (∀ (j : Nat), LT.lt.{0} j k → LT.lt.{0} 1 (Agent20_CollatzRound2_01a13459_E20_NativeRank.Core.iter n j)) →
      (∀ (x : Nat), LT.lt.{0} 1 x → LT.lt.{0} (V (Agent20_CollatzRound2_01a13459_E20_NativeRank.Core.U x)) (V x)) →
        LT.lt.{0} (V (Agent20_CollatzRound2_01a13459_E20_NativeRank.Core.iter n k)) (V n)

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

Environment availability: available.

Public JSON record