Trace factorization through the deterministic prefix

Every trace of NTM.compositionNTM tmF N — along any choice sequence — first runs the deterministic pipeline (first computation, output rewind, copy, virtual-input rewind) without consulting a single choice bit. The trace therefore factors through the DetPrefixBoundary configuration in which the virtual input holds f x, after which only the placed retargeted copy of N runs.

The choice-independence is packaged by NTM.compositionNTM_trace_prefix: the length-(s + t) trace equals the length-s trace restarted from the boundary with the first t choices discarded.

theorem Complexity.NTM.compositionNTM_trace_prefix {nf ng : ℕ} (tmF : TM nf) (N : NTM ng) {f : List Bool → List Bool} {TF : ℕ → ℕ} (hF : tmF.ComputesInTime f TF) (x : List Bool) : ∃ (E : Cfg (TM.compositionTapeCount nf ng) (compositionNTM tmF N).Q), ∃ t ≤ 4 * TF x.length + 10, DetPrefixBoundary tmF N (f x) E ∧ ∀ (s : ℕ) (choices : Fin (s + t) → Bool), (compositionNTM tmF N).trace (s + t) choices ((compositionNTM tmF N).initCfg x) = (compositionNTM tmF N).trace s (fun (i : Fin s) => choices ⟨↑i + t, ⋯⟩) E

Trace factorization through the deterministic prefix. There is a boundary configuration E (holding f x on the virtual-input tape) and a prefix length t ≤ 4 * TF |x| + 10 such that every trace of the composite factors through E, with the first t choice bits ignored.

theorem Complexity.NTM.compositionNTM_trace_run {nf ng : ℕ} (tmF : TM nf) (N : NTM ng) {f : List Bool → List Bool} {TF : ℕ → ℕ} (hF : tmF.ComputesInTime f TF) (x : List Bool) (hne : N.qstart ≠ N.qhalt) : ∃ (E : Cfg (TM.compositionTapeCount nf ng) (compositionNTM tmF N).Q), ∃ t ≤ 4 * TF x.length + 10, DetPrefixBoundary tmF N (f x) E ∧ ∀ (s : ℕ) (choices : Fin (s + 1 + t) → Bool), (compositionNTM tmF N).trace (s + 1 + t) choices ((compositionNTM tmF N).initCfg x) = placedCfg tmF N E.work E.input (N.trace (s + 1) (fun (i : Fin (s + 1)) => choices ⟨↑i + t, ⋯⟩) (N.initCfg (f x)))

Full trace correspondence. For a machine N that does not start halted, every composite trace of length (s + 1) + t is the placed embedding of N's own length-(s + 1) trace on the virtual input f x: the seam step out of the prefix boundary is N's first traced step, and thereafter the composite follows N bit for bit.