Polynomial-time integer square roots on binary naturals

Nat.sqrt m (⌊√m⌋) is computable in polynomial time over Turing.MultiTapeTM.encNat by a most-significant-bit-first fold over m.size bit positions: at position i, the candidate bit 2 ^ i is added to the running root acc whenever (acc + 2 ^ i) ^ 2 ≤ m. Every intermediate accumulator satisfies acc ^ 2 ≤ m, hence acc ≤ m and (encNat acc).length ≤ (encNat m).length.

Main results

• Turing.MultiTapeTM.ComputableInPolyTime.binary_sqrt, .binary_sqrt': plain polynomial-time floor square root Nat.sqrt over encNat.
• Turing.MultiTapeTM.ComputableInPolyTime.binary_ceilSqrt, .binary_ceilSqrt': plain polynomial-time integer ceiling square root if m = 0 then 0 else (m - 1).sqrt + 1 over encNat.

theorem Turing.MultiTapeTM.ComputableInPolyTime.binary_sqrt : ComputableInPolyTime Nat.sqrt encNat encNat

Integer floor square root Nat.sqrt is polynomial-time on binary naturals.

theorem Turing.MultiTapeTM.ComputableInPolyTime.binary_sqrt' {α : Type} {input : α ↪ List Bool} {f : α → ℕ} (hf : ComputableInPolyTime f input encNat) : ComputableInPolyTime (fun (a : α) => (f a).sqrt) input encNat

Integer floor square root of a computed binary natural.

theorem Turing.MultiTapeTM.ComputableInPolyTime.binary_ceilSqrt : ComputableInPolyTime (fun (m : ℕ) => if m = 0 then 0 else (m - 1).sqrt + 1) encNat encNat

Integer ceiling square root if m = 0 then 0 else (m - 1).sqrt + 1 is polynomial-time on binary naturals.

theorem Turing.MultiTapeTM.ComputableInPolyTime.binary_ceilSqrt' {α : Type} {input : α ↪ List Bool} {f : α → ℕ} (hf : ComputableInPolyTime f input encNat) : ComputableInPolyTime (fun (a : α) => if f a = 0 then 0 else (f a - 1).sqrt + 1) input encNat

Integer ceiling square root of a computed binary natural.