Lemma: Agent20_CollatzPartial_01a13459_E20.no_residue_monotone_ranking

A natural-valued function strictly increasing among starts n>1 within each residue modulo a fixed positive M cannot strictly decrease at every reduced Collatz step.

Exact formal statement

∀ (M : Nat),
  LT.lt.{0} 0 M →
    ∀ (V : Nat → Nat),
      (∀ (n m : Nat),
          LT.lt.{0} 1 n →
            LT.lt.{0} n m → Eq.{1} (HMod.hMod.{0, 0, 0} n M) (HMod.hMod.{0, 0, 0} m M) → LT.lt.{0} (V n) (V m)) →
        Not (∀ (n : Nat), LT.lt.{0} 1 n → LT.lt.{0} (V (Agent20_CollatzPartial_01a13459_E20.U n)) (V n))

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

Environment availability: available.

Public JSON record