Lemma: Agent20_CollatzPartial_01a13459_E20.merge_family_converges_from_smaller

If every smaller POSITIVE start reaches 1 under the local reduced map U, then 64*a+15 reaches 1. This is a conditional minimal-counterexample lemma, not universal convergence.

Exact formal statement

∀ (a : Nat),
  (∀ (m : Nat),
      LT.lt.{0} 0 m →
        LT.lt.{0} m (HAdd.hAdd.{0, 0, 0} (HMul.hMul.{0, 0, 0} 64 a) 15) →
          Agent20_CollatzPartial_01a13459_E20.ReachesOne m) →
    Agent20_CollatzPartial_01a13459_E20.ReachesOne (HAdd.hAdd.{0, 0, 0} (HMul.hMul.{0, 0, 0} 64 a) 15)

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

Environment availability: available.

Public JSON record