Rational hitting lists: output adapter

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/RationalHitting/OutputAdapter.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.OutputAdapter.A : Type

The fixed four-symbol alphabet of the tape adapter.

Equations

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

@[reducible, inline]

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

The ten control states used by the tape adapter.

Equations

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

@[reducible, inline]

abbrev Complexity.RationalHitting.TMTime.OutputAdapter.Word (b : ℕ) : Type

A fixed-width encoded block stored in the finite control.

Equations

• Complexity.RationalHitting.TMTime.OutputAdapter.Word b = (Fin b → Bool)

@[reducible, inline]

abbrev Complexity.RationalHitting.TMTime.OutputAdapter.V (b : ℕ) : Type

Finite auxiliary storage used by the tape adapter.

Equations

• Complexity.RationalHitting.TMTime.OutputAdapter.V b = (Complexity.RationalHitting.TMTime.OutputAdapter.Word b × Option Bool)

@[reducible, inline]

abbrev Complexity.RationalHitting.TMTime.OutputAdapter.Stmt (b : ℕ) : Type

A tape-adapter instruction with finite auxiliary storage.

Equations

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

@[reducible, inline]

abbrev Complexity.RationalHitting.TMTime.OutputAdapter.Cfg (b : ℕ) : Type

A configuration of the tape adapter.

Equations

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

def Complexity.RationalHitting.TMTime.OutputAdapter.raw (x : Bool) : A

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

Equations

• Complexity.RationalHitting.TMTime.OutputAdapter.raw x = if x = true then 2 else 1

def Complexity.RationalHitting.TMTime.OutputAdapter.bit (x : Bool) : A

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

Equations

• Complexity.RationalHitting.TMTime.OutputAdapter.bit x = if x = true then 1 else 0

def Complexity.RationalHitting.TMTime.OutputAdapter.jump {b : ℕ} (q : Q) : Stmt b

Jump to the specified adapter control state.

Equations

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

def Complexity.RationalHitting.TMTime.OutputAdapter.move {b : ℕ} (d : Turing.Dir) (q : Q) : Stmt b

Move the tape head and jump to the specified state.

Equations

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

def Complexity.RationalHitting.TMTime.OutputAdapter.leftTo {b : ℕ} (q r : Q) : Stmt b

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.OutputAdapter.readBlock {b : ℕ} : List (Fin b) → Stmt b → Stmt b

Read the designated block coordinates into the finite auxiliary storage.

Equations

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

def Complexity.RationalHitting.TMTime.OutputAdapter.block {b : ℕ} (w : Word b) : List A

Write a fixed-width Boolean block as tape symbols.

Equations

• Complexity.RationalHitting.TMTime.OutputAdapter.block w = List.map (fun (i : Fin b) => Complexity.RationalHitting.TMTime.OutputAdapter.bit (w i)) (List.finRange b)

def Complexity.RationalHitting.TMTime.OutputAdapter.fill {b : ℕ} (is : List (Fin b)) (w v : Word b) : Word b

Copy the designated coordinates from one stored block to another.

Equations

• Complexity.RationalHitting.TMTime.OutputAdapter.fill is w v = List.foldl (fun (u : Complexity.RationalHitting.TMTime.OutputAdapter.Word b) (i : Fin b) => Function.update u i (w i)) v is

theorem Complexity.RationalHitting.TMTime.OutputAdapter.fill_apply {b : ℕ} (is : List (Fin b)) (w v : Word b) (j : Fin b) : fill is w v j = if j ∈ is then w j else v j

@[simp]

theorem Complexity.RationalHitting.TMTime.OutputAdapter.fill_all {b : ℕ} (w v : Word b) : fill (List.finRange b) w v = w

@[simp]

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

theorem Complexity.RationalHitting.TMTime.OutputAdapter.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.OutputAdapter.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)

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

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

@[simp]

theorem Complexity.RationalHitting.TMTime.OutputAdapter.bit_beq_one (x : Bool) : (bit x == 1) = x

@[simp]

theorem Complexity.RationalHitting.TMTime.OutputAdapter.bit_ne_three (x : Bool) : bit x ≠ 3

@[simp]

theorem Complexity.RationalHitting.TMTime.OutputAdapter.raw_ne_three (x : Bool) : raw x ≠ 3

theorem Complexity.RationalHitting.TMTime.OutputAdapter.readBlock_spec {b : ℕ} (is : List (Fin b)) (w v : Word b) (x : Option Bool) (q : Stmt b) (L R : List A) : Turing.TM1.stepAux (readBlock is q) (v, x) (Turing.Tape.mk₂ L (List.map (fun (i : Fin b) => bit (w i)) is ++ R)) = Turing.TM1.stepAux q (fill is w v, x) (Turing.Tape.mk₂ (List.replicate is.length 0 ++ L) R)

def Complexity.RationalHitting.TMTime.OutputAdapter.machine {b : ℕ} (get : Word b → Option Bool) : Q → Stmt b

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.OutputAdapter.machine get 2 = Complexity.RationalHitting.TMTime.OutputAdapter.leftTo 2 3
• Complexity.RationalHitting.TMTime.OutputAdapter.machine get 5 = Complexity.RationalHitting.TMTime.OutputAdapter.leftTo 5 6
• Complexity.RationalHitting.TMTime.OutputAdapter.machine get 7 = Complexity.RationalHitting.TMTime.OutputAdapter.leftTo 7 8

def Complexity.RationalHitting.TMTime.OutputAdapter.state {b : ℕ} (q : Q) (v : V b) (L R : List A) : Cfg b

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

Equations

• Complexity.RationalHitting.TMTime.OutputAdapter.state q v L R = { l := some q, var := v, Tape := Turing.Tape.mk₂ L R }

def Complexity.RationalHitting.TMTime.OutputAdapter.invariant {b : ℕ} (gap : ℕ) (out : List Bool) (R : List A) (v : V b) : Cfg b

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.OutputAdapter.scan_right {b : ℕ} (F : Q → Stmt b) (q : Q) (v : V b) (l L R : List A) (h : ∀ a ∈ l, ∀ (L R : List A), Turing.TM1.step F (state q v L (a :: R)) = some (state q v (a :: L) R)) : exec (Turing.TM1.step F) l.length (state q v L (l ++ R)) = some (state q v (l.reverse ++ L) R)

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

theorem Complexity.RationalHitting.TMTime.OutputAdapter.zeros_cons (k : ℕ) (L : List A) : List.replicate k 0 ++ 0 :: L = 0 :: (List.replicate k 0 ++ L)

theorem Complexity.RationalHitting.TMTime.OutputAdapter.consume_some {b : ℕ} (get : Word b → Option Bool) (w : Word b) (x : Bool) (hx : get w = some x) (gap : ℕ) (out : List Bool) (R : List A) (v : V b) : exec (Turing.TM1.step (machine get)) 1 (invariant gap out (block w ++ R) v) = some (state 2 (w, some x) (List.replicate (gap + b) 0 ++ 3 :: List.map raw out.reverse ++ [3]) (3 :: R))

theorem Complexity.RationalHitting.TMTime.OutputAdapter.emit_one {b : ℕ} (hb : 1 ≤ b) (get : Word b → Option Bool) (w : Word b) (x : Bool) (hx : get w = some x) (gap : ℕ) (out : List Bool) (R : List A) (v : V b) : exec (Turing.TM1.step (machine get)) (2 * (gap + b) + 3) (invariant gap out (block w ++ R) v) = some (invariant (gap + b - 1) (out ++ [x]) R (w, some x))

theorem Complexity.RationalHitting.TMTime.OutputAdapter.consume_none {b : ℕ} (get : Word b → Option Bool) (w : Word b) (hx : get w = none) (gap : ℕ) (out : List Bool) (v : V b) : exec (Turing.TM1.step (machine get)) 1 (invariant gap out (block w) v) = some (state 5 (w, none) (List.replicate (gap + b + 1) 0 ++ 3 :: List.map raw out.reverse ++ [3]) [])

theorem Complexity.RationalHitting.TMTime.OutputAdapter.clear_blanks (l r : ℕ) (w : List A) : Turing.Tape.mk₂ (List.replicate l 0) (w ++ List.replicate r 0) = Turing.Tape.mk₁ w

theorem Complexity.RationalHitting.TMTime.OutputAdapter.finish {b : ℕ} (get : Word b → Option Bool) (w : Word b) (hx : get w = none) (gap : ℕ) (out : List Bool) (v : V b) : exec (Turing.TM1.step (machine get)) (gap + b + out.length + 6) (invariant gap out (block w) v) = some { l := none, var := (w, none), Tape := Turing.Tape.mk₁ (List.map raw out) }

def Complexity.RationalHitting.TMTime.OutputAdapter.stream {b : ℕ} (code : Bool → Bool → Word b) (stop : Bool → Word b) : Bool → List Bool → List A

Encode a sequence of bits and its terminal block.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.RationalHitting.TMTime.OutputAdapter.stream code stop x✝ [] = Complexity.RationalHitting.TMTime.OutputAdapter.block (stop x✝)

def Complexity.RationalHitting.TMTime.OutputAdapter.cost (b gap len : ℕ) : ℕ → ℕ

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

Equations

• Complexity.RationalHitting.TMTime.OutputAdapter.cost b gap len 0 = gap + b + len + 6
• Complexity.RationalHitting.TMTime.OutputAdapter.cost b gap len n.succ = 2 * (gap + b) + 3 + Complexity.RationalHitting.TMTime.OutputAdapter.cost b (gap + b - 1) (len + 1) n

theorem Complexity.RationalHitting.TMTime.OutputAdapter.decode_stream {b : ℕ} (hb : 1 ≤ b) (get : Word b → Option Bool) (code : Bool → Bool → Word b) (stop : Bool → Word b) (hc : ∀ (f x : Bool), get (code f x) = some x) (hs : ∀ (f : Bool), get (stop f) = none) (xs : List Bool) (f : Bool) (gap : ℕ) (out : List Bool) (v : V b) : ∃ (u : V b), exec (Turing.TM1.step (machine get)) (cost b gap out.length xs.length) (invariant gap out (stream code stop f xs) v) = some { l := none, var := u, Tape := Turing.Tape.mk₁ (List.map raw (out ++ xs)) }

theorem Complexity.RationalHitting.TMTime.OutputAdapter.cost_bound (b gap len n : ℕ) : cost b gap len n ≤ (n + 1) * (3 * (gap + b * (n + 1) + len + n + 10))

theorem Complexity.RationalHitting.TMTime.OutputAdapter.start {b : ℕ} (get : Word b → Option Bool) (R : List A) (v : V b) : exec (Turing.TM1.step (machine get)) 1 { l := some 0, var := v, Tape := Turing.Tape.mk₁ R } = some (invariant 0 [] R v)

theorem Complexity.RationalHitting.TMTime.OutputAdapter.prepare {b : ℕ} (hb : 1 ≤ b) (get : Word b → Option Bool) (code : Bool → Bool → Word b) (stop : Bool → Word b) (hc : ∀ (f x : Bool), get (code f x) = some x) (hs : ∀ (f : Bool), get (stop f) = none) (xs : List Bool) : ∃ t ≤ (3 * b + 34) * (xs.length + 1) ^ 2, ∃ (u : V b), exec (Turing.TM1.step (machine get)) t (Turing.TM1.init (stream code stop true xs)) = some { l := none, var := u, Tape := Turing.Tape.mk₁ (List.map raw xs) }

Literal block input to literal digit output; both head position and blank outside the output are guaranteed, with quadratic bit-time.

theorem Complexity.RationalHitting.TMTime.OutputAdapter.finite_output {b : ℕ} (hb : 1 ≤ b) (get : Word b → Option Bool) (code : Bool → Bool → Word b) (stop : Bool → Word b) (hc : ∀ (f x : Bool), get (code f x) = some x) (hs : ∀ (f : Bool), get (stop f) = none) : ∃ (m : ℕ) (G : Turing.TM0.Machine A (Fin (m + 1))) (C : ℕ), 0 < C ∧ ∀ (xs : List Bool), ∃ t ≤ C * (xs.length + 1) ^ 2, ∃ (a : Turing.TM0.Cfg A (Fin (m + 1))), exec (Turing.TM0.step G) t (Turing.TM0.init (stream code stop true xs)) = some a ∧ Turing.TM0.step G a = none ∧ a.Tape = Turing.Tape.mk₁ (List.map raw xs)

A genuine Fin4 finite TM0 output transducer; the encoding/decoding functions are fixed finite tables and no unbounded state or oracle is used.

theorem Complexity.RationalHitting.TMTime.StackTape.unique {K : Type u_1} {Λ : Type u_2} {σ : Type u_3} {Γ : K → Type u_4} {a b : Turing.TM2.Cfg Γ Λ σ} {c d : Turing.TM1.Cfg (Turing.TM2to1.Γ' K Γ) (Turing.TM2to1.Λ' K Γ Λ σ) σ} (h : Turing.TM2to1.TrCfg a c) (h' : Turing.TM2to1.TrCfg b d) (hs : a.stk = b.stk) : c.Tape = d.Tape

At the boundary of a stack macrostep, the simulator's tape is determined by the actual stack contents. There is no junk-cell assumption.

theorem Complexity.RationalHitting.TMTime.StackTape.clean {K : Type u_1} {Λ : Type u_2} {σ : Type u_3} [DecidableEq K] [Inhabited Λ] [Inhabited σ] (k : K) (w : List Bool) {c : Turing.TM1.Cfg (Turing.TM2to1.Γ' K fun (x : K) => Bool) (Turing.TM2to1.Λ' K (fun (x : K) => Bool) Λ σ) σ} (h : Turing.TM2to1.TrCfg { l := none, var := default, stk := Function.update (fun (x : K) => []) k w } c) : c.Tape = Turing.Tape.mk₁ (Turing.TM2to1.trInit k w)

theorem Complexity.RationalHitting.TMTime.OutputAdapter.blockVector {b : ℕ} (v : List.Vector Bool b) : block v.get = List.map bit v.toList

@[reducible, inline]

abbrev Complexity.RationalHitting.TMTime.OutputAdapter.StackAlphabet (K : Type) : Type

The tape alphabet encoding a marked family of Boolean stacks.

Equations

• Complexity.RationalHitting.TMTime.OutputAdapter.StackAlphabet K = Turing.TM2to1.Γ' K fun (x : K) => Bool

def Complexity.RationalHitting.TMTime.OutputAdapter.code {K : Type} [DecidableEq K] {b : ℕ} (k : K) (enc : StackAlphabet K → List.Vector Bool b) (f x : Bool) : Word b

Encode a stack cell holding one bit in the selected register.

Equations

• Complexity.RationalHitting.TMTime.OutputAdapter.code k enc f x = (enc (f, Function.update (fun (x : K) => none) k (some x))).get

def Complexity.RationalHitting.TMTime.OutputAdapter.stop {K : Type} {b : ℕ} (enc : StackAlphabet K → List.Vector Bool b) (f : Bool) : Word b

Encode a terminal cell with all stacks empty.

Equations

• Complexity.RationalHitting.TMTime.OutputAdapter.stop enc f = (enc (f, fun (x : K) => none)).get

def Complexity.RationalHitting.TMTime.OutputAdapter.getter {K : Type} {b : ℕ} (k : K) (dec : List.Vector Bool b → StackAlphabet K) (w : Word b) : Option Bool

Decode the selected stack's bit from a fixed-width encoded block.

Equations

• Complexity.RationalHitting.TMTime.OutputAdapter.getter k dec w = (dec (List.Vector.ofFn w)).2 k

theorem Complexity.RationalHitting.TMTime.OutputAdapter.getter_code {K : Type} [DecidableEq K] {b : ℕ} (k : K) (enc : StackAlphabet K → List.Vector Bool b) (dec : List.Vector Bool b → StackAlphabet K) (hd : ∀ (a : StackAlphabet K), dec (enc a) = a) (f x : Bool) : getter k dec (code k enc f x) = some x

theorem Complexity.RationalHitting.TMTime.OutputAdapter.getter_stop {K : Type} {b : ℕ} (k : K) (enc : StackAlphabet K → List.Vector Bool b) (dec : List.Vector Bool b → StackAlphabet K) (hd : ∀ (a : StackAlphabet K), dec (enc a) = a) (f : Bool) : getter k dec (stop enc f) = none

theorem Complexity.RationalHitting.TMTime.OutputAdapter.stream_false {K : Type} [DecidableEq K] {b : ℕ} (k : K) (enc : StackAlphabet K → List.Vector Bool b) (xs : List Bool) : stream (code k enc) (stop enc) false xs = List.map bit (List.flatMap (fun (x : (fun (x : K) => Bool) k) => (enc (false, Function.update (fun (x : K) => none) k (some x))).toList) xs) ++ block (stop enc false)

theorem Complexity.RationalHitting.TMTime.OutputAdapter.stream_encoding {K : Type} [DecidableEq K] {b : ℕ} (k : K) (enc : StackAlphabet K → List.Vector Bool b) (h0 : enc default = List.Vector.replicate b false) (xs : List Bool) : Turing.Tape.mk₁ (stream (code k enc) (stop enc) true xs) = Turing.Tape.mk₁ (List.map bit (List.flatMap (fun (z : StackAlphabet K) => (enc z).toList) (Turing.TM2to1.trInit k xs.reverse)))

theorem Complexity.RationalHitting.TMTime.OutputAdapter.width_pos {K : Type} {b : ℕ} (enc : StackAlphabet K → List.Vector Bool b) (dec : List.Vector Bool b → StackAlphabet K) (hd : ∀ (a : StackAlphabet K), dec (enc a) = a) : 1 ≤ b

theorem Complexity.RationalHitting.TMTime.OutputAdapter.raw_stack_output {K : Type} [DecidableEq K] {b : ℕ} (k : K) (enc : StackAlphabet K → List.Vector Bool b) (dec : List.Vector Bool b → StackAlphabet K) (h0 : enc default = List.Vector.replicate b false) (hd : ∀ (a : StackAlphabet K), dec (enc a) = a) : ∃ (m : ℕ) (G : Turing.TM0.Machine A (Fin (m + 1))) (C : ℕ), 0 < C ∧ ∀ (xs : List Bool), ∃ t ≤ C * (xs.length + 1) ^ 2, ∃ (a : Turing.TM0.Cfg A (Fin (m + 1))), exec (Turing.TM0.step G) t (Turing.TM0.init (List.map bit (List.flatMap (fun (z : StackAlphabet K) => (enc z).toList) (Turing.TM2to1.trInit k xs.reverse)))) = some a ∧ Turing.TM0.step G a = none ∧ a.Tape = Turing.Tape.mk₁ (List.map raw xs)

Exact inverse interface for a clean output stack, including the bottom marker, right-side blank padding and output order.