Pair a computed value with the original input — proof internals

This module verifies the generic fanout pipeline defined in Composition.PairWithInput.Defs.

def Complexity.TM.PairWithInputTailPre (nf : ℕ) (first second : List Bool) (B : ℕ) (inp : Tape) (work : Fin (pairWithInputTapeCount nf) → Tape) (out : Tape) : Prop

Boundary contract after the source computation has redirected its output. Both source heads remain within B, every tape is safely parked away from the left marker, and the real output is fresh for pair emission.

Equations

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

theorem Complexity.TM.pairWithInputTailTM_hoareTime_internal (nf : ℕ) (first second : List Bool) (B : ℕ) : (pairWithInputTailTM nf).HoareTime (PairWithInputTailPre nf first second B) (fun (_inp : Tape) (_work : Fin (pairWithInputTapeCount nf) → Tape) (out : Tape) => out.HasOutput (pair first second)) (2 * B + pairInputWorkTime first second + 6)

The normalization-and-emission tail turns a raw delimited source output and the original input into their canonical pair.

theorem Complexity.TM.pairWithInputTM_computesInTime_internal {nf : ℕ} {tmF : TM nf} {f : List Bool → List Bool} {T : ℕ → ℕ} (hcomp : tmF.ComputesInTime f T) : tmF.pairWithInputTM.ComputesInTime (fun (x : List Bool) => pair (f x) x) (pairWithInputTime T)

Internal correctness of the executable fanout combinator.