Logarithmic inflation of constructible clocks

A polynomial-time computation on the binary representation of a natural number m takes time polynomial in its number of digits, hence O(m + 1). Consequently a binary-polynomial transformation that does not decrease a time-constructible clock preserves time constructibility. The transformation need only dominate the values taken by that clock.

In particular, a clock can be multiplied by a positive binary-polynomial function of its own value, such as one plus its binary length, or the fourth root ⌊√⌊√⌊log₂ f⌋⌋⌋ of its logarithm. These are logarithmic or smaller overheads, below multiplying the clock by the input length when it is polynomially bounded. These closure lemmas use the library's certified machines and do not assume a faster universal simulator.

Main results

• Cslib.Complexity.TimeConstructible.comp_of_computableInPolyTime: efficient binary postprocessing preserves time constructibility when it does not decrease the clock.
• Cslib.Complexity.TimeConstructible.mul_comp_of_computableInPolyTime: so does multiplying the clock by a positive binary-polynomial function of its value.
• Cslib.Complexity.TimeConstructible.mul_size_succ: a time-constructible f remains time-constructible after replacing f n by f n * (Nat.size (f n) + 1).
• Cslib.Complexity.TimeConstructible.mul_sqrt_sqrt_log_two: likewise for f n * ⌊√⌊√⌊log₂ (f n)⌋⌋⌋ when 2 ≤ f n.

theorem Cslib.Complexity.TimeConstructible.comp_of_computableInPolyTime {f g : ℕ → ℕ} (hf : TimeConstructible f) (hg : Turing.MultiTapeTM.ComputableInPolyTime g Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encNat) (hfg : ∀ (n : ℕ), f n ≤ g (f n)) : TimeConstructible fun (n : ℕ) => g (f n)

Binary-polynomial postprocessing of a time-constructible bound is time-constructible, provided the transformed clock dominates the original one. The cost polynomial in the binary length of f n is absorbed in O(f n + 1) before composition.

theorem Cslib.Complexity.TimeConstructible.mul_comp_of_computableInPolyTime {f g : ℕ → ℕ} (hf : TimeConstructible f) (hg : Turing.MultiTapeTM.ComputableInPolyTime g Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encNat) (hfg : ∀ (n : ℕ), 1 ≤ g (f n)) : TimeConstructible fun (n : ℕ) => f n * g (f n)

Multiplying a time-constructible clock by a binary-polynomial function of its value preserves time constructibility, provided that function is positive on the values of the clock.

theorem Cslib.Complexity.TimeConstructible.mul_size_succ {f : ℕ → ℕ} (hf : TimeConstructible f) : TimeConstructible fun (n : ℕ) => f n * ((f n).size + 1)

Multiplying a time-constructible clock by one plus its binary length preserves time constructibility, including at the zero value of the clock.

theorem Cslib.Complexity.TimeConstructible.mul_sqrt_sqrt_log_two {f : ℕ → ℕ} (hf : TimeConstructible f) (hf₂ : ∀ (n : ℕ), 2 ≤ f n) : TimeConstructible fun (n : ℕ) => f n * (Nat.log 2 (f n)).sqrt.sqrt

Multiplying a time-constructible clock f ≥ 2 by the fourth root ⌊√⌊√⌊log₂ f⌋⌋⌋ of its logarithm preserves time constructibility.