Powers of two in binary

The binary digits of 2 ^ n, least significant first, are n zeros followed by a one (Turing.MultiTapeTM.encNat_two_pow). So an exponential clock 2 ^ n is written in linear time, by a transducer replacing every symbol of a word of length n by false and appending true, without ever writing 2 ^ n in unary.

Main results

• Turing.MultiTapeTM.encNat_two_pow: the binary digits of 2 ^ n.
• Turing.MultiTapeTM.ComputableTidilyInDegree.two_pow_length: 2 ^ (encIn a).length is linear.

theorem Turing.MultiTapeTM.encNat_two_pow (n : ℕ) : encNat (2 ^ n) = List.replicate n false ++ [true]

The binary digits of 2 ^ n, least significant first: n zeros followed by a one.

def Turing.MultiTapeTM.twoPowT : Transducer Bool Unit

Replaces every symbol by false and appends true.

theorem Turing.MultiTapeTM.twoPowT_run (w : List Bool) : twoPowT.run () w = List.replicate w.length false ++ [true]

theorem Turing.MultiTapeTM.ComputableTidilyInDegree.two_pow_length {α : Type u_1} (encIn : α ↪ List Bool) : ComputableTidilyInDegree (fun (a : α) => 2 ^ (encIn a).length) encIn encNat 1 1

An exponential clock in binary. 2 ^ (encIn a).length is tidily computable in linear time and space, for every encoding of the input.