Unrestricted depth-three lower bound: language parameters

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/DepthThree/LanguageParameters.lean

Imports, namespaces, module visibility, documentation, and formatting are adapted for complexitylib. The source theorem statements and mathematical proofs are retained.

def Complexity.DepthThreeLowerBound.dataDimension (n : ℕ) : ℕ

Use one fifth of the input length for data variables.

Equations

• Complexity.DepthThreeLowerBound.dataDimension n = n / 5

theorem Complexity.DepthThreeLowerBound.five_mul_dataDimension_le (n : ℕ) : 5 * dataDimension n ≤ n

theorem Complexity.DepthThreeLowerBound.lt_five_mul_dataDimension_add_five (n : ℕ) : n < 5 * dataDimension n + 5

theorem Complexity.DepthThreeLowerBound.dataDimension_eq_zero_iff (n : ℕ) : dataDimension n = 0 ↔ n < 5

theorem Complexity.DepthThreeLowerBound.hashDimension_exists (d : ℕ) (hd : 0 < d) : ∃ (r : ℕ), 0 < r ∧ d ^ 2 ≤ r ^ 3

def Complexity.DepthThreeLowerBound.hashDimension (d : ℕ) : ℕ

The least positive r with d ^ 2 ≤ r ^ 3, or zero when d = 0.

Equations

• Complexity.DepthThreeLowerBound.hashDimension d = if hd : d = 0 then 0 else Nat.find ⋯

@[simp]

theorem Complexity.DepthThreeLowerBound.hashDimension_zero : hashDimension 0 = 0

theorem Complexity.DepthThreeLowerBound.hashDimension_spec {d : ℕ} (hd : 0 < d) : 0 < hashDimension d ∧ d ^ 2 ≤ hashDimension d ^ 3

theorem Complexity.DepthThreeLowerBound.hashDimension_pos {d : ℕ} (hd : 0 < d) : 0 < hashDimension d

theorem Complexity.DepthThreeLowerBound.hashDimension_cube_bound (d : ℕ) : d ^ 2 ≤ hashDimension d ^ 3

theorem Complexity.DepthThreeLowerBound.hashDimension_minimal {d r : ℕ} (hd : 0 < d) (hr : 0 < r) (hcube : d ^ 2 ≤ r ^ 3) : hashDimension d ≤ r

theorem Complexity.DepthThreeLowerBound.hashDimension_le (d : ℕ) : hashDimension d ≤ d

theorem Complexity.DepthThreeLowerBound.hashDimension_le_iff {d r : ℕ} (hd : 0 < d) : hashDimension d ≤ r ↔ 0 < r ∧ d ^ 2 ≤ r ^ 3

theorem Complexity.DepthThreeLowerBound.nat_le_sixth_power (j : ℕ) : j ≤ j ^ 6

theorem Complexity.DepthThreeLowerBound.sixth_power_le_implies_le {j d : ℕ} (hj : j ^ 6 ≤ d) : j ≤ d

def Complexity.DepthThreeLowerBound.independenceOrder (d : ℕ) : ℕ

The independence parameter chosen for the input dimension.

Equations

• Complexity.DepthThreeLowerBound.independenceOrder d = Nat.findGreatest (fun (t : ℕ) => Even t ∧ t ^ 6 ≤ d) d

@[simp]

theorem Complexity.DepthThreeLowerBound.independenceOrder_zero : independenceOrder 0 = 0

theorem Complexity.DepthThreeLowerBound.independenceOrder_spec (d : ℕ) : Even (independenceOrder d) ∧ independenceOrder d ^ 6 ≤ d

theorem Complexity.DepthThreeLowerBound.independenceOrder_even (d : ℕ) : Even (independenceOrder d)

theorem Complexity.DepthThreeLowerBound.independenceOrder_pow_le (d : ℕ) : independenceOrder d ^ 6 ≤ d

theorem Complexity.DepthThreeLowerBound.independenceOrder_le (d : ℕ) : independenceOrder d ≤ d

theorem Complexity.DepthThreeLowerBound.independenceOrder_greatest {d j : ℕ} (hj : Even j) (hpow : j ^ 6 ≤ d) : j ≤ independenceOrder d

theorem Complexity.DepthThreeLowerBound.independenceOrder_two_le_iff (d : ℕ) : 2 ≤ independenceOrder d ↔ 64 ≤ d

theorem Complexity.DepthThreeLowerBound.independenceOrder_eq_zero_iff (d : ℕ) : independenceOrder d = 0 ↔ d < 64

theorem Complexity.DepthThreeLowerBound.independenceOrder_next_pow_gt (d : ℕ) : d < (independenceOrder d + 2) ^ 6

theorem Complexity.DepthThreeLowerBound.independenceOrder_eq_iff (d j : ℕ) : independenceOrder d = j ↔ Even j ∧ j ^ 6 ≤ d ∧ ∀ (k : ℕ), Even k → k ^ 6 ≤ d → k ≤ j

theorem Complexity.DepthThreeLowerBound.independenceOrder_dataDimension_two_le_iff (n : ℕ) : 2 ≤ independenceOrder (dataDimension n) ↔ 320 ≤ n

def Complexity.DepthThreeLowerBound.hashBlockLength (d : ℕ) : ℕ

The number of seed bits used by the Toeplitz hash.

Equations

• Complexity.DepthThreeLowerBound.hashBlockLength d = d + Complexity.DepthThreeLowerBound.hashDimension d - 1

def Complexity.DepthThreeLowerBound.hashOffset (d : ℕ) : ℕ

The input position at which the hash-seed block starts.

Equations

• Complexity.DepthThreeLowerBound.hashOffset d = d

def Complexity.DepthThreeLowerBound.polynomialOffset (d : ℕ) : ℕ

The input position at which the modulus block starts.

Equations

• Complexity.DepthThreeLowerBound.polynomialOffset d = Complexity.DepthThreeLowerBound.hashOffset d + Complexity.DepthThreeLowerBound.hashBlockLength d

def Complexity.DepthThreeLowerBound.coefficientsOffset (d : ℕ) : ℕ

The input position at which the coefficient blocks start.

Equations

• Complexity.DepthThreeLowerBound.coefficientsOffset d = Complexity.DepthThreeLowerBound.polynomialOffset d + Complexity.DepthThreeLowerBound.hashDimension d

def Complexity.DepthThreeLowerBound.coefficientOffset (d j : ℕ) : ℕ

The input position at which a selected coefficient block starts.

Equations

• Complexity.DepthThreeLowerBound.coefficientOffset d j = Complexity.DepthThreeLowerBound.coefficientsOffset d + j * Complexity.DepthThreeLowerBound.hashDimension d

def Complexity.DepthThreeLowerBound.blockLen (d : ℕ) : ℕ

Total length of the data and parameter blocks.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.DepthThreeLowerBound.polynomialOffset_eq (d : ℕ) : polynomialOffset d = d + (d + hashDimension d - 1)

theorem Complexity.DepthThreeLowerBound.coefficientsOffset_eq (d : ℕ) : coefficientsOffset d = d + (d + hashDimension d - 1) + hashDimension d

theorem Complexity.DepthThreeLowerBound.blockLen_eq_sum (d : ℕ) : blockLen d = d + (d + hashDimension d - 1) + hashDimension d + independenceOrder d * hashDimension d

theorem Complexity.DepthThreeLowerBound.blockLen_eq {d : ℕ} (hd : 0 < d) : blockLen d = 2 * d + (independenceOrder d + 2) * hashDimension d - 1

theorem Complexity.DepthThreeLowerBound.hashBlockLength_pos {d : ℕ} (hd : 0 < d) : 0 < hashBlockLength d

theorem Complexity.DepthThreeLowerBound.hashOffset_le_polynomialOffset (d : ℕ) : hashOffset d ≤ polynomialOffset d

theorem Complexity.DepthThreeLowerBound.polynomialOffset_le_coefficientsOffset (d : ℕ) : polynomialOffset d ≤ coefficientsOffset d

theorem Complexity.DepthThreeLowerBound.coefficientsOffset_le_blockLen (d : ℕ) : coefficientsOffset d ≤ blockLen d

@[simp]

theorem Complexity.DepthThreeLowerBound.coefficientOffset_zero (d : ℕ) : coefficientOffset d 0 = coefficientsOffset d

theorem Complexity.DepthThreeLowerBound.coefficientOffset_succ (d j : ℕ) : coefficientOffset d (j + 1) = coefficientOffset d j + hashDimension d

theorem Complexity.DepthThreeLowerBound.coefficientOffset_last (d : ℕ) : coefficientOffset d (independenceOrder d) = blockLen d

theorem Complexity.DepthThreeLowerBound.coefficientOffset_mono (d : ℕ) {j k : ℕ} (hjk : j ≤ k) : coefficientOffset d j ≤ coefficientOffset d k

theorem Complexity.DepthThreeLowerBound.hash_index_lt {d i s : ℕ} (hi : i < hashDimension d) (hs : s < d) : i + s < hashBlockLength d

theorem Complexity.DepthThreeLowerBound.hash_absolute_index_lt {d i s : ℕ} (hi : i < hashDimension d) (hs : s < d) : hashOffset d + (i + s) < polynomialOffset d

theorem Complexity.DepthThreeLowerBound.polynomial_index_lt {d i : ℕ} (hi : i < hashDimension d) : polynomialOffset d + i < coefficientsOffset d

theorem Complexity.DepthThreeLowerBound.coefficient_index_lt {d j i : ℕ} (hj : j < independenceOrder d) (hi : i < hashDimension d) : coefficientOffset d j + i < blockLen d

theorem Complexity.DepthThreeLowerBound.blockLen_le_quad (d : ℕ) : blockLen d ≤ d * d + 4 * d

theorem Complexity.DepthThreeLowerBound.blockLen_le_four_mul_sub_one {d : ℕ} (hd : 0 < d) (hlt : d < 64) : blockLen d ≤ 4 * d - 1