Native control for binary-choice query passes

An initializer runs once, followed by one or more passes. At each pass boundary one native binary choice selects a deterministic pass routine. A blank continuation tape selects the finalizer; a nonblank one starts another pass. All routing steps preserve every tape and head.

The finite native control contains only the control states of the initializer, the two pass routines and the finalizer, together with two routing states. In particular, neither the abstract query state nor the history of choices is put in native control.

Main definitions

• Turing.NondeterministicQueryMachine.Native.State: native finite control.
• Turing.NondeterministicQueryMachine.Native.table: a binary-choice native transition table.
• Turing.NondeterministicQueryMachine.Native.machine: its ordinary nondeterministic machine.

Main results

• Turing.NondeterministicQueryMachine.Native.exists_runPath_iff: all native run paths are exactly finite coin replays, including halted self-loops.

inductive Turing.NondeterministicQueryMachine.Native.State (SI : Type) (SP : Bool → Type) (SF : Type) : Type

Native control for initialization, binary-choice passes, and finalization.

• init {SI : Type} {SP : Bool → Type} {SF : Type} (q : SI) : State SI SP SF

  The initializer is running.

• choose {SI : Type} {SP : Bool → Type} {SF : Type} : State SI SP SF

  Choose the next pass routine, without moving any head.

• pass {SI : Type} {SP : Bool → Type} {SF : Type} (choice : Bool) (q : SP choice) : State SI SP SF

  The selected deterministic pass is running.

• check {SI : Type} {SP : Bool → Type} {SF : Type} : State SI SP SF

  Read the continuation tape after a pass.

• finish {SI : Type} {SP : Bool → Type} {SF : Type} (q : SF) : State SI SP SF

  The finalizer is running.

instance Turing.NondeterministicQueryMachine.Native.instFiniteState {SI SF : Type} {SP : Bool → Type} [Finite SI] [∀ (b : Bool), Finite (SP b)] [Finite SF] : Finite (State SI SP SF)

def Turing.NondeterministicQueryMachine.Native.relabelAction {k : ℕ} {S S' : Type} (φ : Option S → Option S') (a : Action k Bool S) : Action k Bool S'

Relabel an action's optional next state, preserving all tape actions.

def Turing.NondeterministicQueryMachine.Native.routeAction {k : ℕ} {S : Type} (q : Option S) : Action k Bool S

A routing instruction changes control and leaves every head, tape and output unchanged.

def Turing.NondeterministicQueryMachine.Native.initState {SI SF : Type} {SP : Bool → Type} : Option SI → Option (State SI SP SF)

Embed initializer states, sending its halt to the first binary-choice boundary.

def Turing.NondeterministicQueryMachine.Native.passState {SI SF : Type} {SP : Bool → Type} (b : Bool) : Option (SP b) → Option (State SI SP SF)

Embed pass states, sending the halt to the continuation check.

def Turing.NondeterministicQueryMachine.Native.finishState {SI SF : Type} {SP : Bool → Type} : Option SF → Option (State SI SP SF)

Embed finalizer states, preserving the final halt.

noncomputable def Turing.NondeterministicQueryMachine.Native.instruction {k : ℕ} {SI SF : Type} {SP : Bool → Type} (I : MultiTapeTM k Bool SI) (P : (b : Bool) → MultiTapeTM k Bool (SP b)) (F : MultiTapeTM k Bool SF) (C : Fin k) (q : State SI SP SF) (input : Option Bool) (work : Fin k → Option Bool) (choice : Bool) : Action k Bool (State SI SP SF)

Native instruction under one binary choice. Only choose depends on the choice.

noncomputable def Turing.NondeterministicQueryMachine.Native.table {k : ℕ} {SI SF : Type} {SP : Bool → Type} (I : MultiTapeTM k Bool SI) (P : (b : Bool) → MultiTapeTM k Bool (SP b)) (F : MultiTapeTM k Bool SF) (C : Fin k) : MultiTapePTM k Bool (State SI SP SF)

The native binary-choice transition table. Its oracle type is empty.

noncomputable def Turing.NondeterministicQueryMachine.Native.machine {k : ℕ} {SI SF : Type} {SP : Bool → Type} (I : MultiTapeTM k Bool SI) (P : (b : Bool) → MultiTapeTM k Bool (SP b)) (F : MultiTapeTM k Bool SF) (C : Fin k) : MultiTapeNTM k Bool (State SI SP SF)

The ordinary native nondeterministic machine.

theorem Turing.NondeterministicQueryMachine.Native.exists_step {k : ℕ} {SI SF : Type} {SP : Bool → Type} (I : MultiTapeTM k Bool SI) (P : (b : Bool) → MultiTapeTM k Bool (SP b)) (F : MultiTapeTM k Bool SF) (C : Fin k) {input : List Bool} (c : Cfg k Bool (State SI SP SF) input) : ∃ (c' : Cfg k Bool (State SI SP SF) input), (machine I P F C).Step c c'

The finite native machine is never stuck, even away from its intended invariant.

theorem Turing.NondeterministicQueryMachine.Native.step_iff {k : ℕ} {SI SF : Type} {SP : Bool → Type} (I : MultiTapeTM k Bool SI) (P : (b : Bool) → MultiTapeTM k Bool (SP b)) (F : MultiTapeTM k Bool SF) (C : Fin k) {input : List Bool} {c c' : Cfg k Bool (State SI SP SF) input} : (machine I P F C).Step c c' ↔ ∃ (choice : Bool), MultiTapeTM.step c = c'

A native step is selected by one binary choice.

theorem Turing.NondeterministicQueryMachine.Native.exists_runPath_iff {k : ℕ} {SI SF : Type} {SP : Bool → Type} (I : MultiTapeTM k Bool SI) (P : (b : Bool) → MultiTapeTM k Bool (SP b)) (F : MultiTapeTM k Bool SF) (C : Fin k) {input : List Bool} {c c' : Cfg k Bool (State SI SP SF) input} {n : ℕ} : (∃ (p : (machine I P F C).RunPath input), RelSeries.head p = c ∧ p.length = n ∧ RelSeries.last p = c') ↔ ∃ (choices : List Bool), choices.length = n ∧ (table I P F C).stepCoins choices c = c'

Finite native paths are exactly finite coin replays. Coins are proof-level witnesses.

theorem Turing.NondeterministicQueryMachine.Native.tr_withCoin {k : ℕ} {SI SF : Type} {SP : Bool → Type} (I : MultiTapeTM k Bool SI) (P : (b : Bool) → MultiTapeTM k Bool (SP b)) (F : MultiTapeTM k Bool SF) (C : Fin k) (choice : Bool) (q : State SI SP SF) (input : Option Bool) (work : Fin k → Option Bool) : ((table I P F C).withCoin choice).toTM.tr q input work = instruction I P F C q input work choice

theorem Turing.NondeterministicQueryMachine.Native.apply_relabelAction {k : ℕ} {S S' : Type} {input : List Bool} (φ ψ : Option S → Option S') (a : Action k Bool S) (c : Cfg k Bool S input) : (relabelAction φ a).apply (Cfg.mapState ψ c) = Cfg.mapState φ (a.apply c)

Applying a relabeled action agrees with relabeling the resulting configuration. The old control state is never read by Action.apply.

theorem Turing.NondeterministicQueryMachine.Native.apply_routeAction {k : ℕ} {S : Type} {input : List Bool} (q : Option S) (c : Cfg k Bool S input) : (routeAction q).apply c = c.withState q

theorem Turing.NondeterministicQueryMachine.Native.step_init {k : ℕ} {SI SF : Type} {SP : Bool → Type} (I : MultiTapeTM k Bool SI) (P : (b : Bool) → MultiTapeTM k Bool (SP b)) (F : MultiTapeTM k Bool SF) (C : Fin k) {input : List Bool} (choice : Bool) (c : Cfg k Bool SI input) (h : ¬c.Halted) : MultiTapeTM.step (Cfg.mapState initState c) = Cfg.mapState initState (MultiTapeTM.step c)

The initializer is simulated step for step until its first halt.

theorem Turing.NondeterministicQueryMachine.Native.step_pass {k : ℕ} {SI SF : Type} {SP : Bool → Type} (I : MultiTapeTM k Bool SI) (P : (b : Bool) → MultiTapeTM k Bool (SP b)) (F : MultiTapeTM k Bool SF) (C : Fin k) {input : List Bool} (coin b : Bool) (c : Cfg k Bool (SP b) input) (h : ¬c.Halted) : MultiTapeTM.step (Cfg.mapState (passState b) c) = Cfg.mapState (passState b) (MultiTapeTM.step c)

A selected pass is deterministic until its first halt, regardless of subsequent coins.

theorem Turing.NondeterministicQueryMachine.Native.step_finish {k : ℕ} {SI SF : Type} {SP : Bool → Type} (I : MultiTapeTM k Bool SI) (P : (b : Bool) → MultiTapeTM k Bool (SP b)) (F : MultiTapeTM k Bool SF) (C : Fin k) {input : List Bool} (choice : Bool) (c : Cfg k Bool SF input) (h : ¬c.Halted) : MultiTapeTM.step (Cfg.mapState finishState c) = Cfg.mapState finishState (MultiTapeTM.step c)

The finalizer is simulated step for step, with its halt preserved.

theorem Turing.NondeterministicQueryMachine.Native.step_choose {k : ℕ} {SI SF : Type} {SP : Bool → Type} (I : MultiTapeTM k Bool SI) (P : (b : Bool) → MultiTapeTM k Bool (SP b)) (F : MultiTapeTM k Bool SF) (C : Fin k) {input : List Bool} (choice : Bool) (c : Cfg k Bool (State SI SP SF) input) (h : c.state = some State.choose) : MultiTapeTM.step c = c.withState (some (State.pass choice (P choice).q₀))

The choice step selects a routine without storing any earlier choices or moving a head.

theorem Turing.NondeterministicQueryMachine.Native.step_check {k : ℕ} {SI SF : Type} {SP : Bool → Type} (I : MultiTapeTM k Bool SI) (P : (b : Bool) → MultiTapeTM k Bool (SP b)) (F : MultiTapeTM k Bool SF) (C : Fin k) {input : List Bool} (choice : Bool) (c : Cfg k Bool (State SI SP SF) input) (h : c.state = some State.check) : MultiTapeTM.step c = c.withState (some (if (c.workTapeSymbols C).isSome = true then State.choose else State.finish F.q₀))

The continuation check changes only native control.

theorem Turing.NondeterministicQueryMachine.Native.step_pass_iff {k : ℕ} {SI SF : Type} {SP : Bool → Type} (I : MultiTapeTM k Bool SI) (P : (b : Bool) → MultiTapeTM k Bool (SP b)) (F : MultiTapeTM k Bool SF) (C : Fin k) {input : List Bool} (b : Bool) (c : Cfg k Bool (SP b) input) (h : ¬c.Halted) (c' : Cfg k Bool (State SI SP SF) input) : (machine I P F C).Step (Cfg.mapState (passState b) c) c' ↔ c' = Cfg.mapState (passState b) (MultiTapeTM.step c)

Every native successor inside a live pass is the same deterministic successor.

theorem Turing.NondeterministicQueryMachine.Native.step_init_iff {k : ℕ} {SI SF : Type} {SP : Bool → Type} (I : MultiTapeTM k Bool SI) (P : (b : Bool) → MultiTapeTM k Bool (SP b)) (F : MultiTapeTM k Bool SF) (C : Fin k) {input : List Bool} (c : Cfg k Bool SI input) (h : ¬c.Halted) (c' : Cfg k Bool (State SI SP SF) input) : (machine I P F C).Step (Cfg.mapState initState c) c' ↔ c' = Cfg.mapState initState (MultiTapeTM.step c)

Every native successor inside the live initializer is its deterministic successor.

theorem Turing.NondeterministicQueryMachine.Native.step_finish_iff {k : ℕ} {SI SF : Type} {SP : Bool → Type} (I : MultiTapeTM k Bool SI) (P : (b : Bool) → MultiTapeTM k Bool (SP b)) (F : MultiTapeTM k Bool SF) (C : Fin k) {input : List Bool} (c : Cfg k Bool SF input) (h : ¬c.Halted) (c' : Cfg k Bool (State SI SP SF) input) : (machine I P F C).Step (Cfg.mapState finishState c) c' ↔ c' = Cfg.mapState finishState (MultiTapeTM.step c)

Every native successor inside the live finalizer is its deterministic successor.

theorem Turing.NondeterministicQueryMachine.Native.follows_pass {k : ℕ} {SI SF : Type} {SP : Bool → Type} (I : MultiTapeTM k Bool SI) (P : (b : Bool) → MultiTapeTM k Bool (SP b)) (F : MultiTapeTM k Bool SF) (C : Fin k) {input : List Bool} (b : Bool) (p : (machine I P F C).RunPath input) (q : RelSeries ((P b).runningStepRel input)) (hhead : RelSeries.head p = Cfg.mapState (passState b) q.head) (n : ℕ) (hn : n < p.length + 1) (hq : n < q.length + 1) : p.toFun ⟨n, hn⟩ = Cfg.mapState (passState b) (q.toFun ⟨n, hq⟩)

Every native pass prefix is the deterministic pass prefix. This is the reverse direction needed for space bounds on all native computation paths, rather than only a selected replay. The endpoint is included; it is the native continuation-check state.

theorem Turing.NondeterministicQueryMachine.Native.follows_init {k : ℕ} {SI SF : Type} {SP : Bool → Type} (I : MultiTapeTM k Bool SI) (P : (b : Bool) → MultiTapeTM k Bool (SP b)) (F : MultiTapeTM k Bool SF) (C : Fin k) {input : List Bool} (p : (machine I P F C).RunPath input) (q : RelSeries (I.runningStepRel input)) (hhead : RelSeries.head p = Cfg.mapState initState q.head) (n : ℕ) (hn : n < p.length + 1) (hq : n < q.length + 1) : p.toFun ⟨n, hn⟩ = Cfg.mapState initState (q.toFun ⟨n, hq⟩)

Every native initialization prefix is the deterministic initialization prefix.

theorem Turing.NondeterministicQueryMachine.Native.follows_finish {k : ℕ} {SI SF : Type} {SP : Bool → Type} (I : MultiTapeTM k Bool SI) (P : (b : Bool) → MultiTapeTM k Bool (SP b)) (F : MultiTapeTM k Bool SF) (C : Fin k) {input : List Bool} (p : (machine I P F C).RunPath input) (q : RelSeries (F.runningStepRel input)) (hhead : RelSeries.head p = Cfg.mapState finishState q.head) (n : ℕ) (hn : n < p.length + 1) (hq : n < q.length + 1) : p.toFun ⟨n, hn⟩ = Cfg.mapState finishState (q.toFun ⟨n, hq⟩)

Every native finalization prefix is the deterministic finalization prefix.

theorem Turing.NondeterministicQueryMachine.Native.inWindow_pass_prefix {k : ℕ} {SI SF : Type} {SP : Bool → Type} (I : MultiTapeTM k Bool SI) (P : (b : Bool) → MultiTapeTM k Bool (SP b)) (F : MultiTapeTM k Bool SF) (C : Fin k) {input : List Bool} (b : Bool) (p : (machine I P F C).RunPath input) (q : RelSeries ((P b).runningStepRel input)) (hhead : RelSeries.head p = Cfg.mapState (passState b) q.head) (hlen : p.length ≤ q.length) {s : ℕ} (hwin : ∀ c ∈ q, ∀ (i : Fin k), c.workTapePos i ∈ window s) : p.InWindow s

Every prefix that is still in one pass stays within the pass's original common window. No sum over time, repeated visits, or choices is taken.

def Turing.NondeterministicQueryMachine.Native.initHom {k : ℕ} {SI SF : Type} {SP : Bool → Type} (I : MultiTapeTM k Bool SI) (P : (b : Bool) → MultiTapeTM k Bool (SP b)) (F : MultiTapeTM k Bool SF) (C : Fin k) {input : List Bool} : (I.runningStepRel input).Hom ((machine I P F C).stepRel input)

Embed the running part of an initializer path into the native machine.

@[simp]

theorem Turing.NondeterministicQueryMachine.Native.initHom_apply {k : ℕ} {SI SF : Type} {SP : Bool → Type} (I : MultiTapeTM k Bool SI) (P : (b : Bool) → MultiTapeTM k Bool (SP b)) (F : MultiTapeTM k Bool SF) (C : Fin k) {input : List Bool} (c : Cfg k Bool SI input) : (initHom I P F C) c = Cfg.mapState initState c

def Turing.NondeterministicQueryMachine.Native.passHom {k : ℕ} {SI SF : Type} {SP : Bool → Type} (I : MultiTapeTM k Bool SI) (P : (b : Bool) → MultiTapeTM k Bool (SP b)) (F : MultiTapeTM k Bool SF) (C : Fin k) {input : List Bool} (b : Bool) : ((P b).runningStepRel input).Hom ((machine I P F C).stepRel input)

Embed the running part of a selected pass, retaining every head position.

@[simp]

theorem Turing.NondeterministicQueryMachine.Native.passHom_apply {k : ℕ} {SI SF : Type} {SP : Bool → Type} (I : MultiTapeTM k Bool SI) (P : (b : Bool) → MultiTapeTM k Bool (SP b)) (F : MultiTapeTM k Bool SF) (C : Fin k) {input : List Bool} (b : Bool) (c : Cfg k Bool (SP b) input) : (passHom I P F C b) c = Cfg.mapState (passState b) c

def Turing.NondeterministicQueryMachine.Native.finishHom {k : ℕ} {SI SF : Type} {SP : Bool → Type} (I : MultiTapeTM k Bool SI) (P : (b : Bool) → MultiTapeTM k Bool (SP b)) (F : MultiTapeTM k Bool SF) (C : Fin k) {input : List Bool} : (F.runningStepRel input).Hom ((machine I P F C).stepRel input)

Embed the running part of a finalizer, preserving its final halt.

@[simp]

theorem Turing.NondeterministicQueryMachine.Native.finishHom_apply {k : ℕ} {SI SF : Type} {SP : Bool → Type} (I : MultiTapeTM k Bool SI) (P : (b : Bool) → MultiTapeTM k Bool (SP b)) (F : MultiTapeTM k Bool SF) (C : Fin k) {input : List Bool} (c : Cfg k Bool SF input) : (finishHom I P F C) c = Cfg.mapState finishState c

theorem Turing.NondeterministicQueryMachine.Native.exists_round {k : ℕ} {SI SF : Type} {SP : Bool → Type} (I : MultiTapeTM k Bool SI) (P : (b : Bool) → MultiTapeTM k Bool (SP b)) (F : MultiTapeTM k Bool SF) (C : Fin k) {input : List Bool} (b : Bool) {Pre : List Bool → (Fin k → List Bool) → Prop} {Post : List Bool → (Fin k → List Bool) → (Fin k → List Bool) → List Bool → Prop} {t s : ℕ} (h : (P b).TransformsTapes Pre Post t s) {ws : Fin k → List Bool} (out : List Bool) (hPre : Pre input ws) : ∃ (ws' : Fin k → List Bool) (e : List Bool), Post input ws ws' e ∧ ∃ (p : (machine I P F C).RunPath input), RelSeries.head p = wordsCfg input (some State.choose) ws out ∧ RelSeries.last p = wordsCfg input (some (if ws' C = [] then State.finish F.q₀ else State.choose)) ws' (out ++ e) ∧ p.length ≤ t + 2 ∧ p.InWindow s

A deterministic pass specification gives a native round with one binary-choice step and one continuation check. Its heads stay in the same origin-centered window, independently of the number of preceding or following rounds.