Common windows for all native query-loop prefixes

The bounds here concern every native path, with no bound on its length. Each deterministic routine starts with its heads at the common origin. Its space bound therefore confines its heads to the same window as every other invocation. The choice and continuation instructions move no heads. Repeating the routines does not multiply the window by the number of iterations.

Main results

• Turing.NondeterministicQueryMachine.Native.choose_inWindow: every prefix from a pass boundary stays in the common routine window, assuming a preserved invariant on tape words.

theorem Turing.NondeterministicQueryMachine.Native.step_check_words {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) (ws : Fin k → List Bool) (out : List Bool) : MultiTapeTM.step (wordsCfg input (some State.check) ws out) = wordsCfg input (some (if ws C = [] then State.finish F.q₀ else State.choose)) ws out

From a word-holding configuration the continuation instruction reads exactly whether the continuation word is empty.

theorem Turing.NondeterministicQueryMachine.Native.finish_inWindow {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} {ws : Fin k → List Bool} {out : List Bool} {t s : ℕ} (hF : F.TransformsTapes (fun (inp : List Bool) (w : Fin k → List Bool) => inp = input ∧ w = ws) (fun (x : List Bool) (x_1 x_2 : Fin k → List Bool) (x_3 : List Bool) => True) t s) (p : (machine I P F C).RunPath input) (hhead : RelSeries.head p = wordsCfg input (some (State.finish F.q₀)) ws out) : p.InWindow s

Any prefix begun at a finalizer stays in its deterministic window, including arbitrary halted self-loop padding after the finalizer ends.

theorem Turing.NondeterministicQueryMachine.Native.choose_inWindow {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} (Inv : (Fin k → List Bool) → Prop) {s : ℕ} (hP : ∀ (b : Bool) (ws : Fin k → List Bool), Inv ws → ∃ (t : ℕ), (P b).TransformsTapes (fun (inp : List Bool) (w : Fin k → List Bool) => inp = input ∧ w = ws) (fun (x : List Bool) (x_1 w' : Fin k → List Bool) (x_2 : List Bool) => Inv w') t s) (hF : ∀ (ws : Fin k → List Bool), Inv ws → ∃ (t : ℕ), F.TransformsTapes (fun (inp : List Bool) (w : Fin k → List Bool) => inp = input ∧ w = ws) (fun (x : List Bool) (x_1 x_2 : Fin k → List Bool) (x_3 : List Bool) => True) t s) (p : (machine I P F C).RunPath input) {ws : Fin k → List Bool} {out : List Bool} (hInv : Inv ws) (hhead : RelSeries.head p = wordsCfg input (some State.choose) ws out) : p.InWindow s

Every native pass-loop prefix stays in one fixed window. Each of the two pass routines preserves Inv on tape words and uses at most s cells when started at the origin. The finalizer has the same bound. These routines can run arbitrarily many times: the conclusion is independent of the number of passes and applies to all native choices and all computation prefixes.

theorem Turing.NondeterministicQueryMachine.Native.runsInSpace_of_transforms {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} (Inv : (Fin k → List Bool) → Prop) {s tI : ℕ} (hI : I.TransformsTapes (fun (inp : List Bool) (ws : Fin k → List Bool) => inp = input ∧ ws = fun (x : Fin k) => []) (fun (x : List Bool) (x_1 ws' : Fin k → List Bool) (x_2 : List Bool) => Inv ws') tI s) (hP : ∀ (b : Bool) (ws : Fin k → List Bool), Inv ws → ∃ (t : ℕ), (P b).TransformsTapes (fun (inp : List Bool) (w : Fin k → List Bool) => inp = input ∧ w = ws) (fun (x : List Bool) (x_1 w' : Fin k → List Bool) (x_2 : List Bool) => Inv w') t s) (hF : ∀ (ws : Fin k → List Bool), Inv ws → ∃ (t : ℕ), F.TransformsTapes (fun (inp : List Bool) (w : Fin k → List Bool) => inp = input ∧ w = ws) (fun (x : List Bool) (x_1 x_2 : Fin k → List Bool) (x_3 : List Bool) => True) t s) : (machine I P F C).RunsInSpace input (k * (2 * s + 1))

The complete native loop uses one common window on every computation prefix. Tidy initialization establishes the word invariant, the selected passes preserve it, and finalization terminates tidily. The number of iterations and their runtimes do not occur in the space bound. This theorem does not assert that the loop terminates.