Pair a computed value with the original input

This file defines a generic deterministic pipeline for the fanout operation x ↦ pair (f x) x. It redirects the computed value to a work tape, rewinds that tape and the immutable original input, then emits both components directly to the real output. Only the first raw-output delimiter is semantic; later cells may contain arbitrary non-▷ junk.

@[reducible, inline]

abbrev Complexity.TM.pairWithInputTapeCount (nf : ℕ) : ℕ

Work-tape count of pairWithInputTM. One extra tape beyond the redirected output is kept as a stable phase-composition frame.

Equations

• Complexity.TM.pairWithInputTapeCount nf = Complexity.TM.compositionTapeCount nf 0

def Complexity.TM.pairWithInputRawOutputIdx (nf : ℕ) : Fin (pairWithInputTapeCount nf)

Physical work tape holding the raw output of the function computation.

Equations

• Complexity.TM.pairWithInputRawOutputIdx nf = Complexity.TM.compositionRawOutputIdx nf 0

def Complexity.TM.pairWithInputFirstTM {nf : ℕ} (tmF : TM nf) : TM (pairWithInputTapeCount nf)

First phase of pairWithInputTM: compute with the output redirected to the raw-output work tape.

Equations

• tmF.pairWithInputFirstTM = tmF.compositionFirstTM 0

def Complexity.TM.pairWithInputTailTM (nf : ℕ) : TM (pairWithInputTapeCount nf)

Normalize the two read heads, then emit the computed value paired with the unchanged original input.

Equations

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

def Complexity.TM.pairWithInputTM {nf : ℕ} (tmF : TM nf) : TM (pairWithInputTapeCount nf)

Executable deterministic fanout combinator computing x ↦ pair (f x) x whenever tmF computes f.

Equations

• tmF.pairWithInputTM = tmF.pairWithInputFirstTM.seqTM (Complexity.TM.pairWithInputTailTM nf)

def Complexity.TM.pairWithInputTime (sourceTime : ℕ → ℕ) (inputLength : ℕ) : ℕ

Coarse time budget for pairWithInputTM. It covers the source run, both rewinds, pair emission, and the three phase transitions.

Equations

• Complexity.TM.pairWithInputTime sourceTime inputLength = 5 * sourceTime inputLength + inputLength + 12