Lemma: Agent20_CollatzPartial_01a13459_E20.affine_lift

For the locally defined reduced Collatz map U, iter(n+2^k*t,k)=iter(n,k)+coeff(n,k)*t for all natural k,n,t. Coeff is the product of 1/3 parity factors.

Exact formal statement

∀ (k n t : Nat),
  Eq.{1}
    (Agent20_CollatzPartial_01a13459_E20.iter (HAdd.hAdd.{0, 0, 0} n (HMul.hMul.{0, 0, 0} (HPow.hPow.{0, 0, 0} 2 k) t))
      k)
    (HAdd.hAdd.{0, 0, 0} (Agent20_CollatzPartial_01a13459_E20.iter n k)
      (HMul.hMul.{0, 0, 0} (Agent20_CollatzPartial_01a13459_E20.coeff n k) t))

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

Environment availability: available.

Public JSON record