Documentation

Complexity.Computability.Complexity.FineGrained.CountingScale

The sublinear exponent of the interpolation counting algorithm #

The rational-interpolation route of OpenAI's The Exponential Time Hypothesis is False, Proposition 6.4, uses the scale n (log log n)² / √log n. Shifting the logarithm's argument by sixteen gives a real-valued scale defined at every natural input. This module proves that the scale is sublinear. It does not construct a counting algorithm or certify its running time.

Main definitions #

Main results #

References #

source
noncomputable def Cslib.Complexity.SubexponentialSAT.interpolationScale (n : ℕ) :
ℝ

The interpolation exponent with a positive logarithm argument at every natural input.

Instances For
    source
    theorem Cslib.Complexity.SubexponentialSAT.isLittleO_interpolationScale :
    interpolationScale =o[Filter.atTop] fun (n : ℕ) => ↑n

    The interpolation exponent grows more slowly than the number of variables.

    source
    theorem Cslib.Complexity.SubexponentialSAT.eventually_mul_interpolationScale_le (A : ℝ) {ε : ℝ} (hε : 0 < ε) :
    ∀ᶠ (n : ℕ) in Filter.atTop, A * interpolationScale n ≤ ε * ↑n

    Every fixed multiple of the exponent is eventually at most any positive linear exponent.

    source
    theorem Cslib.Complexity.SubexponentialSAT.interpolationScale_nonneg (n : ℕ) :
    0 ≤ interpolationScale n

    The interpolation scale is nonnegative at every natural input.

    source
    @[simp]
    theorem Cslib.Complexity.SubexponentialSAT.interpolationScale_zero :
    interpolationScale 0 = 0

    At zero variables, the shifted interpolation scale vanishes.

    source
    theorem Cslib.Complexity.SubexponentialSAT.one_lt_log_add_sixteen (n : ℕ) :
    1 < Real.log (↑n + 16)

    For every natural n, the shifted logarithm log (n + 16) exceeds 1.

    source
    theorem Cslib.Complexity.SubexponentialSAT.log_add_sixteen_pos (n : ℕ) :
    0 < Real.log (↑n + 16)

    For every natural n, 0 < log (n + 16).

    source
    theorem Cslib.Complexity.SubexponentialSAT.one_lt_log_log_add_sixteen (n : ℕ) :
    1 < Real.log (Real.log (↑n + 16))

    For every natural n, the shifted iterated logarithm log (log (n + 16)) exceeds 1 (since 16 = 2 ^ 4 and 4 * log 2 > e).

    source
    theorem Cslib.Complexity.SubexponentialSAT.log_log_add_sixteen_pos (n : ℕ) :
    0 < Real.log (Real.log (↑n + 16))

    For every natural n, 0 < log (log (n + 16)).

    source
    theorem Cslib.Complexity.SubexponentialSAT.interpolationScale_pos {n : ℕ} (hn : 1 ≤ n) :
    0 < interpolationScale n

    The interpolation scale is strictly positive for 1 ≤ n.

    source
    theorem Cslib.Complexity.SubexponentialSAT.exists_two_pow_mul_interpolationScale_le (A : ℝ) {ε : ℝ} (hε : 0 < ε) :
    ∃ (K : ℝ), 1 ≤ K ∧ ∀ (n : ℕ), 2 ^ (A * interpolationScale n) ≤ K * 2 ^ (ε * ↑n)

    For any multiplier A and any ε > 0, 2 ^ (A * interpolationScale n) is globally bounded by a constant multiple of 2 ^ (ε * n).