feat(MultiTapeTM): concatenate the outputs of two machines

[crei]

concat tm₀ tm₁ runs tm₀, rewinds the native input head, and runs tm₁. The output tape is write-only and a machine only ever appends to it, so the composite outputs the output of tm₀ followed by the output of tm₁, and no intermediate result is stored anywhere.

The two machines get disjoint blocks of work tapes, tm₀ the first k₀ and tm₁ the last k₁. That is what makes it unnecessary to know anything about the configuration tm₀ halts in: tm₁ starts on blank tapes, exactly as it would on its own, and the tapes tm₀ leaves behind are never touched again. Rewinding the input in between is what lets tm₁ read the same input.

Plumbing/ExtendTapes.lean:

• eq_embed_initCfg reads the embedding backwards, and is what hands a fresh block of tapes to a machine: a configuration in that machine's initial state whose own block is blank and rewound, with the input head at the start, is its embedded initial configuration, whatever the other tapes hold and whatever output has been produced. So a combinator can start a machine on a block without knowing anything about the configuration the previous one left behind, beyond its output and that it did not touch this block.
• workTapes_embed_of_notMem_range, workTapePos_embed_of_notMem_range: the idleness of the extra tapes, which the module docstring claimed but which was observable only through spaceUsedByTape_extra.
• extend_eq_self, initCfg_extendTapes (factored out of runFrom_extendTapes) and spaceUsed_extendTapes.

NormalForms/RewindInput.lean:

• spaceUsed_rewindInput_le: normalizing costs no space. The rewind moves no work-tape head, so every cell the normalized machine visits was already visited by the original one.
• rewindInput_halts_spaceUsed: the normal form together with its cost, so a combinator that feeds one input to two machines never has to unfold the rewind. Only the time bound grows, by the input length plus two.
• initCfg_rewindInput.

Plumbing/Concat.lean (new):

• concatTapeLeft, concatTapeRight: the two blocks of work tapes, and their disjointness.
• concatPrefix, concat: the first phase and the composite.
• computesInTimeAndSpace_concat: the composite computes the concatenation. The extra time is one input rewind; the extra space is k₀ + k₁, since whichever machine is not running has an idle head on each of its tapes and each such head still counts for the cell it sits on. The rewind itself contributes nothing.

Combinators/Concat.lean (new, with a README for the new directory):

• computableInTimeAndSpace_concat: the function-level result, stated for an arbitrary function together with the assumption that its encoding is the concatenation of the two encodings, rather than for a fixed pairing. So it covers whatever the caller encodes, and the caller is the one who has to know that the concatenation of the two encodings is again injective.
• computableInTimeAndSpace_pair: the pair, the typical case.

The remaining supporting results, all of which the concatenation needs and none of which is specific to it:

• TapeLemmas: visitedByTapeHead_add and spaceUsed_add_le split the space of a run into its two phases; spaceUsed_eq_of_workTapePos reduces space usage to the head positions alone, which is what lets a machine be replaced by a simulation of it; and spaceUsed_le_of_workTapePos_mem is the sharp bound for a phase that moves no head, which visits no new cell at all rather than one per tape.
• Plumbing/Basic: Cfg.prependOutput and runFrom_prependOutput: a run does not depend on the output accumulated before it, which is what lets a machine run after another has already written part of the output.
• Plumbing/Sequential: initCfg_seq and spaceUsed_seq_le.
• Plumbing/Rewind: step_input_workTapePos and runFrom_input_workTapePos, since the input rewind moves no work-tape head.

Plumbing/Basic now imports TapeLemmas rather than Deterministic directly, which is also what brings TapeLemmas into the import graph of this directory, and Plumbing/ExtendTapes imports Plumbing/Basic for Cfg.prependOutput.

AI disclosure: Created using Claude.