Binary codes of numbers in polynomial time — proof internals

The helper facts behind Complexitylib.Classes.P.NatCodes.

A bit of a number is a quotient by a power of two, and the power can be capped: dividing n by anything above n gives 0, just as dividing by a larger power of two does. That keeps the power a polynomial-time number.

Reading a binary numeral back is a fold over its bits, from the most significant (last) bit to the least significant (first) one, that doubles the value and adds the bit. Capping every intermediate value at c keeps the fold's states polynomially short and changes nothing below the cap, since doubling and adding preserve "at least c".

Contents

• div_min_two_pow — a quotient by a power of two, with the power capped
• bit_fpPred — bit i of a polynomial-time number, as a test on pair z (1^i)
• fromBitsLE_min_internal — the capped value of a binary numeral is a polynomial-time number

theorem Complexity.div_min_two_pow (n i : ℕ) : n / min (2 ^ i) (n + 1) = n / 2 ^ i

Capping the power of two at n + 1 does not change the quotient of n.

theorem Complexity.bit_fpPred {n : List Bool → ℕ} (hn : UnaryFn n) : FPPred fun (v : List Bool) => n (pairFst v) / 2 ^ (pairSnd v).length % 2 = 1

Bit i of a polynomial-time number is a polynomial-time test of pair z (1^i).

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

The capped value of a binary numeral is a polynomial-time number. The fold over the bits of s z that doubles the value, adds the bit and caps the result at c z computes min (Nat.fromBitsLE (s z)) (c z).