Reserving work tapes without changing counts

The shared tape compiler maps each transition occurrence once. Extra tapes retain their contents and head positions throughout the entire List execution, with the same native clock.

Main results

• Turing.MultiTapeCTM.runList_embed: exact configuration occurrences under tape extension.
• Turing.MultiTapeCTM.HaltsWithin.embed: preserve the native all-branches clock.

References

The shared compiler and its original source credit are in MultiTape.Machine.ExtendTapes.

theorem Turing.MultiTapeCTM.Nonblocking.extendTapes {k k' : ℕ} {Symbol State : Type} {machine : MultiTapeCTM k Symbol State} (h : machine.Nonblocking) (e : Fin k ↪ Fin k') : Nonblocking (MultiTapeMachine.extendTapes machine e)

Reindexing work tapes maps every transition occurrence once.

theorem Turing.MultiTapeCTM.runList_embed {k k' : ℕ} {Symbol State : Type} {input : List Symbol} (machine : MultiTapeCTM k Symbol State) (e : Fin k ↪ Fin k') (cfg : MultiTapeMachine.Config k Symbol State Empty input) (extraTapes : Fin k' → ℤ → Option Symbol) (extraPos : Fin k' → ℤ) (fuel : ℕ) : runList (MultiTapeMachine.extendTapes machine e) fuel (cfg.embed e extraTapes extraPos).tapes = List.map (fun (final : Cfg k Symbol State input) => ((MultiTapeMachine.Config.emptyOracleEquiv.symm final).embed e extraTapes extraPos).tapes) (machine.runList fuel cfg.tapes)

Tape extension preserves the entire List, including unused tape contents and heads.

theorem Turing.MultiTapeCTM.branchCount_embed {k k' : ℕ} {Symbol State : Type} {input : List Symbol} (machine : MultiTapeCTM k Symbol State) (e : Fin k ↪ Fin k') (cfg : MultiTapeMachine.Config k Symbol State Empty input) (extraTapes : Fin k' → ℤ → Option Symbol) (extraPos : Fin k' → ℤ) (fuel : ℕ) (verdict : List Symbol → Bool) : branchCount (MultiTapeMachine.extendTapes machine e) verdict fuel (cfg.embed e extraTapes extraPos).tapes = machine.branchCount verdict fuel cfg.tapes

Tape extension preserves native terminal counts at every clock, including short clocks.

theorem Turing.MultiTapeCTM.HaltsWithin.embed {k k' : ℕ} {Symbol State : Type} {input : List Symbol} {machine : MultiTapeCTM k Symbol State} (hnon : machine.Nonblocking) (e : Fin k ↪ Fin k') (cfg : MultiTapeMachine.Config k Symbol State Empty input) (extraTapes : Fin k' → ℤ → Option Symbol) (extraPos : Fin k' → ℤ) (fuel : ℕ) (h : machine.HaltsWithin fuel cfg.tapes) : HaltsWithin (MultiTapeMachine.extendTapes machine e) fuel (cfg.embed e extraTapes extraPos).tapes

Nonblocking tape extension preserves the native clock, even with dirty unused tapes.

theorem Turing.MultiTapeCTM.branchCount_extendTapes {k k' : ℕ} {Symbol State : Type} (machine : MultiTapeCTM k Symbol State) (e : Fin k ↪ Fin k') (input : List Symbol) (fuel : ℕ) (verdict : List Symbol → Bool) : branchCount (MultiTapeMachine.extendTapes machine e) verdict fuel ((MultiTapeMachine.extendTapes machine e).initialConfig input).tapes = machine.branchCount verdict fuel (MultiTapeMachine.initialConfig machine input).tapes

Initializing the extended machine reserves blank tapes without changing any terminal count.

theorem Turing.MultiTapeCTM.HaltsWithin.extendTapes {k k' : ℕ} {Symbol State : Type} {machine : MultiTapeCTM k Symbol State} (hnon : machine.Nonblocking) (e : Fin k ↪ Fin k') (input : List Symbol) (fuel : ℕ) (h : machine.HaltsWithin fuel (MultiTapeMachine.initialConfig machine input).tapes) : HaltsWithin (MultiTapeMachine.extendTapes machine e) fuel ((MultiTapeMachine.extendTapes machine e).initialConfig input).tapes

The initialized tape extension has the same native all-branches clock.