pairBuildTM: construct pair x y on a work tape

The DTM pairBuildTM k yIdx pIdx assumes:

• x lives on the input tape (standard layout: head 0 on ▷, x in cells 1..|x|, blanks beyond),
• y lives on work tape yIdx (same layout: head 0 on ▷, y in cells 1..|y|, blanks beyond),
• work tape pIdx is the empty Tape.init [].

After running, work tape pIdx carries pair x y — the doubled-bits encoding of x followed by the [false, true] separator followed by y verbatim — with head positioned at cell 1, matching the convention used by the other rewindWorkTM-based subroutines.

Phase structure

init        advance every ▷-reading tape past ▷ (one step)
copyX1      if input blank → writeSep1; else write bit to pIdx, advance pIdx
copyX2      write the same bit to pIdx, advance input *and* pIdx
writeSep1   write `false` to pIdx, advance pIdx
writeSep2   write `true`  to pIdx, advance pIdx
copyY       if y blank → rewindP1; else write y-bit to pIdx, advance y+pIdx
rewindP1    if pIdx reads ▷ → rewindP2; else move pIdx left
rewindP2    one extra right step, transition to done (leaves pIdx head=1)
done        halt

Total running time: linear in |x| + |y| (see pairBuildTM_hoareTime).

Status

Everything in this file is fully proved (no sorry). The main contents:

• Machine: pairBuildTM (with δ_right_of_start), the phase type PairBuildPhase, and the running-time bound pairBuildTime.
• Init-step variants for phase composition: pairBuild_init_step_started (pair tape still fresh at head 0) and pairBuild_init_step_all_started (all tracked tapes already past ▷).
• Tape helper: Tape.eq_init_move_right_of_binary, identifying a head-1 binary tape with a standard Tape.init moved right once.
• Main correctness: pairBuildTM_hoareTime, a HoareTime triple stating that from x on the input tape, y on work tape yIdx, and an empty work tape pIdx, the machine halts within pairBuildTime |x| |y| steps with pair x y on tape pIdx.
• Corollaries: pairBuildTM_hoareTime_initTape_move_right (the pair tape equals Tape.init of the encoding moved right once), pairBuildTM_hoareTime_all_started_initTape_move_right (same, from the all-started layout), its NTM lift pairBuildTM_toNTM_hoareTime_all_started_initTape_move_right, and pairBuildTM_hoareTime_hasOutput (Tape.HasOutput form).
• Frame lemmas for NTM traces: pairBuildTM_trace_one_preserves_output / pairBuildTM_trace_preserves_output (the output tape is untouched) and pairBuildTM_trace_one_preserves_other_work / pairBuildTM_trace_preserves_other_work (work tapes other than yIdx and pIdx are untouched), each assuming the tape's head is past ▷.

inductive Complexity.TM.PairBuildPhase : Type

Control states of pairBuildTM, one per phase of the construction: advance past ▷ (init), double each input bit onto the pair tape (copyX1/copyX2), write the [false, true] separator (writeSep1/writeSep2), copy the witness verbatim (copyY), rewind the pair tape to cell 1 (rewindP1/rewindP2), and halt (done).

• init : PairBuildPhase
• copyX1 : PairBuildPhase
• copyX2 : PairBuildPhase
• writeSep1 : PairBuildPhase
• writeSep2 : PairBuildPhase
• copyY : PairBuildPhase
• rewindP1 : PairBuildPhase
• rewindP2 : PairBuildPhase
• done : PairBuildPhase

@[implicit_reducible]

instance Complexity.TM.instDecidableEqPairBuildPhase : DecidableEq PairBuildPhase

Equations

• Complexity.TM.instDecidableEqPairBuildPhase x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Complexity.TM.instFintypePairBuildPhase : Fintype PairBuildPhase

Equations

• One or more equations did not get rendered due to their size.

def Complexity.TM.pairBuildTM {k : ℕ} (yIdx pIdx : Fin k) : TM k

Build pair x y on work tape pIdx, reading x from the input tape and y from work tape yIdx. Requires yIdx ≠ pIdx for the construction to make sense; the definition itself is valid for any indices.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.TM.pairBuild_init_step_started {k : ℕ} (yIdx pIdx : Fin k) (c : Cfg k (pairBuildTM yIdx pIdx).Q) (hst : c.state = PairBuildPhase.init) (hinp : c.input.read ≠ Γ.start) (hy : (c.work yIdx).read ≠ Γ.start) (hpi0 : (c.work pIdx).head = 0) (hpic0 : (c.work pIdx).cells 0 = Γ.start) : ∃ (c' : Cfg k (pairBuildTM yIdx pIdx).Q), (pairBuildTM yIdx pIdx).step c = some c' ∧ c'.state = PairBuildPhase.copyX1 ∧ c'.input = c.input ∧ c'.work yIdx = c.work yIdx ∧ (c'.work pIdx).head = 1 ∧ (c'.work pIdx).cells = (c.work pIdx).cells

Variant of the init step for phase composition: input and witness tapes may already be positioned at their first data cells, while the pair tape is still the fresh head-0 tape.

theorem Complexity.TM.pairBuild_init_step_all_started {k : ℕ} (yIdx pIdx : Fin k) (c : Cfg k (pairBuildTM yIdx pIdx).Q) (hst : c.state = PairBuildPhase.init) (hinp : c.input.read ≠ Γ.start) (hy : (c.work yIdx).read ≠ Γ.start) (hp : (c.work pIdx).read ≠ Γ.start) : ∃ (c' : Cfg k (pairBuildTM yIdx pIdx).Q), (pairBuildTM yIdx pIdx).step c = some c' ∧ c'.state = PairBuildPhase.copyX1 ∧ c'.input = c.input ∧ c'.work yIdx = c.work yIdx ∧ c'.work pIdx = c.work pIdx

Variant of the init step for fully-started phase composition: input, witness, and pair tapes may all already be positioned past ▷.

def Complexity.TM.pairBuildTime (xLen yLen : ℕ) : ℕ

Running-time bound: pairBuildTM finishes in 4·|x| + 2·|y| + 10 steps.

Breakdown:

• init: 1 step.
• copyX1+copyX2: 2·|x| + 1 steps (one final copyX1 detects blank).
• writeSep1+writeSep2: 2 steps.
• copyY: |y| + 1 steps.
• rewindP1: one step per cell left from 2|x|+2+|y|+1 to 0, so 2|x|+|y|+3 steps; plus the rewindP2 step; plus the done transition step.

Equations

• Complexity.TM.pairBuildTime xLen yLen = 4 * xLen + 2 * yLen + 10

theorem Complexity.TM.Tape.eq_init_move_right_of_binary {t : Tape} {bits : List Bool} (hhead : t.head = 1) (h0 : t.cells 0 = Γ.start) (hbits : ∀ (i : ℕ) (h : i < bits.length), t.cells (i + 1) = Γ.ofBool bits[i]) (htail : ∀ (i : ℕ), bits.length ≤ i → t.cells (i + 1) = Γ.blank) : t = (Tape.init (List.map Γ.ofBool bits)).move Dir3.right

A tape with head at cell 1, a start marker at cell 0, binary contents bits, and a blank tail is exactly the standard initialized tape for bits, moved right once.

theorem Complexity.TM.pairBuildTM_hoareTime {k : ℕ} (yIdx pIdx : Fin k) (hne : yIdx ≠ pIdx) (x y : List Bool) : (pairBuildTM yIdx pIdx).HoareTime (fun (inp : Tape) (work : Fin k → Tape) (x_1 : Tape) => inp = Tape.init (List.map Γ.ofBool x) ∧ work yIdx = Tape.init (List.map Γ.ofBool y) ∧ work pIdx = Tape.init []) (fun (x_1 : Tape) (work : Fin k → Tape) (x_2 : Tape) => (work pIdx).head = 1 ∧ (work pIdx).cells 0 = Γ.start ∧ (∀ (i : ℕ) (h : i < (pair x y).length), (work pIdx).cells (i + 1) = Γ.ofBool (pair x y)[i]) ∧ ∀ (i : ℕ), (pair x y).length ≤ i → (work pIdx).cells (i + 1) = Γ.blank) (pairBuildTime x.length y.length)

pairBuildTM correctness. Given x on the input tape and y on work tape yIdx (with yIdx ≠ pIdx), pairBuildTM yIdx pIdx halts leaving work tape pIdx carrying pair x y (in the cells indexed 1..|pair x y|), blank thereafter, with head at cell 1, within pairBuildTime steps.

theorem Complexity.TM.pairBuildTM_hoareTime_initTape_move_right {k : ℕ} (yIdx pIdx : Fin k) (hne : yIdx ≠ pIdx) (x y : List Bool) : (pairBuildTM yIdx pIdx).HoareTime (fun (inp : Tape) (work : Fin k → Tape) (x_1 : Tape) => inp = Tape.init (List.map Γ.ofBool x) ∧ work yIdx = Tape.init (List.map Γ.ofBool y) ∧ work pIdx = Tape.init []) (fun (x_1 : Tape) (work : Fin k → Tape) (x_2 : Tape) => work pIdx = (Tape.init (List.map Γ.ofBool (pair x y))).move Dir3.right) (pairBuildTime x.length y.length)

A compact corollary of pairBuildTM_hoareTime: the pair tape satisfies exact equality with the standard initialized pair tape, moved to cell 1.

theorem Complexity.TM.pairBuildTM_hoareTime_all_started_initTape_move_right {k : ℕ} (yIdx pIdx : Fin k) (hne : yIdx ≠ pIdx) (x y : List Bool) : (pairBuildTM yIdx pIdx).HoareTime (fun (inp : Tape) (work : Fin k → Tape) (x_1 : Tape) => inp = (Tape.init (List.map Γ.ofBool x)).move Dir3.right ∧ work yIdx = (Tape.init (List.map Γ.ofBool y)).move Dir3.right ∧ work pIdx = (Tape.init []).move Dir3.right) (fun (x_1 : Tape) (work : Fin k → Tape) (x_2 : Tape) => work pIdx = (Tape.init (List.map Γ.ofBool (pair x y))).move Dir3.right) (pairBuildTime x.length y.length)

pairBuildTM correctness for phase composition where input, witness, and pair tapes have already passed the start marker. This is the layout produced by earlier setup phases that idle untouched tapes once from ▷ to cell 1.

theorem Complexity.TM.pairBuildTM_toNTM_hoareTime_all_started_initTape_move_right {k : ℕ} (yIdx pIdx : Fin k) (hne : yIdx ≠ pIdx) (x y : List Bool) : (pairBuildTM yIdx pIdx).toNTM.HoareTime (fun (inp : Tape) (work : Fin k → Tape) (x_1 : Tape) => inp = (Tape.init (List.map Γ.ofBool x)).move Dir3.right ∧ work yIdx = (Tape.init (List.map Γ.ofBool y)).move Dir3.right ∧ work pIdx = (Tape.init []).move Dir3.right) (fun (x_1 : Tape) (work : Fin k → Tape) (x_2 : Tape) => work pIdx = (Tape.init (List.map Γ.ofBool (pair x y))).move Dir3.right) (pairBuildTime x.length y.length)

Nondeterministic lift of pairBuildTM_hoareTime_all_started_initTape_move_right.

theorem Complexity.TM.pairBuildTM_trace_one_preserves_output {k : ℕ} (yIdx pIdx : Fin k) (choice : Bool) (c : Cfg k (pairBuildTM yIdx pIdx).Q) (hread : c.output.read ≠ Γ.start) : ((pairBuildTM yIdx pIdx).toNTM.trace 1 (fun (x : Fin 1) => choice) c).output = c.output

One pair-builder step preserves the output tape once the output head is past the start marker.

theorem Complexity.TM.pairBuildTM_trace_preserves_output {k : ℕ} (yIdx pIdx : Fin k) (T : ℕ) (choices : Fin T → Bool) (c : Cfg k (pairBuildTM yIdx pIdx).Q) (hread : c.output.read ≠ Γ.start) : ((pairBuildTM yIdx pIdx).toNTM.trace T choices c).output = c.output

Pair-builder traces preserve the output tape once the output head is past the start marker.

theorem Complexity.TM.pairBuildTM_trace_one_preserves_other_work {k : ℕ} (yIdx pIdx otherIdx : Fin k) (choice : Bool) (c : Cfg k (pairBuildTM yIdx pIdx).Q) (hy : otherIdx ≠ yIdx) (hp : otherIdx ≠ pIdx) (hread : (c.work otherIdx).read ≠ Γ.start) : ((pairBuildTM yIdx pIdx).toNTM.trace 1 (fun (x : Fin 1) => choice) c).work otherIdx = c.work otherIdx

One pair-builder step preserves a non-active work tape once that tape's head is past the start marker.

theorem Complexity.TM.pairBuildTM_trace_preserves_other_work {k : ℕ} (yIdx pIdx otherIdx : Fin k) (T : ℕ) (choices : Fin T → Bool) (c : Cfg k (pairBuildTM yIdx pIdx).Q) (hy : otherIdx ≠ yIdx) (hp : otherIdx ≠ pIdx) (hread : (c.work otherIdx).read ≠ Γ.start) : ((pairBuildTM yIdx pIdx).toNTM.trace T choices c).work otherIdx = c.work otherIdx

Pair-builder traces preserve a non-active work tape once that tape's head is past the start marker.

theorem Complexity.TM.pairBuildTM_hoareTime_hasOutput {k : ℕ} (yIdx pIdx : Fin k) (hne : yIdx ≠ pIdx) (x y : List Bool) : (pairBuildTM yIdx pIdx).HoareTime (fun (inp : Tape) (work : Fin k → Tape) (x_1 : Tape) => inp = Tape.init (List.map Γ.ofBool x) ∧ work yIdx = Tape.init (List.map Γ.ofBool y) ∧ work pIdx = Tape.init []) (fun (x_1 : Tape) (work : Fin k → Tape) (x_2 : Tape) => (work pIdx).head = 1 ∧ (work pIdx).HasOutput (pair x y)) (pairBuildTime x.length y.length)

A compact corollary of pairBuildTM_hoareTime: the pair tape satisfies the standard Tape.HasOutput predicate for pair x y.