Documentation

Complexitylib.Circuits.DepthThree.LowerBound.Internal.TapeNaturalAccess

Unrestricted depth-three lower bound: tape natural access #

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

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

source
theorem Complexity.DepthThreeLowerBound.TapeNaturalAccess.take_length (xs : List Bool) (i : ℕ) (hi : i < xs.length) :
(List.take i xs).length = i
source
theorem Complexity.DepthThreeLowerBound.TapeNaturalAccess.split (xs : List Bool) (i : ℕ) (hi : i < xs.length) :
xs = List.take i xs ++ xs.getD i false :: List.drop (i + 1) xs
source
theorem Complexity.DepthThreeLowerBound.TapeNaturalAccess.xorListAt_eq_split (xs : List Bool) (i : ℕ) (hi : i < xs.length) (v : Bool) :
xorListAt xs i v = List.take i xs ++ (xs.getD i false ^^ v) :: List.drop (i + 1) xs
source
theorem Complexity.DepthThreeLowerBound.TapeNaturalAccess.read (index array : TapeRegister) (hne : index ≠ array) (σ : TapeStore) (i : ℕ) (hi : σ index = List.replicate i true) (hib : i < (σ array).length) :
RunsIn (TapeArray.code index array id).step (TapeMultiProgram.cfg TapeArray.State.start (storeTapes σ)) (TapeMultiProgram.cfg (TapeArray.State.done ((σ array).getD i false)) (storeTapes σ)) (2 * i + 4)
source
theorem Complexity.DepthThreeLowerBound.TapeNaturalAccess.xorAt (index array : TapeRegister) (hne : index ≠ array) (σ : TapeStore) (i : ℕ) (v : Bool) (hi : σ index = List.replicate i true) (hib : i < (σ array).length) :
RunsIn (TapeArray.code index array fun (old : Bool) => old ^^ v).step (TapeMultiProgram.cfg TapeArray.State.start (storeTapes σ)) (TapeMultiProgram.cfg (TapeArray.State.done ((σ array).getD i false)) (storeTapes (Function.update σ array (xorListAt (σ array) i v)))) (2 * i + 4)
source
theorem Complexity.DepthThreeLowerBound.TapeNaturalAccess.productTerm (ia a ib b ic c : TapeRegister) (hia : ia ≠ a) (hib : ib ≠ b) (hic : ic ≠ c) (σ : TapeStore) (i j k : ℕ) (hi : σ ia = List.replicate i true) (hj : σ ib = List.replicate j true) (hk : σ ic = List.replicate k true) (hAi : i < (σ a).length) (hBj : j < (σ b).length) (hCk : k < (σ c).length) :
RunsIn (TapeProductTerm.program ia a ib b ic c).step (TapeMultiProgram.cfg TapeProductTerm.start (storeTapes σ)) (TapeMultiProgram.cfg (TapeProductTerm.done ((σ a).getD i false) ((σ b).getD j false) ((σ c).getD k false)) (storeTapes (Function.update σ c (xorListAt (σ c) k ((σ a).getD i false && (σ b).getD j false))))) (2 * (i + j + k) + 14)