Unrestricted depth-three lower bound: language

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

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

noncomputable def Complexity.DepthThreeLowerBound.ParsedInput.hashPolynomial (q : ParsedInput) : Polynomial (ZMod 2)

Pack the hashed data as a polynomial over the two-element field.

Equations

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

noncomputable def Complexity.DepthThreeLowerBound.ParsedInput.coefficientPolynomial (q : ParsedInput) (j : Fin q.coefficientCount) : Polynomial (ZMod 2)

Pack one parsed coefficient block as a binary polynomial.

Equations

• q.coefficientPolynomial j = Complexity.DepthThreeLowerBound.BinaryAlgebra.pack fun (i : Fin q.ringDegree) => Complexity.DepthThreeLowerBound.BinaryAlgebra.bitValue (q.coefficients j i)

noncomputable def Complexity.DepthThreeLowerBound.ParsedInput.modulus (q : ParsedInput) : Polynomial (ZMod 2)

The monic modulus polynomial specified by the parsed input.

Equations

• q.modulus = Complexity.DepthThreeLowerBound.BinaryAlgebra.inputPolynomialBits q.polynomial

theorem Complexity.DepthThreeLowerBound.ParsedInput.modulus_monic (q : ParsedInput) : q.modulus.Monic

theorem Complexity.DepthThreeLowerBound.ParsedInput.modulus_degree (q : ParsedInput) : q.modulus.degree = ↑q.ringDegree

noncomputable def Complexity.DepthThreeLowerBound.ParsedInput.evaluationPolynomial (q : ParsedInput) : Polynomial (ZMod 2)

Evaluate the parsed coefficient polynomial at the hash polynomial.

Equations

• q.evaluationPolynomial = ∑ j : Fin q.coefficientCount, q.coefficientPolynomial j * q.hashPolynomial ^ ↑j

noncomputable def Complexity.DepthThreeLowerBound.ParsedInput.evaluationRemainder (q : ParsedInput) : Polynomial (ZMod 2)

Reduce the evaluation polynomial modulo the parsed monic modulus.

Equations

• q.evaluationRemainder = q.evaluationPolynomial %ₘ q.modulus

theorem Complexity.DepthThreeLowerBound.ParsedInput.evaluationRemainder_degree_lt (q : ParsedInput) : q.evaluationRemainder.degree < ↑q.ringDegree

noncomputable def Complexity.DepthThreeLowerBound.ParsedInput.evaluate (q : ParsedInput) : Bool

Accept when the constant coefficient of the evaluation remainder is zero.

Equations

• q.evaluate = decide (q.evaluationRemainder.coeff 0 = 0)

theorem Complexity.DepthThreeLowerBound.ParsedInput.evaluate_eq_true_iff (q : ParsedInput) : q.evaluate = true ↔ q.evaluationRemainder.coeff 0 = 0

noncomputable def Complexity.DepthThreeLowerBound.language (w : List Bool) : Bool

The explicit language: parse the input and test the constant coefficient of its remainder.

Equations

• Complexity.DepthThreeLowerBound.language w = match Complexity.DepthThreeLowerBound.parseInput w with | none => false | some q => q.evaluate

theorem Complexity.DepthThreeLowerBound.language_of_not_fits {w : List Bool} (h : ¬InputFits w) : language w = false

theorem Complexity.DepthThreeLowerBound.language_of_fits {w : List Bool} (h : InputFits w) : language w = (decodeInput w).evaluate

theorem Complexity.DepthThreeLowerBound.language_eq_true_iff (w : List Bool) : language w = true ↔ InputFits w ∧ (decodeInput w).evaluationRemainder.coeff 0 = 0