Unrestricted depth-three lower bound: language slice

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

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

def Complexity.DepthThreeLowerBound.parameterSlice {n d r t : ℕ} (u : Fin (d + r - 1) → Bool) (p : Fin r → Bool) (b : Fin t → Fin r → Bool) : Fin n → Fin d ⊕ Bool

Fix the parameter bits while leaving the data variables free.

Equations

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

theorem Complexity.DepthThreeLowerBound.parameterSlice_data {n d r t : ℕ} (u : Fin (d + r - 1) → Bool) (p : Fin r → Bool) (b : Fin t → Fin r → Bool) (i : Fin d) (hn : ↑i < n) : parameterSlice u p b ⟨↑i, hn⟩ = Sum.inl i

theorem Complexity.DepthThreeLowerBound.parameterSlice_hash {n d r t : ℕ} (u : Fin (d + r - 1) → Bool) (p : Fin r → Bool) (b : Fin t → Fin r → Bool) (i : Fin (d + r - 1)) (hn : d + ↑i < n) : parameterSlice u p b ⟨d + ↑i, hn⟩ = Sum.inr (u i)

theorem Complexity.DepthThreeLowerBound.parameterSlice_polynomial {n d r t : ℕ} (u : Fin (d + r - 1) → Bool) (p : Fin r → Bool) (b : Fin t → Fin r → Bool) (i : Fin r) (hn : d + (d + r - 1) + ↑i < n) : parameterSlice u p b ⟨d + (d + r - 1) + ↑i, hn⟩ = Sum.inr (p i)

theorem Complexity.DepthThreeLowerBound.parameterSlice_coefficient {n d r t : ℕ} (u : Fin (d + r - 1) → Bool) (p : Fin r → Bool) (b : Fin t → Fin r → Bool) (j : Fin t) (i : Fin r) (hn : d + (d + r - 1) + r + ↑j * r + ↑i < n) : parameterSlice u p b ⟨d + (d + r - 1) + r + ↑j * r + ↑i, hn⟩ = Sum.inr (b j i)

theorem Complexity.DepthThreeLowerBound.parameterSlice_suffix {n d r t : ℕ} (u : Fin (d + r - 1) → Bool) (p : Fin r → Bool) (b : Fin t → Fin r → Bool) (i : Fin n) (hi : d + (d + r - 1) + r + t * r ≤ ↑i) : parameterSlice u p b i = Sum.inr false

def Complexity.DepthThreeLowerBound.sliceParsedInput (n : ℕ) (u : Fin (dataDimension n + hashDimension (dataDimension n) - 1) → Bool) (p : Fin (hashDimension (dataDimension n)) → Bool) (b : Fin (independenceOrder (dataDimension n)) → Fin (hashDimension (dataDimension n)) → Bool) (x : Fin (dataDimension n) → Bool) : ParsedInput

The parsed input obtained from a fixed-parameter slice.

Equations

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

def Complexity.DepthThreeLowerBound.canonicalSlice (n : ℕ) (u : Fin (dataDimension n + hashDimension (dataDimension n) - 1) → Bool) (p : Fin (hashDimension (dataDimension n)) → Bool) (b : Fin (independenceOrder (dataDimension n)) → Fin (hashDimension (dataDimension n)) → Bool) : Fin n → Fin (dataDimension n) ⊕ Bool

The canonical input substitution fixing a chosen parameter tuple.

Equations

• Complexity.DepthThreeLowerBound.canonicalSlice n u p b = Complexity.DepthThreeLowerBound.parameterSlice u p b

def Complexity.DepthThreeLowerBound.canonicalSliceWord (n : ℕ) (u : Fin (dataDimension n + hashDimension (dataDimension n) - 1) → Bool) (p : Fin (hashDimension (dataDimension n)) → Bool) (b : Fin (independenceOrder (dataDimension n)) → Fin (hashDimension (dataDimension n)) → Bool) (x : Fin (dataDimension n) → Bool) : List Bool

Encode a data assignment as a word in the canonical slice.

Equations

• Complexity.DepthThreeLowerBound.canonicalSliceWord n u p b x = List.ofFn (Complexity.DepthThreeLowerBound.GateInput.assignment (Complexity.DepthThreeLowerBound.canonicalSlice n u p b) x)

@[simp]

theorem Complexity.DepthThreeLowerBound.canonicalSliceWord_length (n : ℕ) (u : Fin (dataDimension n + hashDimension (dataDimension n) - 1) → Bool) (p : Fin (hashDimension (dataDimension n)) → Bool) (b : Fin (independenceOrder (dataDimension n)) → Fin (hashDimension (dataDimension n)) → Bool) (x : Fin (dataDimension n) → Bool) : (canonicalSliceWord n u p b x).length = n

theorem Complexity.DepthThreeLowerBound.canonicalSlice_first (n : ℕ) (u : Fin (dataDimension n + hashDimension (dataDimension n) - 1) → Bool) (p : Fin (hashDimension (dataDimension n)) → Bool) (b : Fin (independenceOrder (dataDimension n)) → Fin (hashDimension (dataDimension n)) → Bool) (i : Fin (dataDimension n)) : canonicalSlice n u p b ⟨↑i, ⋯⟩ = Sum.inl i

theorem Complexity.DepthThreeLowerBound.canonicalSlice_unused (n : ℕ) (u : Fin (dataDimension n + hashDimension (dataDimension n) - 1) → Bool) (p : Fin (hashDimension (dataDimension n)) → Bool) (b : Fin (independenceOrder (dataDimension n)) → Fin (hashDimension (dataDimension n)) → Bool) (i : Fin n) (hi : blockLen (dataDimension n) ≤ ↑i) : canonicalSlice n u p b i = Sum.inr false

theorem Complexity.DepthThreeLowerBound.canonicalSliceWord_fits (n : ℕ) (u : Fin (dataDimension n + hashDimension (dataDimension n) - 1) → Bool) (p : Fin (hashDimension (dataDimension n)) → Bool) (b : Fin (independenceOrder (dataDimension n)) → Fin (hashDimension (dataDimension n)) → Bool) (x : Fin (dataDimension n) → Bool) (hd : 0 < dataDimension n) (ht : 2 ≤ independenceOrder (dataDimension n)) (hlen : blockLen (dataDimension n) ≤ n) : InputFits (canonicalSliceWord n u p b x)

theorem Complexity.DepthThreeLowerBound.decodeInput_canonicalSliceWord (n : ℕ) (u : Fin (dataDimension n + hashDimension (dataDimension n) - 1) → Bool) (p : Fin (hashDimension (dataDimension n)) → Bool) (b : Fin (independenceOrder (dataDimension n)) → Fin (hashDimension (dataDimension n)) → Bool) (x : Fin (dataDimension n) → Bool) (_hd : 0 < dataDimension n) (_ht : 2 ≤ independenceOrder (dataDimension n)) (hlen : blockLen (dataDimension n) ≤ n) : decodeInput (canonicalSliceWord n u p b x) = sliceParsedInput n u p b x

theorem Complexity.DepthThreeLowerBound.language_canonicalSliceWord (n : ℕ) (u : Fin (dataDimension n + hashDimension (dataDimension n) - 1) → Bool) (p : Fin (hashDimension (dataDimension n)) → Bool) (b : Fin (independenceOrder (dataDimension n)) → Fin (hashDimension (dataDimension n)) → Bool) (x : Fin (dataDimension n) → Bool) (hd : 0 < dataDimension n) (ht : 2 ≤ independenceOrder (dataDimension n)) (hlen : blockLen (dataDimension n) ≤ n) : language (canonicalSliceWord n u p b x) = (sliceParsedInput n u p b x).evaluate

theorem Complexity.DepthThreeLowerBound.language_ofFn_canonicalSlice (n : ℕ) (u : Fin (dataDimension n + hashDimension (dataDimension n) - 1) → Bool) (p : Fin (hashDimension (dataDimension n)) → Bool) (b : Fin (independenceOrder (dataDimension n)) → Fin (hashDimension (dataDimension n)) → Bool) (x : Cube (Fin (dataDimension n))) (hd : 0 < dataDimension n) (ht : 2 ≤ independenceOrder (dataDimension n)) (hlen : blockLen (dataDimension n) ≤ n) : language (List.ofFn (GateInput.assignment (canonicalSlice n u p b) x)) = (sliceParsedInput n u p b x).evaluate

theorem Complexity.DepthThreeLowerBound.language_canonicalSlice_quotient (n : ℕ) (u : Fin (dataDimension n + hashDimension (dataDimension n) - 1) → Bool) (p : Fin (hashDimension (dataDimension n)) → Bool) (b : Fin (independenceOrder (dataDimension n)) → Fin (hashDimension (dataDimension n)) → Bool) (x : Cube (Fin (dataDimension n))) (hd : 0 < dataDimension n) (ht : 2 ≤ independenceOrder (dataDimension n)) (hlen : blockLen (dataDimension n) ≤ n) : language (List.ofFn (GateInput.assignment (canonicalSlice n u p b) x)) = true ↔ (BinaryAlgebra.degreeZero ⋯) (sliceParsedInput n u p b x).quotientEvaluation = 0

theorem Complexity.DepthThreeLowerBound.language_canonicalSlice_acceptEval (n : ℕ) (u : Fin (dataDimension n + hashDimension (dataDimension n) - 1) → Bool) (p : Fin (hashDimension (dataDimension n)) → Bool) (b : Fin (independenceOrder (dataDimension n)) → Fin (hashDimension (dataDimension n)) → Bool) (x : Fin (dataDimension n) → Bool) [Fact (Irreducible (BinaryAlgebra.inputPolynomialBits p))] (hd : 0 < dataDimension n) (ht : 2 ≤ independenceOrder (dataDimension n)) (hlen : blockLen (dataDimension n) ≤ n) : language (List.ofFn (GateInput.assignment (canonicalSlice n u p b) x)) = Interpolation.acceptEval (BinaryAlgebra.degreeZero ⋯) (independenceOrder (dataDimension n)) (fun (y : Fin (dataDimension n) → Bool) => BinaryAlgebra.encode (fun (i : Fin (hashDimension (dataDimension n))) => BinaryAlgebra.bitValue (p i)) fun (i : Fin (hashDimension (dataDimension n))) => BinaryAlgebra.bitValue (BinaryHash.hashBool u y i)) (fun (j : Fin (independenceOrder (dataDimension n))) => BinaryAlgebra.encode (fun (i : Fin (hashDimension (dataDimension n))) => BinaryAlgebra.bitValue (p i)) fun (i : Fin (hashDimension (dataDimension n))) => BinaryAlgebra.bitValue (b j i)) x