Documentation

Complexitylib.Circuits.DepthThree.LowerBound.Internal.LanguageParser

Unrestricted depth-three lower bound: language parser #

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

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

structure Complexity.DepthThreeLowerBound.ParsedInput :

The data, hash seed, modulus bits, and coefficients parsed from an input word.

dataSize : ℕ
Number of data bits.
ringDegree : ℕ
Degree of the monic modulus polynomial.
coefficientCount : ℕ
Number of coefficient blocks.
data : Fin self.dataSize → Bool
The input data bits.
hashSeed : Fin (self.dataSize + self.ringDegree - 1) → Bool
The seed bits for the linear hash.
polynomial : Fin self.ringDegree → Bool
The lower coefficients of the monic modulus.
coefficients : Fin self.coefficientCount → Fin self.ringDegree → Bool
The coefficient blocks of the evaluation polynomial.

Instances For

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

Extract the parameter blocks and data from an input word.

Equations

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

Instances For

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

The input has sufficient length for all blocks specified by its parameters.

Equations

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

Instances For

@[instance_reducible]

instance Complexity.DepthThreeLowerBound.instDecidableInputFits (w : List Bool) :

Decidable (InputFits w)

Equations

Complexity.DepthThreeLowerBound.instDecidableInputFits w = id inferInstance

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

Option ParsedInput

Parse an input when its parameter blocks fit, rejecting otherwise.

Equations

Complexity.DepthThreeLowerBound.parseInput w = if Complexity.DepthThreeLowerBound.InputFits w then some (Complexity.DepthThreeLowerBound.decodeInput w) else none

Instances For

theorem Complexity.DepthThreeLowerBound.parseInput_of_fits {w : List Bool} (h : InputFits w) :

parseInput w = some (decodeInput w)

theorem Complexity.DepthThreeLowerBound.parseInput_of_not_fits {w : List Bool} (h : ¬InputFits w) :

parseInput w = none

theorem Complexity.DepthThreeLowerBound.parseInput_eq_some_iff (w : List Bool) (q : ParsedInput) :

parseInput w = some q ↔ InputFits w ∧ decodeInput w = q

theorem Complexity.DepthThreeLowerBound.parseInput_eq_none_iff (w : List Bool) :

parseInput w = none ↔ ¬InputFits w

theorem Complexity.DepthThreeLowerBound.decodeInput_dataSize (w : List Bool) :

(decodeInput w).dataSize = dataDimension w.length

theorem Complexity.DepthThreeLowerBound.decodeInput_ringDegree (w : List Bool) :

(decodeInput w).ringDegree = hashDimension (dataDimension w.length)

theorem Complexity.DepthThreeLowerBound.decodeInput_coefficientCount (w : List Bool) :

(decodeInput w).coefficientCount = independenceOrder (dataDimension w.length)

theorem Complexity.DepthThreeLowerBound.data_read_lt (w : List Bool) (i : Fin (dataDimension w.length)) :

↑i < w.length

theorem Complexity.DepthThreeLowerBound.hash_read_lt {w : List Bool} (h : InputFits w) (i : Fin (dataDimension w.length + hashDimension (dataDimension w.length) - 1)) :

hashOffset (dataDimension w.length) + ↑i < w.length

theorem Complexity.DepthThreeLowerBound.polynomial_read_lt {w : List Bool} (h : InputFits w) (i : Fin (hashDimension (dataDimension w.length))) :

polynomialOffset (dataDimension w.length) + ↑i < w.length

theorem Complexity.DepthThreeLowerBound.coefficient_read_lt {w : List Bool} (h : InputFits w) (j : Fin (independenceOrder (dataDimension w.length))) (i : Fin (hashDimension (dataDimension w.length))) :

coefficientOffset (dataDimension w.length) ↑j + ↑i < w.length

theorem Complexity.DepthThreeLowerBound.decoded_ringDegree_pos {w : List Bool} (h : InputFits w) :

0 < (decodeInput w).ringDegree

theorem Complexity.DepthThreeLowerBound.decoded_coefficientCount_two_le {w : List Bool} (h : InputFits w) :

2 ≤ (decodeInput w).coefficientCount