Truncating to the length of a leading block — proof internals

takeLen (pair c y) = y.take |c|: the leading self-delimiting block acts as a ruler and the verbatim suffix is truncated to its length. Carrying a width bound as a string rather than as a number is what keeps an iterated FP step function polynomial-time — each iteration truncates its state to the ruler, so no intermediate value can grow beyond it.

The transducer takeLenTM has one work tape: scan parses the leading block two symbols at a time, writing one unary mark per payload bit; rewind returns the work head to cell one; copy emits one input symbol per remaining mark. Malformed input halts with empty output, matching unpair? = none.

Main results

• Complexity.takeLen_pair — the defining equation on genuine pairs
• Complexity.takeLen_mem_FP — the truncation is in FP

The function computed by the scanner

def Complexity.takeLenAux (k : ℕ) (w : List Bool) : List Bool

The remaining output of the truncation scanner when k payload bits of the leading block have already been counted and w is the unread part of the input: the suffix truncated to the total ruler length, and nothing at all when the block framing is broken.

Equations

• Complexity.takeLenAux k w = match Complexity.unpair? w with | some (x, y) => List.take (k + x.length) y | none => []

def Complexity.takeLen (p : List Bool) : List Bool

Truncate the verbatim suffix of a pair to the length of its leading block.

Equations

• Complexity.takeLen p = Complexity.takeLenAux 0 p

@[simp]

theorem Complexity.takeLenAux_nil (k : ℕ) : takeLenAux k [] = []

@[simp]

theorem Complexity.takeLenAux_singleton (k : ℕ) (b : Bool) : takeLenAux k [b] = []

@[simp]

theorem Complexity.takeLenAux_sep (k : ℕ) (z : List Bool) : takeLenAux k (false :: true :: z) = List.take k z

Reaching the separator ends the ruler: the suffix is truncated to k.

theorem Complexity.takeLenAux_double (k : ℕ) (b : Bool) (z : List Bool) : takeLenAux k (b :: b :: z) = takeLenAux (k + 1) z

A doubled payload bit lengthens the ruler by one.

@[simp]

theorem Complexity.takeLenAux_broken (k : ℕ) (z : List Bool) : takeLenAux k (true :: false :: z) = []

A broken doubling halts the scan with no output.

theorem Complexity.takeLen_pair (c y : List Bool) : takeLen (pair c y) = List.take c.length y

On a genuine pair the leading block is the ruler.

inductive Complexity.TakePhase : Type

Control states of takeLenTM.

• skip : TakePhase

  Move every head off the left-end marker.

• scanA : TakePhase

  Read the first symbol of a doubled payload bit.

• scanB0 : TakePhase

  The first symbol of the pair was 0.

• scanB1 : TakePhase

  The first symbol of the pair was 1.

• rew : TakePhase

  Rewind the work head to cell one.

• copy : TakePhase

  Emit one input symbol per remaining mark.

• done : TakePhase

  Halt.

@[implicit_reducible]

instance Complexity.instDecidableEqTakePhase : DecidableEq TakePhase

Equations

• Complexity.instDecidableEqTakePhase x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Complexity.instFintypeTakePhase : Fintype TakePhase

Equations

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

def Complexity.takeLenTM : TM 1

The truncation scanner. Parses the leading self-delimiting block into |c| unary marks on its work tape, then copies that many input symbols to the output. Computes takeLen.

Equations

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

Correctness of the scanner

theorem Complexity.takeLenTM_computesInTime : takeLenTM.ComputesInTime takeLen fun (n : ℕ) => 3 * n + 6

takeLenTM computes takeLen in 3 · |p| + 6 steps.

theorem Complexity.takeLen_mem_FP : takeLen ∈ FP

Internal proof that ruler-truncation is in FP.