Lemma: Agent20_CollatzRound2_01a13459_E20_Rewrite.shorter_witness_of_meeting

If U^k(n)=U^ell(w), ell<k<=K, and U^K(n)=1, then w has a 1-hitting witness J<K. This is an explicit conditional transfer of finite witnesses, not universal existence of K.

Exact formal statement

∀ (n w k ell K : Nat),
  LE.le.{0} k K →
    LT.lt.{0} ell k →
      Eq.{1} (Agent20_CollatzRound2_01a13459_E20_Rewrite.Core.iter n k)
          (Agent20_CollatzRound2_01a13459_E20_Rewrite.Core.iter w ell) →
        Eq.{1} (Agent20_CollatzRound2_01a13459_E20_Rewrite.Core.iter n K) 1 →
          Exists.{1} fun J => And (LT.lt.{0} J K) (Eq.{1} (Agent20_CollatzRound2_01a13459_E20_Rewrite.Core.iter w J) 1)

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

Environment availability: available.

Public JSON record