Split a paired input onto work tapes

pairSplitCoreTM is the deterministic machine-level inverse of the neutral pair codec. On a canonical input pair x y, it writes x and y as canonical binary prefixes on two distinct work tapes in exact time 2 * |x| + |y| + 4.

This is intentionally a canonical-pair primitive, not a total recognizer for the image of pair: malformed inputs may share its halting state. A client requiring rejecting semantics for arbitrary outer strings must use a parser with a distinct failure result.

Main results

• pairSplitCoreTM_reachesIn_initCfg — exact initialized endpoint with frames.
• pairSplitCoreTM_from_init_initTape_move_right — exact endpoint semantics.
• pairSplitCoreTM_hoareTime_prefix_marker_frame — binary prefixes, left markers, and preserved frames.
• pairSplitCoreTM_hoareTime_prefix_frame — compatibility binary-prefix specification with frames.
• pairSplitCoreTM_hoareTime_prefix — compact binary-prefix specification.
• pairSplitCoreTM_hoareTime_frame and pairSplitCoreTM_hoareTime — compatible HasOutput specifications.

@[simp]

theorem Complexity.TM.pairSplitCoreTime_eq_pair_length (x y : List Bool) : pairSplitCoreTime x.length y.length = (pair x y).length + 2

On a canonical pair, the splitter's exact time is the encoded input length plus two steps.

theorem Complexity.TM.pairSplitCoreTM_reachesIn_initCfg {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 genuine machine initialization. The target work tapes contain the decoded components, while every unrelated work tape and the output are the canonical started blank tape.

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 from the already-started .scanX phase. This preserves the theorem name formerly exposed from the NP-internal implementation.

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

One phase-composition step from .init to .scanX, preserving the already-started input and target work 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 a canonical pair and two empty started work tapes, pairSplitCoreTM halts in its exact advertised time. The two target tapes contain the decoded components and finish immediately after them.

theorem Complexity.TM.pairSplitCoreTM_hoareTime_prefix_marker_frame {k : ℕ} (xIdx yIdx : Fin k) (hne : xIdx ≠ yIdx) (x y : List Bool) (frameWork : Fin k → Tape) (frameOutput : Tape) (hframeWork : ∀ (i : Fin k), i ≠ xIdx → i ≠ yIdx → (frameWork i).read ≠ Γ.start) (hframeOutput : frameOutput.read ≠ Γ.start) : (pairSplitCoreTM xIdx yIdx).HoareTime (fun (inp : Tape) (work : Fin k → Tape) (out : Tape) => inp = (Tape.init (List.map Γ.ofBool (pair x y))).move Dir3.right ∧ work xIdx = (Tape.init []).move Dir3.right ∧ work yIdx = (Tape.init []).move Dir3.right ∧ (∀ (i : Fin k), i ≠ xIdx → i ≠ yIdx → work i = frameWork i) ∧ out = frameOutput) (fun (inp : Tape) (work : Fin k → Tape) (out : Tape) => inp.head = (pair x y).length + 1 ∧ inp.cells = (Tape.init (List.map Γ.ofBool (pair x y))).cells ∧ (work xIdx).cells 0 = Γ.start ∧ (work xIdx).HasBinaryPrefix x ∧ (work yIdx).cells 0 = Γ.start ∧ (work yIdx).HasBinaryPrefix y ∧ (∀ (i : Fin k), i ≠ xIdx → i ≠ yIdx → work i = frameWork i) ∧ out = frameOutput) (pairSplitCoreTime x.length y.length)

Marker-aware frame-preserving specification. The decoded components are canonical binary prefixes with their left markers intact, and the splitter preserves an arbitrary off-start output tape and every arbitrary off-start work tape outside the two targets.

theorem Complexity.TM.pairSplitCoreTM_hoareTime_prefix_frame {k : ℕ} (xIdx yIdx : Fin k) (hne : xIdx ≠ yIdx) (x y : List Bool) (frameWork : Fin k → Tape) (frameOutput : Tape) (hframeWork : ∀ (i : Fin k), i ≠ xIdx → i ≠ yIdx → (frameWork i).read ≠ Γ.start) (hframeOutput : frameOutput.read ≠ Γ.start) : (pairSplitCoreTM xIdx yIdx).HoareTime (fun (inp : Tape) (work : Fin k → Tape) (out : Tape) => inp = (Tape.init (List.map Γ.ofBool (pair x y))).move Dir3.right ∧ work xIdx = (Tape.init []).move Dir3.right ∧ work yIdx = (Tape.init []).move Dir3.right ∧ (∀ (i : Fin k), i ≠ xIdx → i ≠ yIdx → work i = frameWork i) ∧ out = frameOutput) (fun (inp : Tape) (work : Fin k → Tape) (out : Tape) => inp.head = (pair x y).length + 1 ∧ inp.cells = (Tape.init (List.map Γ.ofBool (pair x y))).cells ∧ (work xIdx).HasBinaryPrefix x ∧ (work yIdx).HasBinaryPrefix y ∧ (∀ (i : Fin k), i ≠ xIdx → i ≠ yIdx → work i = frameWork i) ∧ out = frameOutput) (pairSplitCoreTime x.length y.length)

Frame-preserving compositional specification. The decoded components are canonical binary prefixes, and the splitter preserves an arbitrary off-start output tape and every arbitrary off-start work tape outside the two targets.

theorem Complexity.TM.pairSplitCoreTM_hoareTime_frame {k : ℕ} (xIdx yIdx : Fin k) (hne : xIdx ≠ yIdx) (x y : List Bool) (frameWork : Fin k → Tape) (frameOutput : Tape) (hframeWork : ∀ (i : Fin k), i ≠ xIdx → i ≠ yIdx → (frameWork i).read ≠ Γ.start) (hframeOutput : frameOutput.read ≠ Γ.start) : (pairSplitCoreTM xIdx yIdx).HoareTime (fun (inp : Tape) (work : Fin k → Tape) (out : Tape) => inp = (Tape.init (List.map Γ.ofBool (pair x y))).move Dir3.right ∧ work xIdx = (Tape.init []).move Dir3.right ∧ work yIdx = (Tape.init []).move Dir3.right ∧ (∀ (i : Fin k), i ≠ xIdx → i ≠ yIdx → work i = frameWork i) ∧ out = frameOutput) (fun (inp : Tape) (work : Fin k → Tape) (out : Tape) => inp.head = (pair x y).length + 1 ∧ inp.cells = (Tape.init (List.map Γ.ofBool (pair x y))).cells ∧ (work xIdx).head = 1 + x.length ∧ (work xIdx).HasOutput x ∧ (work yIdx).head = 1 + y.length ∧ (work yIdx).HasOutput y ∧ (∀ (i : Fin k), i ≠ xIdx → i ≠ yIdx → work i = frameWork i) ∧ out = frameOutput) (pairSplitCoreTime x.length y.length)

Frame-preserving compositional specification exposing the decoded heads and HasOutput facts. The prefix-strengthened form is pairSplitCoreTM_hoareTime_prefix_frame.

theorem Complexity.TM.pairSplitCoreTM_hoareTime_prefix {k : ℕ} (xIdx yIdx : Fin k) (hne : xIdx ≠ yIdx) (x y : List Bool) : (pairSplitCoreTM xIdx yIdx).HoareTime (fun (inp : Tape) (work : Fin k → Tape) (x_1 : Tape) => inp = (Tape.init (List.map Γ.ofBool (pair x y))).move Dir3.right ∧ work xIdx = (Tape.init []).move Dir3.right ∧ work yIdx = (Tape.init []).move Dir3.right) (fun (inp : Tape) (work : Fin k → Tape) (x_1 : Tape) => inp.head = (pair x y).length + 1 ∧ inp.cells = (Tape.init (List.map Γ.ofBool (pair x y))).cells ∧ (work xIdx).HasBinaryPrefix x ∧ (work yIdx).HasBinaryPrefix y) (pairSplitCoreTime x.length y.length)

Compositional canonical-pair specification. The target work tapes begin empty at cell 1; on exit they are canonical binary prefixes for the two decoded strings. This compact theorem makes no claim about unrelated work tapes or the output; use pairSplitCoreTM_hoareTime_prefix_frame when those frames must be preserved.

theorem Complexity.TM.pairSplitCoreTM_hoareTime {k : ℕ} (xIdx yIdx : Fin k) (hne : xIdx ≠ yIdx) (x y : List Bool) : (pairSplitCoreTM xIdx yIdx).HoareTime (fun (inp : Tape) (work : Fin k → Tape) (x_1 : Tape) => inp = (Tape.init (List.map Γ.ofBool (pair x y))).move Dir3.right ∧ work xIdx = (Tape.init []).move Dir3.right ∧ work yIdx = (Tape.init []).move Dir3.right) (fun (inp : Tape) (work : Fin k → Tape) (x_1 : Tape) => inp.head = (pair x y).length + 1 ∧ inp.cells = (Tape.init (List.map Γ.ofBool (pair x y))).cells ∧ (work xIdx).head = 1 + x.length ∧ (work xIdx).HasOutput x ∧ (work yIdx).head = 1 + y.length ∧ (work yIdx).HasOutput y) (pairSplitCoreTime x.length y.length)

Compact canonical-pair specification exposing the decoded heads and HasOutput facts. The prefix-strengthened form is pairSplitCoreTM_hoareTime_prefix.