What the bracket scan computes

A model of the left-to-right pass over a serialized Data value: a bracket depth, a count of the top-level children already passed, and the bits collected while inside the child that was asked for. This file is about the model alone — that it really does extract the requested child — and says nothing about computability; Complexitylib.Classes.PCP.Internal.DataScan runs the same pass as a polynomial-time fold.

Two facts drive everything. The depth and the count evolve without looking at the collected bits, and the collected bits only ever grow at the end (runSpec_append_acc); and a serialized value read at any depth returns to that depth, having contributed exactly its own serialization when it was the child being sought (runSpec_toBits).

Main definitions

• Complexity.DataScan.runSpec — the model of the pass

Main results

• Complexity.DataScan.runSpec_toBits — reading one serialized value
• Complexity.DataScan.runSpec_flatten — reading a whole run of children
• Complexity.DataScan.runSpec_inner — the pass over a serialized list returns the requested child

def Complexity.DataScan.stepSpec (i : ℕ) (st : ℕ × ℕ × List Bool) (b : Bool) : ℕ × ℕ × List Bool

One step of the pass: false opens a bracket, true closes one, and the bit joins the output exactly when the count matches the child sought.

Equations

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

def Complexity.DataScan.runSpec (i : ℕ) (st : ℕ × ℕ × List Bool) (s : List Bool) : ℕ × ℕ × List Bool

The pass over a whole string.

Equations

• Complexity.DataScan.runSpec i st s = List.foldl (Complexity.DataScan.stepSpec i) st s

@[simp]

theorem Complexity.DataScan.runSpec_nil (i : ℕ) (st : ℕ × ℕ × List Bool) : runSpec i st [] = st

theorem Complexity.DataScan.runSpec_append (i : ℕ) (st : ℕ × ℕ × List Bool) (s t : List Bool) : runSpec i st (s ++ t) = runSpec i (runSpec i st s) t

theorem Complexity.DataScan.runSpec_cons (i : ℕ) (st : ℕ × ℕ × List Bool) (b : Bool) (s : List Bool) : runSpec i st (b :: s) = runSpec i (stepSpec i st b) s

theorem Complexity.DataScan.runSpec_append_acc (i : ℕ) (s : List Bool) (d c : ℕ) (pre acc : List Bool) : runSpec i (d, c, pre ++ acc) s = ((runSpec i (d, c, acc) s).fst, (runSpec i (d, c, acc) s).snd.fst, pre ++ (runSpec i (d, c, acc) s).snd.snd)

The collected bits only grow at the end. A prefix already present in the output is carried through untouched, and the depth and count do not see it.

theorem Complexity.DataScan.runSpec_toBits (i : ℕ) (y : Data) (d c : ℕ) (acc : List Bool) : runSpec i (d, c, acc) y.toBits = (d, if d = 0 then c + 1 else c, if c = i then acc ++ y.toBits else acc)

Reading one serialized value. Starting at depth d with c children already passed, the pass over y.toBits returns to depth d; it counts one more child exactly when it was at the top level, and it contributes y.toBits to the output exactly when y is the child sought.

A run of children

def Complexity.DataScan.selFrom (xs : List Data) (i c : ℕ) : List Bool

The child a pass looking for index i picks out of xs, having already passed c children.

Equations

• Complexity.DataScan.selFrom xs i c = if c ≤ i then (Option.map Complexity.Data.toBits xs[i - c]?).getD [] else []

@[simp]

theorem Complexity.DataScan.selFrom_nil (i c : ℕ) : selFrom [] i c = []

theorem Complexity.DataScan.runSpec_flatten (i : ℕ) (xs : List Data) (c : ℕ) (acc : List Bool) : runSpec i (0, c, acc) (List.map Data.toBits xs).flatten = (0, c + xs.length, acc ++ selFrom xs i c)

Reading a run of children. At the top level the pass counts every child and contributes exactly the one it was asked for.

theorem Complexity.DataScan.runSpec_inner (i : ℕ) (xs : List Data) : runSpec i (0, 0, []) (List.map Data.toBits xs).flatten = (0, xs.length, (Option.map Data.toBits xs[i]?).getD [])

The pass over a serialized list. Reading the bits strictly between the outer brackets returns the requested child's own serialization.