Lemma: Agent20_CollatzRound2_01a13459_E20_V2.no_smaller_ancestor_for_multiple_three

If N is divisible by 3 and U^k(w)=N, then N<=w. Thus pure smaller-ancestor induction cannot cover positive multiples of three.

Exact formal statement

∀ (N w k : Nat),
  Eq.{1} (HMod.hMod.{0, 0, 0} N 3) 0 → Eq.{1} (Agent20_CollatzRound2_01a13459_E20_V2.Core.iter w k) N → LE.le.{0} N w

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

Environment availability: available.