Reduced transducer snapshot dynamics — proof internals #
This module proves that one-way, space-bounded transducer steps are determined
by the finite snapshot from SpaceTime.Defs, once the shared read-only input
contents are fixed.
theorem
Complexity.TM.transducerSnapshot_step_congr
{k : ℕ}
{tm : TM k}
{inputLength space : ℕ}
{c₁ c₂ d₁ d₂ : Cfg k tm.Q}
(htrans : tm.IsTransducer)
(hc₁ : c₁.WithinAuxSpace inputLength space)
(hc₂ : c₂.WithinAuxSpace inputLength space)
(hd₁ : d₁.WithinAuxSpace inputLength space)
(hd₂ : d₂.WithinAuxSpace inputLength space)
(hinput : c₁.input.cells = c₂.input.cells)
(hblank₁ : c₁.output.BlankAfterHead)
(hblank₂ : c₂.output.BlankAfterHead)
(hsnap : tm.transducerSnapshot c₁ inputLength space hc₁ = tm.transducerSnapshot c₂ inputLength space hc₂)
(hstep₁ : tm.step c₁ = some d₁)
(hstep₂ : tm.step c₂ = some d₂)
:
One transducer step preserves equality of finite snapshots when both source configurations share the same read-only input contents and all source and target work heads stay within the advertised space bound.
theorem
Complexity.TM.transducerSnapshot_reachesIn_congr
{k : ℕ}
{tm : TM k}
{inputLength space t : ℕ}
{c₁ c₂ d₁ d₂ : Cfg k tm.Q}
(htrans : tm.IsTransducer)
(hreach₁ : tm.reachesIn t c₁ d₁)
(hreach₂ : tm.reachesIn t c₂ d₂)
(hspace₁ : ∀ {u : ℕ} {d : Cfg k tm.Q}, tm.reachesIn u c₁ d → d.WithinAuxSpace inputLength space)
(hspace₂ : ∀ {u : ℕ} {d : Cfg k tm.Q}, tm.reachesIn u c₂ d → d.WithinAuxSpace inputLength space)
(hinput : c₁.input.cells = c₂.input.cells)
(hblank₁ : c₁.output.BlankAfterHead)
(hblank₂ : c₂.output.BlankAfterHead)
(hsnap : tm.transducerSnapshot c₁ inputLength space ⋯ = tm.transducerSnapshot c₂ inputLength space ⋯)
:
Equal snapshots stay equal along equal-length transducer runs whose work and input heads remain within the same auxiliary-space window.