Pair emission from the input and a work tape — proof internals

This module verifies the exact two-pass controller in PairEmit.Defs.

theorem Complexity.TM.pairInputWorkTM_reachesIn_internal {n : ℕ} (firstIdx : Fin n) (first second : List Bool) {inp out : Tape} {work : Fin n → Tape} (hinput : inp = (Tape.init (List.map Γ.ofBool second)).move Dir3.right) (hsourceHead : (work firstIdx).head = 1) (hsourceOutput : (work firstIdx).HasOutput first) (hwork : ∀ (i : Fin n), (work i).StartInvariant ∧ 1 ≤ (work i).head) (houtput : out = (Tape.init []).move Dir3.right) : ∃ (c' : Cfg n (pairInputWorkTM firstIdx).Q), (pairInputWorkTM firstIdx).reachesIn (pairInputWorkTime first second) { state := (pairInputWorkTM firstIdx).qstart, input := inp, work := work, output := out } c' ∧ (pairInputWorkTM firstIdx).halted c' ∧ c'.input.HasBinarySuffix [] ∧ c'.input.cells = inp.cells ∧ (c'.work firstIdx).HasBinarySuffix [] ∧ (c'.work firstIdx).cells = (work firstIdx).cells ∧ (c'.work firstIdx).HasOutput first ∧ (∀ (i : Fin n), i ≠ firstIdx → c'.work i = work i) ∧ c'.output.HasBinaryPrefix (pair first second)

Exact execution from the concrete tape boundary used by the generic fanout combinator.

theorem Complexity.TM.pairInputWorkTM_hoareTime_internal {n : ℕ} (firstIdx : Fin n) (first second : List Bool) : (pairInputWorkTM firstIdx).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = (Tape.init (List.map Γ.ofBool second)).move Dir3.right ∧ (work firstIdx).head = 1 ∧ (work firstIdx).HasOutput first ∧ (∀ (i : Fin n), (work i).StartInvariant ∧ 1 ≤ (work i).head) ∧ out = (Tape.init []).move Dir3.right) (fun (_inp : Tape) (_work : Fin n → Tape) (out : Tape) => out.HasOutput (pair first second)) (pairInputWorkTime first second)

Internal compact Hoare contract for pair emission.