Polynomial-time logarithms and bounded powers

The base-two logarithm is the binary representation's length minus one, with truncated subtraction handling zero. Unary input first uses the certified unary-to-binary conversion. Other fixed bases use repeated division with a linear bound on the encoded state. Ceiling logarithms follow from floor logarithms; raising a fixed factor to a ceiling logarithm uses the existing polynomial bound on logarithmically many multiplications. These latter certificates charge unary counter lengths; the bounded-power rule also accepts any caller's encoding with a certified unary size function.

Main results

• Turing.MultiTapeTM.ComputableTidilyInPolyTime.binary_log_two: compute the logarithm of a binary natural, returning its unary value.
• Turing.MultiTapeTM.ComputableTidilyInPolyTime.unary_log_two: the unary-input version.
• Turing.MultiTapeTM.ComputableTidilyInPolyTime.unary_log_const, .unary_clog_const: floor and ceiling logarithms in any fixed base on unary counters.
• Turing.MultiTapeTM.ComputableTidilyInPolyTime.unary_pow_clog_const: a fixed factor raised to a fixed-base ceiling logarithm, with unary output and complete intermediate-size bounds.
• Turing.MultiTapeTM.ComputableInPolyTime.unary_pow_clog_const: the same bounded power for plain certificates.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.binary_log_two : ComputableTidilyInPolyTime (Nat.log 2) encNat encUnary

The base-two logarithm is polynomial-time on binary naturals, with its result in unary.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.unary_log_two : ComputableTidilyInPolyTime (Nat.log 2) encUnary encUnary

The base-two logarithm is polynomial-time with both input and output in unary.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.unary_log_const (base : ℕ) : ComputableTidilyInPolyTime (Nat.log base) encUnary encUnary

Fixed-base logarithms are polynomial-time on unary counters, including bases zero and one. The division loop maintains the logarithm identity and a linear bound on its complete state.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.unary_clog_const (base : ℕ) : ComputableTidilyInPolyTime (Nat.clog base) encUnary encUnary

Ceiling logarithms in any fixed base are polynomial-time on unary counters.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.unary_pow_clog_const {α : Type} {input : α ↪ List Bool} {size : α → ℕ} (hsize : ComputableTidilyInPolyTime size input encUnary) (factor base : ℕ) : ComputableTidilyInPolyTime (fun (x : α) => factor ^ Nat.clog base (size x)) input encUnary

Given an efficient unary size function, a fixed factor raised to its fixed-base ceiling logarithm has a polynomial-time unary output in the caller's original encoding. The bound charges every intermediate power, including the initial one when the factor is zero.

theorem Turing.MultiTapeTM.ComputableInPolyTime.binary_log_two : ComputableInPolyTime (Nat.log 2) encNat encUnary

Turing.MultiTapeTM.ComputableTidilyInPolyTime.binary_log_two for plain certificates.

theorem Turing.MultiTapeTM.ComputableInPolyTime.unary_clog_const (base : ℕ) : ComputableInPolyTime (Nat.clog base) encUnary encUnary

Turing.MultiTapeTM.ComputableTidilyInPolyTime.unary_clog_const for plain certificates.

theorem Turing.MultiTapeTM.ComputableInPolyTime.unary_pow_clog_const {α : Type} {input : α ↪ List Bool} {size : α → ℕ} (hsize : ComputableInPolyTime size input encUnary) (factor base : ℕ) : ComputableInPolyTime (fun (x : α) => factor ^ Nat.clog base (size x)) input encUnary

Turing.MultiTapeTM.ComputableTidilyInPolyTime.unary_pow_clog_const for plain certificates.