Unrestricted depth-three lower bound: language input block words

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

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

theorem Complexity.DepthThreeLowerBound.inputBlockData_data_length {w : List Bool} (hfit : InputFits w) : (inputBlockData w InputBlockKind.data).length = (decodeInput w).dataSize

theorem Complexity.DepthThreeLowerBound.inputBlockData_hash_length {w : List Bool} (hfit : InputFits w) : (inputBlockData w InputBlockKind.hash).length = (decodeInput w).dataSize + (decodeInput w).ringDegree - 1

theorem Complexity.DepthThreeLowerBound.inputBlockData_polynomial_length {w : List Bool} (hfit : InputFits w) : (inputBlockData w InputBlockKind.polynomial).length = (decodeInput w).ringDegree

theorem Complexity.DepthThreeLowerBound.inputBlockData_coefficients_length {w : List Bool} (hfit : InputFits w) : (inputBlockData w InputBlockKind.coefficients).length = (decodeInput w).coefficientCount * (decodeInput w).ringDegree

theorem Complexity.DepthThreeLowerBound.decoded_ringDegree_ne_zero {w : List Bool} (hfit : InputFits w) : (decodeInput w).ringDegree ≠ 0

theorem Complexity.DepthThreeLowerBound.inputBlockData_data_eq_ofFn {w : List Bool} (hfit : InputFits w) : inputBlockData w InputBlockKind.data = List.ofFn (decodeInput w).data

theorem Complexity.DepthThreeLowerBound.inputBlockData_hash_eq_ofFn {w : List Bool} (hfit : InputFits w) : inputBlockData w InputBlockKind.hash = List.ofFn (decodeInput w).hashSeed

theorem Complexity.DepthThreeLowerBound.inputBlockData_polynomial_eq_ofFn {w : List Bool} (hfit : InputFits w) : inputBlockData w InputBlockKind.polynomial = List.ofFn (decodeInput w).polynomial

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

The list of coefficient blocks extracted from the input.

Equations

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

@[simp]

theorem Complexity.DepthThreeLowerBound.decodedCoefficientBlocks_length (w : List Bool) : (decodedCoefficientBlocks w).length = (decodeInput w).coefficientCount

theorem Complexity.DepthThreeLowerBound.decodedCoefficientBlocks_row_length (w b : List Bool) : b ∈ decodedCoefficientBlocks w → b.length = (decodeInput w).ringDegree

theorem Complexity.DepthThreeLowerBound.decodedCoefficientBlocks_flatten_length (w : List Bool) : (decodedCoefficientBlocks w).flatten.length = (decodeInput w).coefficientCount * (decodeInput w).ringDegree

theorem Complexity.DepthThreeLowerBound.inputBlockData_coefficients_eq_flatten {w : List Bool} (hfit : InputFits w) : inputBlockData w InputBlockKind.coefficients = (decodedCoefficientBlocks w).flatten

theorem Complexity.DepthThreeLowerBound.hornerBitLists_ofFn {r t : ℕ} (p h : BitWord r) (b : Fin t → BitWord r) : hornerBitLists r (List.ofFn p) (List.ofFn h) (List.ofFn fun (j : Fin t) => List.ofFn (b j)) = List.ofFn (wordHorner p h t b)

theorem Complexity.DepthThreeLowerBound.hashByUpdates_inputBlocks {w : List Bool} (hfit : InputFits w) : hashByUpdates (decodeInput w).ringDegree (inputBlockData w InputBlockKind.hash) (inputBlockData w InputBlockKind.data) = List.ofFn (wordHash (decodeInput w).hashSeed (decodeInput w).data)

theorem Complexity.DepthThreeLowerBound.hornerBitLists_inputBlocks {w : List Bool} (hfit : InputFits w) : hornerBitLists (decodeInput w).ringDegree (inputBlockData w InputBlockKind.polynomial) (hashByUpdates (decodeInput w).ringDegree (inputBlockData w InputBlockKind.hash) (inputBlockData w InputBlockKind.data)) (decodedCoefficientBlocks w) = List.ofFn (decodeInput w).evaluationBits

theorem Complexity.DepthThreeLowerBound.hornerFrom_inputBlocks {w : List Bool} (hfit : InputFits w) : hornerFrom (decodeInput w).ringDegree (inputBlockData w InputBlockKind.polynomial) (hashByUpdates (decodeInput w).ringDegree (inputBlockData w InputBlockKind.hash) (inputBlockData w InputBlockKind.data)) (decodedCoefficientBlocks w) (List.replicate (decodeInput w).ringDegree false) = List.ofFn (decodeInput w).evaluationBits

theorem Complexity.DepthThreeLowerBound.evaluateBits_eq_final_bit {w : List Bool} (hfit : InputFits w) : (decodeInput w).evaluateBits = !(hornerBitLists (decodeInput w).ringDegree (inputBlockData w InputBlockKind.polynomial) (hashByUpdates (decodeInput w).ringDegree (inputBlockData w InputBlockKind.hash) (inputBlockData w InputBlockKind.data)) (decodedCoefficientBlocks w)).getD 0 false

theorem Complexity.DepthThreeLowerBound.language_eq_final_bit {w : List Bool} (hfit : InputFits w) : language w = !(hornerBitLists (decodeInput w).ringDegree (inputBlockData w InputBlockKind.polynomial) (hashByUpdates (decodeInput w).ringDegree (inputBlockData w InputBlockKind.hash) (inputBlockData w InputBlockKind.data)) (decodedCoefficientBlocks w)).getD 0 false