Lemma: Agent20_CollatzRound2_01a13459_E20_V2.reverse_class_29

For every natural a, U^14(16384*a+6847)=19683*a+8227, and the input is positive and smaller than the output. Hence this image residue class cannot contain a minimal positive counterexample. No novelty or full-target solve is claimed.

Exact formal statement

∀ (a : Nat),
  And
    (Eq.{1}
      (Agent20_CollatzRound2_01a13459_E20_V2.Core.iter (HAdd.hAdd.{0, 0, 0} 6847 (HMul.hMul.{0, 0, 0} 16384 a)) 14)
      (HAdd.hAdd.{0, 0, 0} 8227 (HMul.hMul.{0, 0, 0} 19683 a)))
    (And (LT.lt.{0} 0 (HAdd.hAdd.{0, 0, 0} 6847 (HMul.hMul.{0, 0, 0} 16384 a)))
      (LT.lt.{0} (HAdd.hAdd.{0, 0, 0} 6847 (HMul.hMul.{0, 0, 0} 16384 a))
        (HAdd.hAdd.{0, 0, 0} 8227 (HMul.hMul.{0, 0, 0} 19683 a))))

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

Environment availability: available.

Public JSON record