Binary codes of numbers in polynomial time

Converting between a number written in unary, which is how Complexitylib.Classes.P.Unary writes a polynomial-time number, and the same number written in binary, least significant bit first, as Nat.toBitsLE, Nat.fromBitsLE and Nat.bits do.

Writing binary is polynomial-time without any side condition. The width-w expansion of n (toBitsLE_mem_FP) lists bit i of n at position i (toBitsLE_eq_map_range), and each bit is a polynomial-time test on i. The minimal expansion Nat.bits n (bits_mem_FP) is the expansion at width Nat.size n.

Reading binary can only be polynomial-time up to a cap, because a numeral of k bits can denote a number near 2 ^ k, far too large to write in unary. The value capped at a polynomial-time number is polynomial-time (UnaryFn.fromBitsLE_min), and so is the value itself when the cap is known not to bind (UnaryFn.fromBitsLE_of_le).

Main results

• toBitsLE_eq_map_range — the fixed-width expansion, bit by bit
• toBitsLE_mem_FP — writing a fixed-width expansion is polynomial-time
• bits_mem_FP, bits_length_mem_FP — writing the minimal expansion is polynomial-time
• UnaryFn.fromBitsLE_min, UnaryFn.fromBitsLE_of_le — reading a numeral back, below a cap, is polynomial-time

Writing binary

theorem Complexity.toBitsLE_eq_map_range (w v : ℕ) : w.toBitsLE v = List.map (fun (i : ℕ) => decide (v / 2 ^ i % 2 = 1)) (List.range w)

The fixed-width expansion, bit by bit. Position i of the width-w little-endian expansion of v holds bit i of v.

theorem Complexity.toBitsLE_mem_FP {w n : List Bool → ℕ} (hw : UnaryFn w) (hn : UnaryFn n) : (fun (z : List Bool) => (w z).toBitsLE (n z)) ∈ FP

Writing a fixed-width expansion is polynomial-time. If w and n are polynomial-time numbers, then so is writing the low w z bits of n z, least significant first.

theorem Complexity.bits_mem_FP {n : List Bool → ℕ} (hn : UnaryFn n) : (fun (z : List Bool) => (n z).bits) ∈ FP

Writing the minimal expansion is polynomial-time: Nat.bits of a polynomial-time number, the expansion with no trailing zero.

theorem Complexity.bits_length_mem_FP : (fun (z : List Bool) => z.length.bits) ∈ FP

The input length, in binary, is polynomial-time.

Reading binary

theorem Complexity.UnaryFn.fromBitsLE_min {c : List Bool → ℕ} {s : List Bool → List Bool} (hs : s ∈ FP) (hc : UnaryFn c) : UnaryFn fun (z : List Bool) => Min.min (Nat.fromBitsLE (s z)) (c z)

Reading a numeral below a cap is polynomial-time. If s ∈ FP and c is a polynomial-time number, then so is the value of s z, read least significant bit first, capped at c z. (Inside the UnaryFn namespace a bare min means UnaryFn.min, hence Min.min.)

theorem Complexity.UnaryFn.fromBitsLE_of_le {c : List Bool → ℕ} {s : List Bool → List Bool} (hs : s ∈ FP) (hc : UnaryFn c) (h : ∀ (z : List Bool), Nat.fromBitsLE (s z) ≤ c z) : UnaryFn fun (z : List Bool) => Nat.fromBitsLE (s z)

Reading a numeral is polynomial-time when its value is at most a polynomial-time number.