Native time-block traces

These original native-model lemmas are prerequisites for the active-block construction in [Wil25], arXiv:2502.17779v1, §3.4. They use the actual multitape machine and its stationary-after-halting run. They do not construct a computation graph, simulate input access, or prove a space bound.

A finite work-tape window retains Option Symbol: blank and a written zero are different. blockEmitted retains only the symbols emitted during a block, not the preceding output. The radius-duration window below is deliberately a locality envelope, not a claim about the optimal number of aligned active blocks or their encoded bit length.

The active-block route was proposed in worker-crei-dc679113’s M0 design for issue #888; these local trace lemmas do not implement its pending graph/packing obligations.

Main definitions

• Turing.MultiTapeTM.blockStart: the native configuration at a block boundary.
• Turing.MultiTapeTM.blockDuration: a block clipped to a finite time horizon.
• Turing.Cfg.workWindow: a finite window around each native work-tape head.
• Turing.MultiTapeTM.blockEmitted: output emitted during a run segment.

Main results

• Turing.MultiTapeTM.blockStart_succ: exact composition of adjacent blocks.
• Turing.MultiTapeTM.runFrom_blockDuration: exact clipped-final-block composition.
• Turing.MultiTapeTM.workTapePos_runFrom_abs_sub_le: local head displacement.
• Turing.MultiTapeTM.workTapes_runFrom_eq_of_outside_window: unchanged exterior cells.
• Turing.MultiTapeTM.output_eq_append_blockEmitted: separate old output from new output.

def Turing.Cfg.workWindow {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (cfg : Cfg k Symbol State input) (radius : ℕ) : Fin k → Fin (2 * radius + 1) → Option Symbol

A finite window of exactly 2 * radius + 1 cells per tape, centered at its starting head. No previous output word is stored here.

theorem Turing.Cfg.workWindow_center {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (cfg : Cfg k Symbol State input) (radius : ℕ) (tape : Fin k) : cfg.workWindow radius tape ⟨radius, ⋯⟩ = cfg.workTapeSymbols tape

The middle entry is the actual scanned cell, including its blank marker.

noncomputable def Turing.MultiTapeTM.blockStart {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (tm : MultiTapeTM k Symbol State) (cfg : Cfg k Symbol State input) (width index : ℕ) : Cfg k Symbol State input

The native configuration at the start of zero-indexed time block index.

def Turing.MultiTapeTM.blockDuration (horizon width index : ℕ) : ℕ

The number of steps left in a block before the finite horizon. A zero width is allowed and gives an empty block; later aligned-block geometry requires positive width separately.

@[simp]

theorem Turing.MultiTapeTM.blockStart_zero {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (tm : MultiTapeTM k Symbol State) (cfg : Cfg k Symbol State input) (width : ℕ) : tm.blockStart cfg width 0 = cfg

Block zero starts at the supplied configuration, even at width zero.

@[simp]

theorem Turing.MultiTapeTM.blockDuration_zero_width (horizon index : ℕ) : blockDuration horizon 0 index = 0

Zero-width blocks contain no steps at any horizon.

theorem Turing.MultiTapeTM.blockDuration_le_width (horizon width index : ℕ) : blockDuration horizon width index ≤ width

Clipping never increases the chosen block width.

theorem Turing.MultiTapeTM.blockStart_succ {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (tm : MultiTapeTM k Symbol State) (cfg : Cfg k Symbol State input) (width index : ℕ) : tm.blockStart cfg width (index + 1) = runFrom (tm.blockStart cfg width index) width

Adjacent full blocks use exactly the same native run, including halted suffixes.

theorem Turing.MultiTapeTM.runFrom_blockDuration {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (tm : MultiTapeTM k Symbol State) (cfg : Cfg k Symbol State input) (horizon width index : ℕ) (hstart : index * width ≤ horizon) : runFrom (tm.blockStart cfg width index) (blockDuration horizon width index) = runFrom cfg (min ((index + 1) * width) horizon)

A block beginning before the horizon ends exactly at the next boundary or the horizon. The hypothesis is essential: a block starting after the horizon is not rewound.

theorem Turing.MultiTapeTM.blockDuration_eq_zero_of_le (horizon width index : ℕ) (h : horizon ≤ index * width) : blockDuration horizon width index = 0

At or beyond the horizon there are no remaining steps.

theorem Turing.MultiTapeTM.workTapePos_runFrom_abs_sub_le {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (tm : MultiTapeTM k Symbol State) (cfg : Cfg k Symbol State input) (duration : ℕ) (tape : Fin k) : |(runFrom cfg duration).workTapePos tape - cfg.workTapePos tape| ≤ ↑duration

The final configuration is included: in duration steps a head is within duration cells of its starting position. This holds for negative tape positions and halted prefixes.

theorem Turing.MultiTapeTM.workTapes_runFrom_eq_of_outside_window {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (tm : MultiTapeTM k Symbol State) (cfg : Cfg k Symbol State input) (duration : ℕ) (tape : Fin k) (position : ℤ) (hout : ↑duration < |position - cfg.workTapePos tape|) : (runFrom cfg duration).workTapes tape position = cfg.workTapes tape position

A cell outside the closed radius-duration locality envelope is never visited and therefore retains its contents. In particular, blank cells do not silently become written zeroes.

theorem Turing.MultiTapeTM.exists_output_suffix {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (tm : MultiTapeTM k Symbol State) (cfg : Cfg k Symbol State input) (duration : ℕ) : ∃ (emitted : List Symbol), (runFrom cfg duration).output = cfg.output ++ emitted ∧ emitted.length ≤ duration

The output of a segment consists of the existing prefix and at most one new symbol per native step. No assumption of halting is needed.

noncomputable def Turing.MultiTapeTM.blockEmitted {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (tm : MultiTapeTM k Symbol State) (cfg : Cfg k Symbol State input) (duration : ℕ) : List Symbol

Only the output newly emitted by this segment. The old prefix is explicitly discarded.

theorem Turing.MultiTapeTM.output_eq_append_blockEmitted {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (tm : MultiTapeTM k Symbol State) (cfg : Cfg k Symbol State input) (duration : ℕ) : (runFrom cfg duration).output = cfg.output ++ tm.blockEmitted cfg duration

Reconstruct the native output from its existing prefix and the segment-only suffix.

theorem Turing.MultiTapeTM.length_blockEmitted_le {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (tm : MultiTapeTM k Symbol State) (cfg : Cfg k Symbol State input) (duration : ℕ) : (tm.blockEmitted cfg duration).length ≤ duration

The suffix payload is at most the segment duration, regardless of the old prefix length.

theorem Turing.MultiTapeTM.blockStart_eq_of_halted {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (tm : MultiTapeTM k Symbol State) (cfg : Cfg k Symbol State input) (hhalt : cfg.Halted) (width index : ℕ) : tm.blockStart cfg width index = cfg

Halting is stationary, including all output and work-tape contents.