pairSplitCoreTM: split pair x y into two work tapes

This file defines the deterministic inverse of pairBuildTM at the machine level. Given an input tape containing pair x y, the machine copies:

• the decoded left component x onto work tape xIdx,
• the suffix y onto work tape yIdx.

The machine is intended as the front half of a deterministic verifier pipeline. The main exposed artifacts are the concrete TM, its running-time function pairSplitCoreTime, and the end-to-end correctness theorems pairSplitCoreTM_from_scanX_initTape_move_right and pairSplitCoreTM_from_init_initTape_move_right.

inductive Complexity.TM.PairSplitPhase : Type

Control states of pairSplitCoreTM: .init steps off ▷; .scanX, .afterFalse, and .writeTrue decode the doubled-bit prefix (with 01 as separator); .copyY copies the suffix; .done is the halting state.

• init : PairSplitPhase
• scanX : PairSplitPhase
• afterFalse : PairSplitPhase
• writeTrue : PairSplitPhase
• copyY : PairSplitPhase
• done : PairSplitPhase

@[implicit_reducible]

instance Complexity.TM.instDecidableEqPairSplitPhase : DecidableEq PairSplitPhase

Equations

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

@[implicit_reducible]

instance Complexity.TM.instFintypePairSplitPhase : Fintype PairSplitPhase

Equations

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

def Complexity.TM.pairSplitCoreTM {k : ℕ} (xIdx yIdx : Fin k) : TM k

Core pair-splitting machine. On well-formed inputs pair x y, it decodes the doubled-bit prefix onto work tape xIdx and copies the remaining suffix to work tape yIdx. Invalid inputs may halt early; the correctness theorem will only target the valid pair x y shape.

Equations

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

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

Running time of the core split phase on valid pair x y inputs.

Equations

• Complexity.TM.pairSplitCoreTime xLen yLen = 2 * xLen + yLen + 4

theorem Complexity.TM.pairSplitCoreTM_from_scanX_initTape_move_right {k : ℕ} (xIdx yIdx : Fin k) (hne : xIdx ≠ yIdx) (x y : List Bool) (c : Cfg k (pairSplitCoreTM xIdx yIdx).Q) (hst : c.state = PairSplitPhase.scanX) (hinp : c.input = (Tape.init (List.map Γ.ofBool (pair x y))).move Dir3.right) (hxw : c.work xIdx = (Tape.init []).move Dir3.right) (hyw : c.work yIdx = (Tape.init []).move Dir3.right) : ∃ (c' : Cfg k (pairSplitCoreTM xIdx yIdx).Q), (pairSplitCoreTM xIdx yIdx).reachesIn (2 * x.length + y.length + 3) c c' ∧ (pairSplitCoreTM xIdx yIdx).halted c' ∧ c'.input.head = (pair x y).length + 1 ∧ c'.input.cells = (Tape.init (List.map Γ.ofBool (pair x y))).cells ∧ (c'.work xIdx).head = 1 + x.length ∧ (c'.work xIdx).cells 0 = Γ.start ∧ (∀ (i : ℕ) (h : i < x.length), (c'.work xIdx).cells (i + 1) = Γ.ofBool x[i]) ∧ (∀ (i : ℕ), x.length ≤ i → (c'.work xIdx).cells (i + 1) = Γ.blank) ∧ (c'.work yIdx).head = 1 + y.length ∧ (c'.work yIdx).cells 0 = Γ.start ∧ (∀ (i : ℕ) (h : i < y.length), (c'.work yIdx).cells (i + 1) = Γ.ofBool y[i]) ∧ ∀ (i : ℕ), y.length ≤ i → (c'.work yIdx).cells (i + 1) = Γ.blank

Core correctness for valid started inputs. Beginning in .scanX with pair x y on the input tape and empty started work tapes, pairSplitCoreTM halts after decoding the doubled x prefix onto xIdx and copying the suffix y onto yIdx. The two work heads finish just past the strings they wrote.

theorem Complexity.TM.pairSplit_init_step_all_started {k : ℕ} (xIdx yIdx : Fin k) (c : Cfg k (pairSplitCoreTM xIdx yIdx).Q) (hst : c.state = PairSplitPhase.init) (hinp : c.input.read ≠ Γ.start) (hx : (c.work xIdx).read ≠ Γ.start) (hy : (c.work yIdx).read ≠ Γ.start) : ∃ (c' : Cfg k (pairSplitCoreTM xIdx yIdx).Q), (pairSplitCoreTM xIdx yIdx).step c = some c' ∧ c'.state = PairSplitPhase.scanX ∧ c'.input = c.input ∧ c'.work xIdx = c.work xIdx ∧ c'.work yIdx = c.work yIdx

Variant of the init step for phase composition: if the input tape and the two tracked work tapes are already positioned past ▷, the .init state advances to .scanX without changing those tapes.

theorem Complexity.TM.pairSplitCoreTM_from_init_initTape_move_right {k : ℕ} (xIdx yIdx : Fin k) (hne : xIdx ≠ yIdx) (x y : List Bool) (c : Cfg k (pairSplitCoreTM xIdx yIdx).Q) (hst : c.state = PairSplitPhase.init) (hinp : c.input = (Tape.init (List.map Γ.ofBool (pair x y))).move Dir3.right) (hxw : c.work xIdx = (Tape.init []).move Dir3.right) (hyw : c.work yIdx = (Tape.init []).move Dir3.right) : ∃ (c' : Cfg k (pairSplitCoreTM xIdx yIdx).Q), (pairSplitCoreTM xIdx yIdx).reachesIn (pairSplitCoreTime x.length y.length) c c' ∧ (pairSplitCoreTM xIdx yIdx).halted c' ∧ c'.input.head = (pair x y).length + 1 ∧ c'.input.cells = (Tape.init (List.map Γ.ofBool (pair x y))).cells ∧ (c'.work xIdx).head = 1 + x.length ∧ (c'.work xIdx).cells 0 = Γ.start ∧ (∀ (i : ℕ) (h : i < x.length), (c'.work xIdx).cells (i + 1) = Γ.ofBool x[i]) ∧ (∀ (i : ℕ), x.length ≤ i → (c'.work xIdx).cells (i + 1) = Γ.blank) ∧ (c'.work yIdx).head = 1 + y.length ∧ (c'.work yIdx).cells 0 = Γ.start ∧ (∀ (i : ℕ) (h : i < y.length), (c'.work yIdx).cells (i + 1) = Γ.ofBool y[i]) ∧ ∀ (i : ℕ), y.length ≤ i → (c'.work yIdx).cells (i + 1) = Γ.blank

Starting from .init with pair x y already on a started input tape and empty started work tapes, pairSplitCoreTM halts within pairSplitCoreTime, leaving xIdx holding x and yIdx holding y, with both heads just past the written strings.