Unrestricted depth-three lower bound: tape xor

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

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

inductive Complexity.DepthThreeLowerBound.TapeXor.State : Type

Control states of the xor routine.

• start : State
• scan : State
• rewind : State
• done : State

@[instance_reducible]

instance Complexity.DepthThreeLowerBound.TapeXor.instDecidableEqState : DecidableEq State

Equations

• Complexity.DepthThreeLowerBound.TapeXor.instDecidableEqState x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Complexity.DepthThreeLowerBound.TapeXor.instInhabitedState : Inhabited State

Equations

• Complexity.DepthThreeLowerBound.TapeXor.instInhabitedState = { default := Complexity.DepthThreeLowerBound.TapeXor.instInhabitedState.default }

@[instance_reducible]

instance Complexity.DepthThreeLowerBound.TapeXor.instFintypeState : Fintype State

Equations

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

def Complexity.DepthThreeLowerBound.TapeXor.start : State

Initial control state of the xor routine.

Equations

• Complexity.DepthThreeLowerBound.TapeXor.start = Complexity.DepthThreeLowerBound.TapeXor.State.start

def Complexity.DepthThreeLowerBound.TapeXor.done : State

Terminal control state of the xor routine.

Equations

• Complexity.DepthThreeLowerBound.TapeXor.done = Complexity.DepthThreeLowerBound.TapeXor.State.done

def Complexity.DepthThreeLowerBound.TapeXor.program (src dst : TapeRegister) : TapeMultiProgram State

Transition function of the xor routine.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.DepthThreeLowerBound.TapeXor.program src dst Complexity.DepthThreeLowerBound.TapeXor.State.done x✝ = none

@[simp]

theorem Complexity.DepthThreeLowerBound.TapeXor.program_done (src dst : TapeRegister) (h : TapeHeads) : program src dst done h = none

theorem Complexity.DepthThreeLowerBound.TapeXor.step_start {src dst : TapeRegister} (hne : src ≠ dst) (T : TapeTapes) (S D : Turing.Tape TapeSymbol) : (program src dst).step (TapeMultiProgram.cfg State.start (TapeCopy.onPair src dst T S D)) = some (TapeMultiProgram.cfg State.scan (TapeCopy.onPair src dst T (Turing.Tape.move Turing.Dir.right S) (Turing.Tape.move Turing.Dir.right D)))

theorem Complexity.DepthThreeLowerBound.TapeXor.step_scan_bit {src dst : TapeRegister} (hne : src ≠ dst) (T : TapeTapes) (S D : Turing.Tape TapeSymbol) (a b : Bool) (hS : S.head = rawInputSymbol a) (hD : D.head = rawInputSymbol b) : (program src dst).step (TapeMultiProgram.cfg State.scan (TapeCopy.onPair src dst T S D)) = some (TapeMultiProgram.cfg State.scan (TapeCopy.onPair src dst T (Turing.Tape.move Turing.Dir.right S) (Turing.Tape.move Turing.Dir.right (Turing.Tape.write (rawInputSymbol (a ^^ b)) D))))

theorem Complexity.DepthThreeLowerBound.TapeXor.step_scan_end {src dst : TapeRegister} (hne : src ≠ dst) (T : TapeTapes) (S D : Turing.Tape TapeSymbol) (hS : S.head = cleanAtom TapeAtom.endMark) (hD : D.head = cleanAtom TapeAtom.endMark) : (program src dst).step (TapeMultiProgram.cfg State.scan (TapeCopy.onPair src dst T S D)) = some (TapeMultiProgram.cfg State.rewind (TapeCopy.onPair src dst T S D))

theorem Complexity.DepthThreeLowerBound.TapeXor.step_rewind_move {src dst : TapeRegister} (hne : src ≠ dst) (T : TapeTapes) (S D : Turing.Tape TapeSymbol) (hS : S.head.1 ≠ TapeAtom.home) : (program src dst).step (TapeMultiProgram.cfg State.rewind (TapeCopy.onPair src dst T S D)) = some (TapeMultiProgram.cfg State.rewind (TapeCopy.onPair src dst T (Turing.Tape.move Turing.Dir.left S) (Turing.Tape.move Turing.Dir.left D)))

theorem Complexity.DepthThreeLowerBound.TapeXor.step_rewind_home {src dst : TapeRegister} (hne : src ≠ dst) (T : TapeTapes) (S D : Turing.Tape TapeSymbol) (hS : S.head.1 = TapeAtom.home) : (program src dst).step (TapeMultiProgram.cfg State.rewind (TapeCopy.onPair src dst T S D)) = some (TapeMultiProgram.cfg State.done (TapeCopy.onPair src dst T S D))

theorem Complexity.DepthThreeLowerBound.TapeXor.runs_scan {src dst : TapeRegister} (hne : src ≠ dst) (T : TapeTapes) (a b : List Bool) (LS LD : List TapeSymbol) (hlen : a.length = b.length) : RunsIn (program src dst).step (TapeMultiProgram.cfg State.scan (TapeCopy.onPair src dst T (Turing.Tape.mk₂ LS (encodeInput a ++ [cleanAtom TapeAtom.endMark])) (Turing.Tape.mk₂ LD (encodeInput b ++ [cleanAtom TapeAtom.endMark])))) (TapeMultiProgram.cfg State.rewind (TapeCopy.onPair src dst T (Turing.Tape.mk₂ ((encodeInput a).reverse ++ LS) [cleanAtom TapeAtom.endMark]) (Turing.Tape.mk₂ ((encodeInput (List.zipWith xor a b)).reverse ++ LD) [cleanAtom TapeAtom.endMark]))) (a.length + 1)

theorem Complexity.DepthThreeLowerBound.TapeXor.runs_rewind {src dst : TapeRegister} (hne : src ≠ dst) (T : TapeTapes) (a b : List Bool) (c : TapeSymbol) (RS RD : List TapeSymbol) (hlen : a.length = b.length) (hc : c.1 ≠ TapeAtom.home) : RunsIn (program src dst).step (TapeMultiProgram.cfg State.rewind (TapeCopy.onPair src dst T (Turing.Tape.mk₂ (encodeInput a ++ [cleanAtom TapeAtom.home]) (c :: RS)) (Turing.Tape.mk₂ (encodeInput b ++ [cleanAtom TapeAtom.home]) RD))) (TapeMultiProgram.cfg State.done (TapeCopy.onPair src dst T (Turing.Tape.mk₂ [] (cleanAtom TapeAtom.home :: ((encodeInput a).reverse ++ c :: RS))) (Turing.Tape.mk₂ [] (cleanAtom TapeAtom.home :: ((encodeInput b).reverse ++ RD))))) (a.length + 2)

theorem Complexity.DepthThreeLowerBound.TapeXor.runs_xor {src dst : TapeRegister} (hne : src ≠ dst) (T : TapeTapes) (a b : List Bool) (hlen : a.length = b.length) : RunsIn (program src dst).step (TapeMultiProgram.cfg start (TapeCopy.onPair src dst T (wordTape a) (wordTape b))) (TapeMultiProgram.cfg done (TapeCopy.onPair src dst T (wordTape a) (wordTape (List.zipWith xor a b)))) (2 * a.length + 4)

theorem Complexity.DepthThreeLowerBound.TapeXor.runs_store {src dst : TapeRegister} (hne : src ≠ dst) (σ : TapeStore) (a b : List Bool) (hsrc : σ src = a) (hdst : σ dst = b) (hlen : a.length = b.length) : RunsIn (program src dst).step (TapeMultiProgram.cfg start (storeTapes σ)) (TapeMultiProgram.cfg done (storeTapes (Function.update σ dst (List.zipWith xor a b)))) (2 * a.length + 4)

theorem Complexity.DepthThreeLowerBound.TapeXor.wordList_xor {n : ℕ} (a b : BitWord n) : wordList (wordXor a b) = List.zipWith xor (wordList a) (wordList b)

theorem Complexity.DepthThreeLowerBound.TapeXor.runs_wordStore {src dst : TapeRegister} (hne : src ≠ dst) (σ : TapeStore) {n : ℕ} (a b : BitWord n) (hsrc : σ src = wordList a) (hdst : σ dst = wordList b) : RunsIn (program src dst).step (TapeMultiProgram.cfg start (storeTapes σ)) (TapeMultiProgram.cfg done (storeTapes (Function.update σ dst (wordList (wordXor a b))))) (2 * n + 4)