Rational hitting lists: input adapter

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

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

@[reducible, inline]

abbrev Complexity.RationalHitting.TMTime.InputAdapter.A : Type

The fixed four-symbol alphabet of the tape adapter.

Equations

• Complexity.RationalHitting.TMTime.InputAdapter.A = Fin 4

@[reducible, inline]

abbrev Complexity.RationalHitting.TMTime.InputAdapter.Q : Type

The ten control states used by the tape adapter.

Equations

• Complexity.RationalHitting.TMTime.InputAdapter.Q = Fin 10

@[reducible, inline]

abbrev Complexity.RationalHitting.TMTime.InputAdapter.V : Type

Finite auxiliary storage used by the tape adapter.

Equations

• Complexity.RationalHitting.TMTime.InputAdapter.V = (Bool × Bool)

@[reducible, inline]

abbrev Complexity.RationalHitting.TMTime.InputAdapter.Cfg : Type

A configuration of the tape adapter.

Equations

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

@[reducible, inline]

abbrev Complexity.RationalHitting.TMTime.InputAdapter.Stmt : Type

A tape-adapter instruction with finite auxiliary storage.

Equations

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

def Complexity.RationalHitting.TMTime.InputAdapter.raw (b : Bool) : A

Encode a literal output or input bit by a nonblank tape symbol.

Equations

• Complexity.RationalHitting.TMTime.InputAdapter.raw b = if b = true then 2 else 1

def Complexity.RationalHitting.TMTime.InputAdapter.bit (b : Bool) : A

Encode a bit inside the compiler's binary tape representation.

Equations

• Complexity.RationalHitting.TMTime.InputAdapter.bit b = if b = true then 1 else 0

def Complexity.RationalHitting.TMTime.InputAdapter.jump (q : Q) : Stmt

Jump to the specified adapter control state.

Equations

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

def Complexity.RationalHitting.TMTime.InputAdapter.move (d : Turing.Dir) (q : Q) : Stmt

Move the tape head and jump to the specified state.

Equations

• Complexity.RationalHitting.TMTime.InputAdapter.move d q = Turing.TM1.Stmt.move d (Complexity.RationalHitting.TMTime.InputAdapter.jump q)

def Complexity.RationalHitting.TMTime.InputAdapter.leftTo (q r : Q) : Stmt

Move left and branch according to whether the delimiter was reached.

Equations

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

def Complexity.RationalHitting.TMTime.InputAdapter.writeBits : List Bool → Stmt → Stmt

Write a finite encoded block before continuing with the next instruction.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.RationalHitting.TMTime.InputAdapter.writeBits [] x✝ = x✝

def Complexity.RationalHitting.TMTime.InputAdapter.machine (code : Bool → Bool → List Bool) : Q → Stmt

The fixed finite control map of the tape adapter.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.RationalHitting.TMTime.InputAdapter.machine code 4 = Complexity.RationalHitting.TMTime.InputAdapter.leftTo 4 5
• Complexity.RationalHitting.TMTime.InputAdapter.machine code 5 = Complexity.RationalHitting.TMTime.InputAdapter.leftTo 5 1
• Complexity.RationalHitting.TMTime.InputAdapter.machine code 8 = Complexity.RationalHitting.TMTime.InputAdapter.leftTo 8 9

@[simp]

theorem Complexity.RationalHitting.TMTime.InputAdapter.head₂ (L R : List A) : (Turing.Tape.mk₂ L R).head = R.headI

@[simp]

theorem Complexity.RationalHitting.TMTime.InputAdapter.right₂ (L : List A) (a : A) (R : List A) : Turing.Tape.move Turing.Dir.right (Turing.Tape.mk₂ L (a :: R)) = Turing.Tape.mk₂ (a :: L) R

theorem Complexity.RationalHitting.TMTime.InputAdapter.left₂ (a : A) (L R : List A) : Turing.Tape.move Turing.Dir.left (Turing.Tape.mk₂ (a :: L) R) = Turing.Tape.mk₂ L (a :: R)

@[simp]

theorem Complexity.RationalHitting.TMTime.InputAdapter.write₂ (L R : List A) (a : A) : Turing.Tape.write a (Turing.Tape.mk₂ L R) = Turing.Tape.mk₂ L (a :: R.tail)

theorem Complexity.RationalHitting.TMTime.InputAdapter.stepAux_writeBits (bs : List Bool) (q : Stmt) (v : V) (L R : List A) : Turing.TM1.stepAux (writeBits bs q) v (Turing.Tape.mk₂ L R) = Turing.TM1.stepAux q v (Turing.Tape.mk₂ ((List.map bit bs).reverse ++ L) (List.drop bs.length R))

theorem Complexity.RationalHitting.TMTime.InputAdapter.scan_right (F : Q → Stmt) (q : Q) (v : V) (l L R : List A) (h : ∀ a ∈ l, ∀ (L R : List A), Turing.TM1.step F { l := some q, var := v, Tape := Turing.Tape.mk₂ L (a :: R) } = some { l := some q, var := v, Tape := Turing.Tape.mk₂ (a :: L) R }) : exec (Turing.TM1.step F) l.length { l := some q, var := v, Tape := Turing.Tape.mk₂ L (l ++ R) } = some { l := some q, var := v, Tape := Turing.Tape.mk₂ (l.reverse ++ L) R }

theorem Complexity.RationalHitting.TMTime.InputAdapter.scan_left (F : Q → Stmt) (q r : Q) (v : V) (l L R : List A) (hF : F q = leftTo q r) (hl : ∀ a ∈ l, a ≠ 3) : exec (Turing.TM1.step F) (l.length + 1) { l := some q, var := v, Tape := Turing.Tape.mk₂ (l ++ 3 :: L) R } = some { l := some r, var := v, Tape := Turing.Tape.mk₂ L (3 :: l.reverse ++ R) }

@[simp]

theorem Complexity.RationalHitting.TMTime.InputAdapter.bit_ne_three (b : Bool) : bit b ≠ 3

@[simp]

theorem Complexity.RationalHitting.TMTime.InputAdapter.raw_ne_zero (b : Bool) : raw b ≠ 0

def Complexity.RationalHitting.TMTime.InputAdapter.state (q : Q) (f b : Bool) (L R : List A) : Cfg

Assemble a configuration from the control state and the two tape halves.

Equations

• Complexity.RationalHitting.TMTime.InputAdapter.state q f b L R = { l := some q, var := (f, b), Tape := Turing.Tape.mk₂ L R }

def Complexity.RationalHitting.TMTime.InputAdapter.invariant (xs : List Bool) (k : ℕ) (out : List Bool) (f b : Bool) : Cfg

The tape layout preserved by the adapter's main scanning loop.

Equations

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

theorem Complexity.RationalHitting.TMTime.InputAdapter.process (code : Bool → Bool → List Bool) (x f b : Bool) (xs out : List Bool) (k : ℕ) : exec (Turing.TM1.step (machine code)) (2 * k + 2 * out.length + (code f x).length + 7) (invariant (x :: xs) k out f b) = some (invariant xs (k + 1) (out ++ code f x) false x)

def Complexity.RationalHitting.TMTime.InputAdapter.emit (code : Bool → Bool → List Bool) : Bool → List Bool → List Bool

Encode all literal input bits, using a distinguished first-block marker.

Equations

• Complexity.RationalHitting.TMTime.InputAdapter.emit code x✝ [] = []
• Complexity.RationalHitting.TMTime.InputAdapter.emit code x✝ (x_2 :: xs) = code x✝ x_2 ++ Complexity.RationalHitting.TMTime.InputAdapter.emit code false xs

def Complexity.RationalHitting.TMTime.InputAdapter.cost (code : Bool → Bool → List Bool) : Bool → List Bool → ℕ → ℕ → ℕ

Exact recursive step bound for the adapter's scanning loop.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.RationalHitting.TMTime.InputAdapter.cost code x✝² [] x✝¹ x✝ = 0

theorem Complexity.RationalHitting.TMTime.InputAdapter.all_process (code : Bool → Bool → List Bool) (xs out : List Bool) (k : ℕ) (f b : Bool) : ∃ (f' : Bool) (b' : Bool), exec (Turing.TM1.step (machine code)) (cost code f xs k out.length) (invariant xs k out f b) = some (invariant [] (k + xs.length) (out ++ emit code f xs) f' b')

theorem Complexity.RationalHitting.TMTime.InputAdapter.emit_length (code : Bool → Bool → List Bool) (B : ℕ) (hb : ∀ (f x : Bool), (code f x).length ≤ B) (f : Bool) (xs : List Bool) : (emit code f xs).length ≤ B * xs.length

theorem Complexity.RationalHitting.TMTime.InputAdapter.cost_bound (code : Bool → Bool → List Bool) (B : ℕ) (hb : ∀ (f x : Bool), (code f x).length ≤ B) (f : Bool) (xs : List Bool) (k L : ℕ) : cost code f xs k L ≤ xs.length * (2 * (k + xs.length) + 2 * (L + B * xs.length) + B + 7)

@[simp]

theorem Complexity.RationalHitting.TMTime.InputAdapter.left_empty (R : List A) : Turing.Tape.move Turing.Dir.left (Turing.Tape.mk₂ [] R) = Turing.Tape.mk₂ [] (0 :: R)

theorem Complexity.RationalHitting.TMTime.InputAdapter.clear_blanks (O : List A) (k : ℕ) : Turing.Tape.mk₂ (List.replicate k 0) (O ++ [0]) = Turing.Tape.mk₁ O

theorem Complexity.RationalHitting.TMTime.InputAdapter.scan_six_zero (code : Bool → Bool → List Bool) (f b : Bool) (L R : List A) : Turing.TM1.step (machine code) (state 6 f b L (0 :: R)) = some (state 6 f b (0 :: L) R)

theorem Complexity.RationalHitting.TMTime.InputAdapter.enter_finish (code : Bool → Bool → List Bool) (out : List Bool) (k : ℕ) (f b : Bool) : exec (Turing.TM1.step (machine code)) 1 (invariant [] k out f b) = some (state 6 f b [] (List.replicate (k + 2) 0 ++ 3 :: List.map bit out ++ [3]))

theorem Complexity.RationalHitting.TMTime.InputAdapter.finish (code : Bool → Bool → List Bool) (out : List Bool) (k : ℕ) (f b : Bool) : exec (Turing.TM1.step (machine code)) (k + 2 * out.length + 7) (invariant [] k out f b) = some { l := none, var := (f, b), Tape := Turing.Tape.mk₁ (List.map bit out) }

theorem Complexity.RationalHitting.TMTime.InputAdapter.scan_zero_raw (code : Bool → Bool → List Bool) (x : Bool) (v : V) (L R : List A) : Turing.TM1.step (machine code) { l := some 0, var := v, Tape := Turing.Tape.mk₂ L (raw x :: R) } = some { l := some 0, var := v, Tape := Turing.Tape.mk₂ (raw x :: L) R }

theorem Complexity.RationalHitting.TMTime.InputAdapter.start_markers (code : Bool → Bool → List Bool) (w : List Bool) (v : V) : exec (Turing.TM1.step (machine code)) 1 { l := some 0, var := v, Tape := Turing.Tape.mk₂ (List.map raw w) [] } = some (invariant w 0 [] true false)

theorem Complexity.RationalHitting.TMTime.InputAdapter.start (code : Bool → Bool → List Bool) (w : List Bool) (v : V) : exec (Turing.TM1.step (machine code)) (w.length + 1) { l := some 0, var := v, Tape := Turing.Tape.mk₁ (List.map raw w) } = some (invariant w.reverse 0 [] true false)

theorem Complexity.RationalHitting.TMTime.InputAdapter.prepare (code : Bool → Bool → List Bool) (B : ℕ) (hb : ∀ (f x : Bool), (code f x).length ≤ B) (w : List Bool) (v : V) : ∃ t ≤ (4 * B + 12) * (w.length + 1) ^ 2, ∃ (v' : V), exec (Turing.TM1.step (machine code)) t { l := some 0, var := v, Tape := Turing.Tape.mk₁ (List.map raw w) } = some { l := none, var := v', Tape := Turing.Tape.mk₁ (List.map bit (emit code true w.reverse)) }

Literal Fin4 raw input is physically erased; no hidden encoded-input precondition is used. The macrotransition charge is quadratic; TM1 compilation adds a fixed multiplicative constant for this one fixed adapter machine.

theorem Complexity.RationalHitting.TMTime.InputAdapter.emit_false (code : Bool → Bool → List Bool) (xs : List Bool) : emit code false xs = List.flatMap (code false) xs

theorem Complexity.RationalHitting.TMTime.InputAdapter.stack_encoding {K : Type} [DecidableEq K] (k : K) (b : ℕ) (enc : (Turing.TM2to1.Γ' K fun (x : K) => Bool) → List.Vector Bool b) (w : List Bool) (hw : w ≠ []) : emit (fun (f x : Bool) => (enc (f, Function.update (fun (x : K) => none) k (some x))).toList) true w.reverse = List.flatMap (fun (a : Turing.TM2to1.Γ' K fun (x : K) => Bool) => (enc a).toList) (Turing.TM2to1.trInit k w)

theorem Complexity.RationalHitting.TMTime.InputAdapter.raw_stack_input {K : Type} [DecidableEq K] (k : K) (b : ℕ) (enc : (Turing.TM2to1.Γ' K fun (x : K) => Bool) → List.Vector Bool b) : ∃ (m : ℕ) (G : Turing.TM0.Machine A (Fin (m + 1))) (C : ℕ), 0 < C ∧ ∀ (w : List Bool), w ≠ [] → ∃ t ≤ C * (w.length + 1) ^ 2, ∃ (a : Turing.TM0.Cfg A (Fin (m + 1))), exec (Turing.TM0.step G) t (Turing.TM0.init (List.map raw w)) = some a ∧ Turing.TM0.step G a = none ∧ a.Tape = Turing.Tape.mk₁ (List.map bit (List.flatMap (fun (z : Turing.TM2to1.Γ' K fun (x : K) => Bool) => (enc z).toList) (Turing.TM2to1.trInit k w)))

Real finite TM0 raw-input adapter, at quadratic bit cost, reaching exactly Mathlib's initial tape for the binary stack simulator, not an assumed encoding.