Lemma: Agent20_CollatzPartial_01a13459_E20_Parity.coeff_eq_pow_oddCount

For the local reduced Collatz map U, the affine lifting coefficient equals 3 raised to the number of odd inputs among the first k steps.

Exact formal statement

∀ (n k : Nat),
  Eq.{1} (Agent20_CollatzPartial_01a13459_E20_Parity.coeff n k)
    (HPow.hPow.{0, 0, 0} 3 (Agent20_CollatzPartial_01a13459_E20_Parity.oddCount n k))

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

Environment availability: available.

Public JSON record