Placed phase of the nondeterministic composition — proof internals

After the deterministic prefix, NTM.compositionNTM tmF N runs the placed retargeted copy of N on the virtual input. This file relates that phase's composite steps to N's own steps, one choice bit at a time:

• NTM.placedCfg — embed an N-configuration into the composite's placed phase, given a stable frame, a stable ignored real-input tape, and the N-configuration (whose input tape becomes the virtual input).
• NTM.placedCfg_step — branch b of the composite steps placedCfg exactly as N.det b steps the underlying configuration.
• NTM.placedCfg_trace — the composite's trace from a placedCfg is the placedCfg of N's trace, along any choice sequence.
• NTM.compositionNTM_seam_step — from a DetPrefixBoundary configuration, one branch-b step enters the placed phase exactly at N's post-first-step configuration on the virtual input (startedCfg).

def Complexity.NTM.placedCfg {nf ng : ℕ} (tmF : TM nf) (N : NTM ng) (extras : Fin (TM.compositionTapeCount nf ng) → Tape) (realInput : Tape) (c : Cfg ng N.Q) : Cfg (TM.compositionTapeCount nf ng) (compositionNTM tmF N).Q

Embed an N-configuration into the composite's placed phase. The frame extras supplies the tapes outside the placed block, realInput the ignored real input tape, and c's input tape becomes the virtual input on the placed block's last tape.

Equations

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

theorem Complexity.NTM.placedCfg_state {nf ng : ℕ} (tmF : TM nf) (N : NTM ng) (extras : Fin (TM.compositionTapeCount nf ng) → Tape) (realInput : Tape) (c : Cfg ng N.Q) : (placedCfg tmF N extras realInput c).state = Sum.inr (Sum.inr (Sum.inr (Sum.inr c.state)))

The state of a placed embedding.

theorem Complexity.NTM.placedCfg_output {nf ng : ℕ} (tmF : TM nf) (N : NTM ng) (extras : Fin (TM.compositionTapeCount nf ng) → Tape) (realInput : Tape) (c : Cfg ng N.Q) : (placedCfg tmF N extras realInput c).output = c.output

The output tape of a placed embedding is c's output tape.

theorem Complexity.NTM.placedCfg_halted_iff {nf ng : ℕ} (tmF : TM nf) (N : NTM ng) (extras : Fin (TM.compositionTapeCount nf ng) → Tape) (realInput : Tape) (c : Cfg ng N.Q) : (placedCfg tmF N extras realInput c).state = (compositionNTM tmF N).qhalt ↔ c.state = N.qhalt

The composite is halted at a placed embedding iff N is halted at the underlying configuration.

theorem Complexity.NTM.placedCfg_step {nf ng : ℕ} (tmF : TM nf) (N : NTM ng) (b : Bool) {extras : Fin (TM.compositionTapeCount nf ng) → Tape} {realInput : Tape} {c c' : Cfg ng N.Q} (hstep : (N.det b).step c = some c') (hvin : c.input.StartInvariant) (hri : realInput.read ≠ Γ.start) (hex : ∀ (i : Fin (TM.compositionTapeCount nf ng)), ¬TM.placeWorkInMiddle (0 + (nf + 1)) (ng + 1) i → (extras i).read ≠ Γ.start) : ((compositionNTM tmF N).det b).step (placedCfg tmF N extras realInput c) = some (placedCfg tmF N extras realInput c')

Placed-phase step commute. Branch b of the composite steps a placed embedding exactly as N.det b steps the underlying configuration, provided the virtual input is start-invariant, the ignored real input reads off ▷, and the frame tapes are stable.

theorem Complexity.NTM.placedCfg_trace {nf ng : ℕ} (tmF : TM nf) (N : NTM ng) {extras : Fin (TM.compositionTapeCount nf ng) → Tape} {realInput : Tape} (hri : realInput.read ≠ Γ.start) (hex : ∀ (i : Fin (TM.compositionTapeCount nf ng)), ¬TM.placeWorkInMiddle (0 + (nf + 1)) (ng + 1) i → (extras i).read ≠ Γ.start) (s : ℕ) (choices : Fin s → Bool) (c : Cfg ng N.Q) (hvin : c.input.StartInvariant) : (compositionNTM tmF N).trace s choices (placedCfg tmF N extras realInput c) = placedCfg tmF N extras realInput (N.trace s choices c)

Placed-phase trace correspondence. Along any choice sequence, the composite's trace from a placed embedding is the placed embedding of N's trace.

theorem Complexity.NTM.compositionNTM_seam_step {nf ng : ℕ} (tmF : TM nf) (N : NTM ng) (b : Bool) {y : List Bool} {E : Cfg (TM.compositionTapeCount nf ng) (compositionNTM tmF N).Q} (hB : DetPrefixBoundary tmF N y E) (hne : (N.det b).qstart ≠ (N.det b).qhalt) : ((compositionNTM tmF N).det b).step E = some (placedCfg tmF N E.work E.input ((N.det b).startedCfg y hne))

The seam into the placed phase. From a DetPrefixBoundary configuration, one branch-b composite step enters the placed phase at N's post-first-step configuration on the virtual input y, with the boundary's own tapes as frame and real input.