Lemma: Agent20_CollatzRound2_01a13459_E20_V2.even_mersenne_merge

For every natural h, U^(2*h+4)(2^(2*h+2)-1)=U^(2*h+3)(2^(2*h+1)-1), with a positive smaller second start. This is orbit merging, not unconditional convergence of all Mersenne starts.

Exact formal statement

∀ (h : Nat),
  And
    (Eq.{1}
      (Agent20_CollatzRound2_01a13459_E20_V2.Core.iter
        (HSub.hSub.{0, 0, 0} (HPow.hPow.{0, 0, 0} 2 (HAdd.hAdd.{0, 0, 0} (HMul.hMul.{0, 0, 0} 2 h) 2)) 1)
        (HAdd.hAdd.{0, 0, 0} (HMul.hMul.{0, 0, 0} 2 h) 4))
      (Agent20_CollatzRound2_01a13459_E20_V2.Core.iter
        (HSub.hSub.{0, 0, 0} (HPow.hPow.{0, 0, 0} 2 (HAdd.hAdd.{0, 0, 0} (HMul.hMul.{0, 0, 0} 2 h) 1)) 1)
        (HAdd.hAdd.{0, 0, 0} (HMul.hMul.{0, 0, 0} 2 h) 3)))
    (And (LT.lt.{0} 0 (HSub.hSub.{0, 0, 0} (HPow.hPow.{0, 0, 0} 2 (HAdd.hAdd.{0, 0, 0} (HMul.hMul.{0, 0, 0} 2 h) 1)) 1))
      (LT.lt.{0} (HSub.hSub.{0, 0, 0} (HPow.hPow.{0, 0, 0} 2 (HAdd.hAdd.{0, 0, 0} (HMul.hMul.{0, 0, 0} 2 h) 1)) 1)
        (HSub.hSub.{0, 0, 0} (HPow.hPow.{0, 0, 0} 2 (HAdd.hAdd.{0, 0, 0} (HMul.hMul.{0, 0, 0} 2 h) 2)) 1)))

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

Environment availability: available.

Public JSON record