Documentation

Complexitylib.Circuits.DepthThree.LowerBound.Internal.TapeStoreRepresentation

Unrestricted depth-three lower bound: tape store representation #

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/DepthThree/TapeStoreRepresentation.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.storeTapes (σ : TapeStore) :
TapeTapes

Represent every register's bit list by a boundary-marked tape.

Equations
Instances For
    source
    @[simp]
    theorem Complexity.DepthThreeLowerBound.storeTapes_apply (σ : TapeStore) (r : TapeRegister) :
    storeTapes σ r = wordTape (σ r)
    source
    theorem Complexity.DepthThreeLowerBound.storeTapes_update (σ : TapeStore) (r : TapeRegister) (bits : List Bool) :
    storeTapes (Function.update σ r bits) = Function.update (storeTapes σ) r (wordTape bits)
    source
    theorem Complexity.DepthThreeLowerBound.onPair_eq_updates {α : Type uDepth1} {src dst : TapeRegister} (hne : src ≠ dst) (T : TapeRegister → α) (S D : α) :
    TapeCopy.onPair src dst T S D = Function.update (Function.update T src S) dst D
    source
    theorem Complexity.DepthThreeLowerBound.TapeStoreRuns.copy {src dst : TapeRegister} (hne : src ≠ dst) (σ : TapeStore) (hempty : σ dst = []) :
    RunsIn (TapeCopy.code src dst).step (TapeMultiProgram.cfg TapeCopy.State.start (storeTapes σ)) (TapeMultiProgram.cfg TapeCopy.State.done (storeTapes (Function.update σ dst (σ src)))) (2 * (σ src).length + 4)
    source
    theorem Complexity.DepthThreeLowerBound.TapeStoreRuns.erase (r : TapeRegister) (σ : TapeStore) :
    RunsIn (TapeErase.code r).step (TapeMultiProgram.cfg TapeErase.State.start (storeTapes σ)) (TapeMultiProgram.cfg TapeErase.State.done (storeTapes (Function.update σ r []))) (2 * (σ r).length + 5)
    source
    theorem Complexity.DepthThreeLowerBound.TapeStoreRuns.push (r : TapeRegister) (b : Bool) (σ : TapeStore) :
    RunsIn (TapeFill.pushProgram r b).step (TapeMultiProgram.cfg TapeUnary.IncState.start (storeTapes σ)) (TapeMultiProgram.cfg TapeUnary.IncState.done (storeTapes (Function.update σ r (b :: σ r)))) 2
    source
    theorem Complexity.DepthThreeLowerBound.TapeStoreRuns.add {counter destination : TapeRegister} (hne : counter ≠ destination) (σ : TapeStore) (n m : ℕ) (hc : σ counter = List.replicate n true) (hd : σ destination = List.replicate m true) :
    RunsIn (TapeArithmetic.addProgram counter destination).step (TapeMultiProgram.cfg TapeArithmetic.addStart (storeTapes σ)) (TapeMultiProgram.cfg TapeArithmetic.addDone (storeTapes (Function.update (Function.update σ counter []) destination (List.replicate (m + n) true)))) (8 * n + 3)
    source
    theorem Complexity.DepthThreeLowerBound.TapeStoreRuns.fill {counter destination : TapeRegister} (hne : counter ≠ destination) (b : Bool) (σ : TapeStore) (n : ℕ) (hc : σ counter = List.replicate n true) :
    RunsIn (TapeFill.fillProgram counter destination b).step (TapeMultiProgram.cfg TapeFill.fillStart (storeTapes σ)) (TapeMultiProgram.cfg TapeFill.fillDone (storeTapes (Function.update (Function.update σ counter []) destination (List.replicate n b ++ σ destination)))) (8 * n + 3)