Unrestricted depth-three lower bound: language bit convolution

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

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

def Complexity.DepthThreeLowerBound.xorBits (xs : List Bool) : Bool

Pointwise XOR of bit sequences.

Equations

• Complexity.DepthThreeLowerBound.xorBits xs = List.foldr xor false xs

@[simp]

theorem Complexity.DepthThreeLowerBound.xorBits_nil : xorBits [] = false

@[simp]

theorem Complexity.DepthThreeLowerBound.xorBits_cons (x : Bool) (xs : List Bool) : xorBits (x :: xs) = (x ^^ xorBits xs)

theorem Complexity.DepthThreeLowerBound.bitValue_xorBits (xs : List Bool) : BinaryAlgebra.bitValue (xorBits xs) = (List.map BinaryAlgebra.bitValue xs).sum

theorem Complexity.DepthThreeLowerBound.bitValue_xorBits_ofFn {n : ℕ} (f : Fin n → Bool) : BinaryAlgebra.bitValue (xorBits (List.ofFn f)) = ∑ i : Fin n, BinaryAlgebra.bitValue (f i)

def Complexity.DepthThreeLowerBound.wordConvolve {r s : ℕ} (a : BitWord r) (b : BitWord s) : BitWord (r + s)

Convolve bit words over the two-element field.

Equations

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

theorem Complexity.DepthThreeLowerBound.coeff_wordPoly_mul {r s : ℕ} (a : BitWord r) (b : BitWord s) (k : ℕ) : (wordPoly a * wordPoly b).coeff k = ∑ i : Fin r, ∑ j : Fin s, if ↑i + ↑j = k then BinaryAlgebra.bitValue (a i) * BinaryAlgebra.bitValue (b j) else 0

theorem Complexity.DepthThreeLowerBound.wordPoly_convolve {r s : ℕ} (a : BitWord r) (b : BitWord s) : wordPoly (wordConvolve a b) = wordPoly a * wordPoly b

def Complexity.DepthThreeLowerBound.wordList {n : ℕ} (a : BitWord n) : List Bool

Read a finite bit word as a list.

Equations

• Complexity.DepthThreeLowerBound.wordList a = List.ofFn a

def Complexity.DepthThreeLowerBound.listWord (n : ℕ) (xs : List Bool) : BitWord n

Read a bit list as a finite bit word.

Equations

• Complexity.DepthThreeLowerBound.listWord n xs i = xs.getD (↑i) false

@[simp]

theorem Complexity.DepthThreeLowerBound.wordList_length {n : ℕ} (a : BitWord n) : (wordList a).length = n

theorem Complexity.DepthThreeLowerBound.wordList_getD {n : ℕ} (a : BitWord n) (i : ℕ) : (wordList a).getD i false = wordGet a i

@[simp]

theorem Complexity.DepthThreeLowerBound.listWord_wordList {n : ℕ} (a : BitWord n) : listWord n (wordList a) = a

theorem Complexity.DepthThreeLowerBound.wordList_listWord_length (xs : List Bool) : wordList (listWord xs.length xs) = xs

theorem Complexity.DepthThreeLowerBound.wordList_listWord {n : ℕ} (xs : List Bool) (h : xs.length = n) : wordList (listWord n xs) = xs