Documentation

Complexitylib.Circuits.DepthThree.LowerBound.Internal.TapeDecodeParsed

Unrestricted depth-three lower bound: tape decode parsed #

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

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

source
def Complexity.DepthThreeLowerBound.TapeDecodeParsed.outputStore (w : List Bool) :
TapeStore

Tape-store contents at the output stage of the decode parsed routine.

Equations
Instances For
    source
    @[simp]
    theorem Complexity.DepthThreeLowerBound.TapeDecodeParsed.outputStore_block (w : List Bool) (kind : InputBlockKind) :
    outputStore w (TapeInputBlocks.outputRegister kind) = inputBlockData w kind
    source
    theorem Complexity.DepthThreeLowerBound.TapeDecodeParsed.outputStore_other (w : List Bool) (q : TapeRegister) (h15 : q ≠ 15) (h16 : q ≠ 16) (h17 : q ≠ 17) (h18 : q ≠ 18) :
    outputStore w q = TapeParse.outputStore w q
    source
    @[simp]
    theorem Complexity.DepthThreeLowerBound.TapeDecodeParsed.outputStore_data (w : List Bool) :
    outputStore w 2 = List.replicate (dataDimension w.length) true
    source
    @[simp]
    theorem Complexity.DepthThreeLowerBound.TapeDecodeParsed.outputStore_hash (w : List Bool) :
    outputStore w 3 = List.replicate (hashDimension (dataDimension w.length)) true
    source
    @[simp]
    theorem Complexity.DepthThreeLowerBound.TapeDecodeParsed.outputStore_order (w : List Bool) :
    outputStore w 4 = List.replicate (independenceOrder (dataDimension w.length)) true
    source
    theorem Complexity.DepthThreeLowerBound.TapeDecodeParsed.outputStore_empty (w : List Bool) (q : TapeRegister) (h0 : q ≠ 0) (h1 : q ≠ 1) (h2 : q ≠ 2) (h3 : q ≠ 3) (h4 : q ≠ 4) (h8 : q ≠ 8) (h15 : q ≠ 15) (h16 : q ≠ 16) (h17 : q ≠ 17) (h18 : q ≠ 18) :
    outputStore w q = []
    source
    theorem Complexity.DepthThreeLowerBound.TapeDecodeParsed.runs_decode (w : List Bool) (hfit : InputFits w) :
    RunsIn TapeDecodeBlocks.program.step (TapeMultiProgram.cfg TapeDecodeBlocks.start (storeTapes (TapeParse.outputStore w))) (TapeMultiProgram.cfg TapeDecodeBlocks.done (storeTapes (outputStore w))) (804 * (w.length + 1) ^ 2)