Pair-splitting machine — proof internals

This file proves the stepwise decoding and exact-time correctness facts for pairSplitCoreTM. Stable statements are re-exposed by Complexitylib.Models.TuringMachine.Subroutines.PairSplit.

theorem Complexity.TM.pairSplitCoreTM_from_scanX_initTape_move_right_internal {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_internal {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_internal {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.

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

Every lifted pair-split trace preserves an off-start output tape.

theorem Complexity.TM.pairSplitCoreTM_toNTM_trace_preserves_other_work_internal {k : ℕ} (xIdx yIdx otherIdx : Fin k) (T : ℕ) (choices : Fin T → Bool) (c : Cfg k (pairSplitCoreTM xIdx yIdx).Q) (hx : otherIdx ≠ xIdx) (hy : otherIdx ≠ yIdx) (hread : (c.work otherIdx).read ≠ Γ.start) : ((pairSplitCoreTM xIdx yIdx).toNTM.trace T choices c).work otherIdx = c.work otherIdx

Every lifted pair-split trace preserves an off-start work tape other than the two destination tapes.

theorem Complexity.TM.pairSplitCoreTM_from_initCfg_internal {k : ℕ} (xIdx yIdx : Fin k) (hne : xIdx ≠ yIdx) (x y : List Bool) : ∃ (c' : Cfg k (pairSplitCoreTM xIdx yIdx).Q), (pairSplitCoreTM xIdx yIdx).reachesIn (pairSplitCoreTime x.length y.length) ((pairSplitCoreTM xIdx yIdx).initCfg (pair x y)) 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) ∧ (∀ (i : Fin k), i ≠ xIdx → i ≠ yIdx → c'.work i = (Tape.init []).move Dir3.right) ∧ c'.output = (Tape.init []).move Dir3.right

Exact pair-split correctness from the machine's genuine initial configuration. In addition to decoding the target tapes, the theorem frames the output and every unrelated work tape as started and blank.