Unrestricted depth-three lower bound: language bit evaluator

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

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

theorem Complexity.DepthThreeLowerBound.mul_remainder_modByMonic (a b p : Polynomial (ZMod 2)) (hp : p.Monic) : a * (b %ₘ p) %ₘ p = a * b %ₘ p

theorem Complexity.DepthThreeLowerBound.wordPoly_mod_self {r : ℕ} (p a : BitWord r) : wordPoly a %ₘ BinaryAlgebra.inputPolynomialBits p = wordPoly a

def Complexity.DepthThreeLowerBound.wordHorner {r : ℕ} (p h : BitWord r) (t : ℕ) : (Fin t → BitWord r) → BitWord r

Evaluate a coefficient sequence by Horner iteration on bit words.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.DepthThreeLowerBound.wordHorner p h 0 x_2 = fun (x : Fin r) => false

theorem Complexity.DepthThreeLowerBound.wordPoly_horner {r : ℕ} (p h : BitWord r) (t : ℕ) (b : Fin t → BitWord r) : wordPoly (wordHorner p h t b) = (∑ j : Fin t, wordPoly (b j) * wordPoly h ^ ↑j) %ₘ BinaryAlgebra.inputPolynomialBits p

def Complexity.DepthThreeLowerBound.wordHash {d r : ℕ} (u : BitWord (d + r - 1)) (x : BitWord d) : BitWord r

Compute the binary hash in the bit-word representation.

Equations

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

theorem Complexity.DepthThreeLowerBound.wordHash_eq {d r : ℕ} (u : BitWord (d + r - 1)) (x : BitWord d) : wordHash u x = BinaryHash.hashBool u x

def Complexity.DepthThreeLowerBound.multiplyBitLists (r : ℕ) (p a b : List Bool) : List Bool

Multiply binary polynomials represented by bit lists.

Equations

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

@[simp]

theorem Complexity.DepthThreeLowerBound.multiplyBitLists_length (r : ℕ) (p a b : List Bool) : (multiplyBitLists r p a b).length = r

theorem Complexity.DepthThreeLowerBound.multiplyBitLists_correct (r : ℕ) (p a b : List Bool) : wordPoly (listWord r (multiplyBitLists r p a b)) = wordPoly (listWord r a) * wordPoly (listWord r b) %ₘ BinaryAlgebra.inputPolynomialBits (listWord r p)

def Complexity.DepthThreeLowerBound.hornerBitLists (r : ℕ) (p h : List Bool) (b : List (List Bool)) : List Bool

Evaluate coefficient bit lists by Horner iteration.

Equations

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

@[simp]

theorem Complexity.DepthThreeLowerBound.hornerBitLists_length (r : ℕ) (p h : List Bool) (b : List (List Bool)) : (hornerBitLists r p h b).length = r

theorem Complexity.DepthThreeLowerBound.hornerBitLists_correct (r : ℕ) (p h : List Bool) (b : List (List Bool)) : wordPoly (listWord r (hornerBitLists r p h b)) = (∑ j : Fin b.length, wordPoly (listWord r (b.getD ↑j [])) * wordPoly (listWord r h) ^ ↑j) %ₘ BinaryAlgebra.inputPolynomialBits (listWord r p)

def Complexity.DepthThreeLowerBound.ParsedInput.evaluationBits (q : ParsedInput) : BitWord q.ringDegree

Compute the parsed evaluation remainder as bits.

Equations

• q.evaluationBits = Complexity.DepthThreeLowerBound.wordHorner q.polynomial (Complexity.DepthThreeLowerBound.wordHash q.hashSeed q.data) q.coefficientCount q.coefficients

theorem Complexity.DepthThreeLowerBound.ParsedInput.wordPoly_evaluationBits (q : ParsedInput) : wordPoly q.evaluationBits = q.evaluationRemainder

def Complexity.DepthThreeLowerBound.ParsedInput.evaluateBits (q : ParsedInput) : Bool

Read the acceptance bit from the bit-level evaluation.

Equations

• q.evaluateBits = !Complexity.DepthThreeLowerBound.wordGet q.evaluationBits 0

theorem Complexity.DepthThreeLowerBound.ParsedInput.evaluateBits_eq (q : ParsedInput) : q.evaluateBits = q.evaluate

def Complexity.DepthThreeLowerBound.languageBits (w : List Bool) : Bool

The bit-level implementation of the explicit language.

Equations

• Complexity.DepthThreeLowerBound.languageBits w = match Complexity.DepthThreeLowerBound.parseInput w with | none => false | some q => q.evaluateBits

theorem Complexity.DepthThreeLowerBound.languageBits_eq_language (w : List Bool) : languageBits w = language w