Unrestricted depth-three lower bound: language bit word

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

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

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.BitWord (n : ℕ) : Type

A finite Boolean coefficient vector.

Equations

• Complexity.DepthThreeLowerBound.BitWord n = (Fin n → Bool)

noncomputable def Complexity.DepthThreeLowerBound.wordPoly {n : ℕ} (a : BitWord n) : Polynomial (ZMod 2)

Interpret a finite bit word as a binary polynomial.

Equations

• Complexity.DepthThreeLowerBound.wordPoly a = Complexity.DepthThreeLowerBound.BinaryAlgebra.pack fun (i : Fin n) => Complexity.DepthThreeLowerBound.BinaryAlgebra.bitValue (a i)

def Complexity.DepthThreeLowerBound.wordXor {n : ℕ} (a b : BitWord n) : BitWord n

Pointwise XOR of finite bit words.

Equations

• Complexity.DepthThreeLowerBound.wordXor a b i = (a i ^^ b i)

def Complexity.DepthThreeLowerBound.wordGet {n : ℕ} (a : BitWord n) (i : ℕ) : Bool

Read a bit-word entry with false as the out-of-range default.

Equations

• Complexity.DepthThreeLowerBound.wordGet a i = if h : i < n then a ⟨i, h⟩ else false

def Complexity.DepthThreeLowerBound.shiftModulus {r m : ℕ} (p : BitWord r) (s : ℕ) : BitWord m

The coefficient word of the shifted modulus polynomial.

Equations

• Complexity.DepthThreeLowerBound.shiftModulus p s i = if ↑i = s + r then true else if h : s ≤ ↑i ∧ ↑i < s + r then p ⟨↑i - s, ⋯⟩ else false

@[simp]

theorem Complexity.DepthThreeLowerBound.wordGet_fin {n : ℕ} (a : BitWord n) (i : Fin n) : wordGet a ↑i = a i

theorem Complexity.DepthThreeLowerBound.wordGet_of_lt {n : ℕ} (a : BitWord n) {i : ℕ} (hi : i < n) : wordGet a i = a ⟨i, hi⟩

theorem Complexity.DepthThreeLowerBound.wordGet_of_le {n : ℕ} (a : BitWord n) {i : ℕ} (hi : n ≤ i) : wordGet a i = false

@[simp]

theorem Complexity.DepthThreeLowerBound.wordGet_wordXor {n : ℕ} (a b : BitWord n) (i : ℕ) : wordGet (wordXor a b) i = (wordGet a i ^^ wordGet b i)

theorem Complexity.DepthThreeLowerBound.coeff_wordPoly {n : ℕ} (a : BitWord n) (i : ℕ) : (wordPoly a).coeff i = BinaryAlgebra.bitValue (wordGet a i)

@[simp]

theorem Complexity.DepthThreeLowerBound.coeff_wordPoly_fin {n : ℕ} (a : BitWord n) (i : Fin n) : (wordPoly a).coeff ↑i = BinaryAlgebra.bitValue (a i)

theorem Complexity.DepthThreeLowerBound.wordPoly_injective {n : ℕ} : Function.Injective wordPoly

@[simp]

theorem Complexity.DepthThreeLowerBound.wordPoly_zero (n : ℕ) : (wordPoly fun (x : Fin n) => false) = 0

theorem Complexity.DepthThreeLowerBound.wordPoly_xor {n : ℕ} (a b : BitWord n) : wordPoly (wordXor a b) = wordPoly a + wordPoly b

theorem Complexity.DepthThreeLowerBound.degree_wordPoly_lt {n : ℕ} (a : BitWord n) : (wordPoly a).degree < ↑n

theorem Complexity.DepthThreeLowerBound.degree_wordPoly_lt_of_zero_tail {n r : ℕ} (a : BitWord n) (h : ∀ (i : ℕ), r ≤ i → wordGet a i = false) : (wordPoly a).degree < ↑r

theorem Complexity.DepthThreeLowerBound.degree_wordPoly_lt_of_tail_false {n r : ℕ} (a : BitWord n) (h : ∀ (i : Fin n), r ≤ ↑i → a i = false) : (wordPoly a).degree < ↑r

theorem Complexity.DepthThreeLowerBound.inputPolynomialBits_eq_wordPoly {r : ℕ} (p : BitWord r) : BinaryAlgebra.inputPolynomialBits p = Polynomial.X ^ r + wordPoly p

@[simp]

theorem Complexity.DepthThreeLowerBound.shiftModulus_top {r m : ℕ} (p : BitWord r) (s : ℕ) (h : s + r < m) : shiftModulus p s ⟨s + r, h⟩ = true

theorem Complexity.DepthThreeLowerBound.shiftModulus_above {r m : ℕ} (p : BitWord r) (s : ℕ) (i : Fin m) (h : s + r < ↑i) : shiftModulus p s i = false

theorem Complexity.DepthThreeLowerBound.wordPoly_shiftModulus {r m : ℕ} (p : BitWord r) (s : ℕ) (hm : s + r < m) : wordPoly (shiftModulus p s) = Polynomial.X ^ s * BinaryAlgebra.inputPolynomialBits p