Unrestricted depth-three lower bound: tape unary compare scan

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

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

inductive Complexity.DepthThreeLowerBound.TapeUnaryCompareScan.State : Type

Control states of the unary compare scan routine.

• beginR : State
• beginS : State
• scan : State
• advanceS : State
• done (result : Ordering) : State

@[instance_reducible]

instance Complexity.DepthThreeLowerBound.TapeUnaryCompareScan.instDecidableEqState : DecidableEq State

Equations

• Complexity.DepthThreeLowerBound.TapeUnaryCompareScan.instDecidableEqState = Complexity.DepthThreeLowerBound.TapeUnaryCompareScan.instDecidableEqState.decEq

def Complexity.DepthThreeLowerBound.TapeUnaryCompareScan.instDecidableEqState.decEq (x✝ x✝¹ : State) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Complexity.DepthThreeLowerBound.TapeUnaryCompareScan.instFintypeState : Fintype State

Equations

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

@[instance_reducible]

instance Complexity.DepthThreeLowerBound.TapeUnaryCompareScan.instInhabitedState : Inhabited State

Equations

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

def Complexity.DepthThreeLowerBound.TapeUnaryCompareScan.result (m n : ℕ) : Ordering

Compare two natural numbers, returning their ordering.

Equations

• Complexity.DepthThreeLowerBound.TapeUnaryCompareScan.result m n = if m < n then Ordering.lt else if m = n then Ordering.eq else Ordering.gt

@[simp]

theorem Complexity.DepthThreeLowerBound.TapeUnaryCompareScan.result_succ (m n : ℕ) : result (m + 1) (n + 1) = result m n

theorem Complexity.DepthThreeLowerBound.TapeUnaryCompareScan.result_eq_lt_iff (m n : ℕ) : result m n = Ordering.lt ↔ m < n

theorem Complexity.DepthThreeLowerBound.TapeUnaryCompareScan.result_eq_eq_iff (m n : ℕ) : result m n = Ordering.eq ↔ m = n

theorem Complexity.DepthThreeLowerBound.TapeUnaryCompareScan.result_eq_gt_iff (m n : ℕ) : result m n = Ordering.gt ↔ n < m

def Complexity.DepthThreeLowerBound.TapeUnaryCompareScan.unaryCursor (k n : ℕ) : Turing.Tape TapeSymbol

A unary tape with a specified number of bits before and after the head.

Equations

• Complexity.DepthThreeLowerBound.TapeUnaryCompareScan.unaryCursor k n = Complexity.DepthThreeLowerBound.cursorTape (List.replicate k true) (List.replicate n true)

@[simp]

theorem Complexity.DepthThreeLowerBound.TapeUnaryCompareScan.unaryCursor_head_zero (k : ℕ) : (unaryCursor k 0).head = cleanAtom TapeAtom.endMark

@[simp]

theorem Complexity.DepthThreeLowerBound.TapeUnaryCompareScan.unaryCursor_head_succ (k n : ℕ) : (unaryCursor k (n + 1)).head = rawInputSymbol true

theorem Complexity.DepthThreeLowerBound.TapeUnaryCompareScan.unaryCursor_right (k n : ℕ) : Turing.Tape.move Turing.Dir.right (unaryCursor k (n + 1)) = unaryCursor (k + 1) n

def Complexity.DepthThreeLowerBound.TapeUnaryCompareScan.pairTapes (r s : TapeRegister) (T : TapeTapes) (R S : Turing.Tape TapeSymbol) : TapeTapes

Replace the tapes at two selected registers.

Equations

• Complexity.DepthThreeLowerBound.TapeUnaryCompareScan.pairTapes r s T R S = Function.update (Function.update T r R) s S

@[simp]

theorem Complexity.DepthThreeLowerBound.TapeUnaryCompareScan.pairTapes_r {r s : TapeRegister} (hrs : r ≠ s) (T : TapeTapes) (R S : Turing.Tape TapeSymbol) : pairTapes r s T R S r = R

@[simp]

theorem Complexity.DepthThreeLowerBound.TapeUnaryCompareScan.pairTapes_s (r s : TapeRegister) (T : TapeTapes) (R S : Turing.Tape TapeSymbol) : pairTapes r s T R S s = S

theorem Complexity.DepthThreeLowerBound.TapeUnaryCompareScan.pairTapes_other (r s : TapeRegister) (T : TapeTapes) (R S : Turing.Tape TapeSymbol) (j : TapeRegister) (hjr : j ≠ r) (hjs : j ≠ s) : pairTapes r s T R S j = T j

theorem Complexity.DepthThreeLowerBound.TapeUnaryCompareScan.update_pairTapes_r {r s : TapeRegister} (hrs : r ≠ s) (T : TapeTapes) (R S R' : Turing.Tape TapeSymbol) : Function.update (pairTapes r s T R S) r R' = pairTapes r s T R' S

theorem Complexity.DepthThreeLowerBound.TapeUnaryCompareScan.update_pairTapes_s (r s : TapeRegister) (T : TapeTapes) (R S S' : Turing.Tape TapeSymbol) : Function.update (pairTapes r s T R S) s S' = pairTapes r s T R S'

def Complexity.DepthThreeLowerBound.TapeUnaryCompareScan.scanTapes (r s : TapeRegister) (T : TapeTapes) (k m n : ℕ) : TapeTapes

The pair of unary tapes during their synchronized comparison scan.

Equations

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

theorem Complexity.DepthThreeLowerBound.TapeUnaryCompareScan.scanTapes_other (r s : TapeRegister) (T : TapeTapes) (k m n : ℕ) (j : TapeRegister) (hjr : j ≠ r) (hjs : j ≠ s) : scanTapes r s T k m n j = T j

def Complexity.DepthThreeLowerBound.TapeUnaryCompareScan.code (r s : TapeRegister) : TapeMultiProgram State

Transition function of the unary compare scan routine.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.DepthThreeLowerBound.TapeUnaryCompareScan.code r s (Complexity.DepthThreeLowerBound.TapeUnaryCompareScan.State.done result) x✝ = none

theorem Complexity.DepthThreeLowerBound.TapeUnaryCompareScan.step_scan_zero_zero {r s : TapeRegister} (hrs : r ≠ s) (T : TapeTapes) (k : ℕ) : (code r s).step (TapeMultiProgram.cfg State.scan (scanTapes r s T k 0 0)) = some (TapeMultiProgram.cfg (State.done Ordering.eq) (scanTapes r s T k 0 0))

theorem Complexity.DepthThreeLowerBound.TapeUnaryCompareScan.step_scan_zero_succ {r s : TapeRegister} (hrs : r ≠ s) (T : TapeTapes) (k n : ℕ) : (code r s).step (TapeMultiProgram.cfg State.scan (scanTapes r s T k 0 (n + 1))) = some (TapeMultiProgram.cfg (State.done Ordering.lt) (scanTapes r s T k 0 (n + 1)))

theorem Complexity.DepthThreeLowerBound.TapeUnaryCompareScan.step_scan_succ_zero {r s : TapeRegister} (hrs : r ≠ s) (T : TapeTapes) (k m : ℕ) : (code r s).step (TapeMultiProgram.cfg State.scan (scanTapes r s T k (m + 1) 0)) = some (TapeMultiProgram.cfg (State.done Ordering.gt) (scanTapes r s T k (m + 1) 0))

theorem Complexity.DepthThreeLowerBound.TapeUnaryCompareScan.step_scan_succ_succ {r s : TapeRegister} (hrs : r ≠ s) (T : TapeTapes) (k m n : ℕ) : (code r s).step (TapeMultiProgram.cfg State.scan (scanTapes r s T k (m + 1) (n + 1))) = some (TapeMultiProgram.cfg State.advanceS (pairTapes r s T (unaryCursor (k + 1) m) (unaryCursor k (n + 1))))

theorem Complexity.DepthThreeLowerBound.TapeUnaryCompareScan.step_advanceS (r s : TapeRegister) (T : TapeTapes) (R S : Turing.Tape TapeSymbol) : (code r s).step (TapeMultiProgram.cfg State.advanceS (pairTapes r s T R S)) = some (TapeMultiProgram.cfg State.scan (pairTapes r s T R (Turing.Tape.move Turing.Dir.right S)))

theorem Complexity.DepthThreeLowerBound.TapeUnaryCompareScan.runs_scan {r s : TapeRegister} (hrs : r ≠ s) (T : TapeTapes) (k m n : ℕ) : RunsIn (code r s).step (TapeMultiProgram.cfg State.scan (scanTapes r s T k m n)) (TapeMultiProgram.cfg (State.done (result m n)) (scanTapes r s T (k + min m n) (m - min m n) (n - min m n))) (2 * min m n + 1)

theorem Complexity.DepthThreeLowerBound.TapeUnaryCompareScan.runs_entry {r s : TapeRegister} (hrs : r ≠ s) (T : TapeTapes) (m n : ℕ) (hR : T r = wordTape (List.replicate m true)) (hS : T s = wordTape (List.replicate n true)) : RunsIn (code r s).step (TapeMultiProgram.cfg State.beginR T) (TapeMultiProgram.cfg State.scan (scanTapes r s T 0 m n)) 2

theorem Complexity.DepthThreeLowerBound.TapeUnaryCompareScan.runs_compare {r s : TapeRegister} (hrs : r ≠ s) (T : TapeTapes) (m n : ℕ) (hR : T r = wordTape (List.replicate m true)) (hS : T s = wordTape (List.replicate n true)) : RunsIn (code r s).step (TapeMultiProgram.cfg State.beginR T) (TapeMultiProgram.cfg (State.done (result m n)) (scanTapes r s T (min m n) (m - min m n) (n - min m n))) (2 * min m n + 3)

theorem Complexity.DepthThreeLowerBound.TapeUnaryCompareScan.prefix_append_left (m n : ℕ) : List.replicate (min m n) true ++ List.replicate (m - min m n) true = List.replicate m true

theorem Complexity.DepthThreeLowerBound.TapeUnaryCompareScan.prefix_append_right (m n : ℕ) : List.replicate (min m n) true ++ List.replicate (n - min m n) true = List.replicate n true

@[simp]

theorem Complexity.DepthThreeLowerBound.TapeUnaryCompareScan.step_done (r s : TapeRegister) (T : TapeTapes) (o : Ordering) : (code r s).step (TapeMultiProgram.cfg (State.done o) T) = none