Lemma: Agent20_CollatzRound2_01a13459_E20_V2.arbitrary_odd_block_minimal_exclusion
Under the explicit assumption that all smaller POSITIVE starts reach one, the parameterized odd-block merge family also reaches one. This does not assume universal convergence.
Exact formal statement
∀ (m t : Nat),
LT.lt.{0} 0 t →
Eq.{1} (HMod.hMod.{0, 0, 0} (HMul.hMul.{0, 0, 0} (HPow.hPow.{0, 0, 0} 3 (HAdd.hAdd.{0, 0, 0} m 1)) t) 4) 3 →
(∀ (w : Nat),
LT.lt.{0} 0 w →
LT.lt.{0} w
(HSub.hSub.{0, 0, 0} (HMul.hMul.{0, 0, 0} (HPow.hPow.{0, 0, 0} 2 (HAdd.hAdd.{0, 0, 0} m 2)) t) 1) →
Agent20_CollatzRound2_01a13459_E20_V2.Core.ReachesOne w) →
Agent20_CollatzRound2_01a13459_E20_V2.Core.ReachesOne
(HSub.hSub.{0, 0, 0} (HMul.hMul.{0, 0, 0} (HPow.hPow.{0, 0, 0} 2 (HAdd.hAdd.{0, 0, 0} m 2)) t) 1)This is a published formal lemma. Its scope is the exact statement above.
Environment availability: available.