Preparing both components of an encoded pair

The two certified pair projections write their outputs to separate work tapes. Both output heads finish at zero, every scratch tape is cleared, and the input head is restored. The preparation cost includes both computations and both rewinds.

Main results

• Turing.MultiTapeTM.PairEncoding.exists_prepare: one finite machine prepares both words in linear time and space, uniformly over all encoded pairs.

References

This uses Christian Reitwiessner's PairEncoding interface and output-to-word compiler.

theorem Turing.MultiTapeTM.PairEncoding.exists_prepare {α β : Type u} (enc₁ : α ↪ List Bool) (enc₂ : β ↪ List Bool) (enc : α × β ↪ List Bool) [PairEncoding enc₁ enc₂ enc] : ∃ (r : ℕ) (State : Type) (_ : Finite State) (machine : MultiTapeTM (r + 2) Bool State) (c : ℕ), ∀ (p : α × β), machine.TransformsTapes (fun (input : List Bool) (ws : Fin (r + 2) → List Bool) => input = enc p ∧ ws = fun (x : Fin (r + 2)) => []) (fun (x : List Bool) (x_1 ws' : Fin (r + 2) → List Bool) (emitted : List Bool) => ws' = Fin.append (fun (x : Fin r) => []) ![enc₁ p.1, enc₂ p.2] ∧ emitted = []) (c * ((enc p).length + 1)) (c * ((enc p).length + 1))

Prepare the two encoded components on the last two work tapes, clearing all scratch tapes and restoring all heads. The machine and its linear bound are independent of the pair.