Bridging the string computation and the counting definitions

The amplified verdict is defined by counting blocks of a seed function Fin (k * T) → Bool inside a Finset; the algebra computes with the seed as a string. This file identifies the two views: a block of the string decodes to the corresponding block of the function, so the algebra's unary count is the blockEventCount of the amplification lemmas.

Main results

• Lautemann.getD_take_drop — reading inside a block of a string
• Lautemann.seedOfList_blockAtIdx — the decoded block is the function's block
• Lautemann.blockEventCount_seedOfList — the two counts agree

theorem Complexity.Lautemann.getD_take_drop (s : List Bool) (a b j : ℕ) (hj : j < b) : (List.take b (List.drop a s)).getD j false = s.getD (a + j) false

Reading inside a block of a string reads the underlying string.

theorem Complexity.Lautemann.seedOfList_blockAtIdx (T : ℕ) (s : List Bool) (i : ℕ) (t : Fin T) : seedOfList T (Cobham.blockAtIdx T s i) t = s.getD (i * T + ↑t) false

The block of a decoded seed is the decoding of the block of the string.

theorem Complexity.Lautemann.blocksEquiv_seedOfList (runs T : ℕ) (s : List Bool) (i : Fin runs) : (blocksEquiv runs T) (seedOfList (runs * T) s) i = seedOfList T (Cobham.blockAtIdx T s ↑i)

The blocks of a decoded long seed are the decodings of its string blocks.

theorem Complexity.Lautemann.pathAccepts_iff {k : ℕ} (tm : NTM k) (x c : List Bool) : Cobham.PathAccepts tm x c ↔ seedOfList c.length c ∈ tm.repeatAcceptEvent x c.length

Path acceptance is membership of the decoded choice string in the single-trial accepting event.

theorem Complexity.Lautemann.blockEventCount_seedOfList {T : ℕ} (E : Finset (Fin T → Bool)) (runs : ℕ) (s : List Bool) : blockEventCount E (seedOfList (runs * T) s) = ∑ j ∈ Finset.range runs, if seedOfList T (Cobham.blockAtIdx T s j) ∈ E then 1 else 0

The block count of a decoded seed is a sum over block indices.

theorem Complexity.Lautemann.blockAtIdx_length (T : ℕ) (s : List Bool) (j runs : ℕ) (hs : s.length = runs * T) (hj : j < runs) : (Cobham.blockAtIdx T s j).length = T

Inside a seed of exactly runs blocks, every block is full.

theorem Complexity.Lautemann.acceptCountAux_length_eq {k : ℕ} (tm : NTM k) (u x τ s ρ : List Bool) (runs : ℕ) (hρ : ρ.length = runs) (hs : s.length = runs * τ.length) (hu : x.length + τ.length + Fintype.card tm.Q + 3 ≤ u.length) : (Cobham.acceptCountAux tm u x τ s ρ).length = blockEventCount (tm.repeatAcceptEvent x τ.length) (seedOfList (runs * τ.length) s)

The algebra's count is the amplification lemmas' block count.

theorem Complexity.Lautemann.majorityFlag_eq_true_iff' {k : ℕ} (tm : NTM k) (u x τ s ρ : List Bool) (runs : ℕ) (hρ : ρ.length = runs) (hs : s.length = runs * τ.length) (hu : x.length + τ.length + Fintype.card tm.Q + 3 ≤ u.length) : Cobham.majorityFlag tm u x τ s ρ = [true] ↔ blockMajority (tm.repeatAcceptEvent x τ.length) (seedOfList (runs * τ.length) s) = true

The algebra's majority flag is the amplified majority verdict.

The shift action

theorem Complexity.Lautemann.getD_padTo (σ b : List Bool) (j : ℕ) (hj : j < σ.length) : (padTo σ b).getD j false = b.getD j false

Reading inside a padded block reads the block.

theorem Complexity.Lautemann.seedOfList_xorSuffix (m : ℕ) (r blk : List Bool) (hr : r.length = m) (hblk : blk.length = m) : seedOfList m (Cobham.xorSuffix r blk) = shift (seedOfList m r) (seedOfList m blk)

The decoded exclusive-or is the shift action on decoded seeds.

theorem Complexity.Lautemann.seedOfList_padTo_block (t m : ℕ) (σ w : List Bool) (hσ : σ.length = m) (i : Fin t) : seedOfList m (padTo σ (Cobham.blockAtIdx m w ↑i)) = shiftsOfList t m w i

The decoded padded block is the decoded shift vector.

The rulers

noncomputable def Complexity.Lautemann.clockStr (pt : Polynomial ℕ) (q : ℕ) (x : List Bool) : List Bool

The clock string for the path simulations: long enough for every block.

Equations

• Complexity.Lautemann.clockStr pt q x = x ++ (Complexity.Cobham.polyLen pt x ++ List.replicate (q + 3) false)

@[simp]

theorem Complexity.Lautemann.clockStr_length (pt : Polynomial ℕ) (q : ℕ) (x : List Bool) : (clockStr pt q x).length = x.length + Polynomial.eval x.length pt + (q + 3)

noncomputable def Complexity.Lautemann.runsStr (pt : Polynomial ℕ) (x : List Bool) : List Bool

The ruler whose length is the number of amplification trials.

Equations

• Complexity.Lautemann.runsStr pt x = List.replicate 133 false ++ Complexity.smash (List.replicate 12 false) (Complexity.Cobham.polyLen pt x)

@[simp]

theorem Complexity.Lautemann.runsStr_length (pt : Polynomial ℕ) (x : List Bool) : (runsStr pt x).length = ampRuns (fun (x : ℕ) => Polynomial.eval x pt) x.length

noncomputable def Complexity.Lautemann.seedStr (pt : Polynomial ℕ) (x : List Bool) : List Bool

The ruler whose length is the amplified seed length.

Equations

• Complexity.Lautemann.seedStr pt x = Complexity.smash (Complexity.Lautemann.runsStr pt x) (Complexity.Cobham.polyLen pt x)

@[simp]

theorem Complexity.Lautemann.seedStr_length (pt : Polynomial ℕ) (x : List Bool) : (seedStr pt x).length = ampRuns (fun (x : ℕ) => Polynomial.eval x pt) x.length * Polynomial.eval x.length pt

noncomputable def Complexity.Lautemann.shiftStr (pt : Polynomial ℕ) (x : List Bool) : List Bool

The ruler whose length is the number of shifts.

Equations

• Complexity.Lautemann.shiftStr pt x = false :: Complexity.Lautemann.seedStr pt x

@[simp]

theorem Complexity.Lautemann.shiftStr_length (pt : Polynomial ℕ) (x : List Bool) : (shiftStr pt x).length = ampShifts (fun (x : ℕ) => Polynomial.eval x pt) x.length

The verdict as an algebra function

noncomputable def Complexity.Lautemann.matrixFn {k : ℕ} (tm : NTM k) (pt : Polynomial ℕ) (b : Bool) (z : List Bool) : List Bool

The matrix verdict, computed from the decoded components with the rulers above: check the seed's length, then take the disjunction over shift blocks of the amplified majority verdict.

Equations

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

theorem Complexity.Lautemann.verdictFlag_shift_iff {k : ℕ} (tm : NTM k) (pt : Polynomial ℕ) (b : Bool) (x w r : List Bool) (hr : r.length = ampRuns (fun (x : ℕ) => Polynomial.eval x pt) x.length * Polynomial.eval x.length pt) (i : Fin (ampShifts (fun (x : ℕ) => Polynomial.eval x pt) x.length)) : Cobham.verdictFlag tm b (clockStr pt (Fintype.card tm.Q) x) x (Cobham.polyLen pt x) (Cobham.xorSuffix r (padTo (seedStr pt x) (Cobham.blockAtIdx (seedStr pt x).length w ↑i))) (runsStr pt x) = [true] ↔ blockMajority (tm.repeatAcceptEvent x (Polynomial.eval x.length pt)) (shift (seedOfList (ampRuns (fun (x : ℕ) => Polynomial.eval x pt) x.length * Polynomial.eval x.length pt) r) (shiftsOfList (ampShifts (fun (x : ℕ) => Polynomial.eval x pt) x.length) (ampRuns (fun (x : ℕ) => Polynomial.eval x pt) x.length * Polynomial.eval x.length pt) w i)) = b

The per-shift verdict is the amplified majority at that shift.

theorem Complexity.Lautemann.matrixFn_eq {k : ℕ} (tm : NTM k) (pt : Polynomial ℕ) (b : Bool) (z : List Bool) : matrixFn tm pt b z = [matrixVerdict tm (fun (x : ℕ) => Polynomial.eval x pt) b z]

The algebra function computes the matrix verdict.

Membership in the algebra

theorem Complexity.Lautemann.fstBlock_cobham {n : ℕ} {g : (Fin n → List Bool) → List Bool} (hg : Cobham g) : Cobham fun (v : Fin n → List Bool) => pairFst (g v)

The pair decoders are in the algebra, being polynomial-time.

theorem Complexity.Lautemann.sndBlock_cobham {n : ℕ} {g : (Fin n → List Bool) → List Bool} (hg : Cobham g) : Cobham fun (v : Fin n → List Bool) => pairSnd (g v)

theorem Complexity.Lautemann.clockStr_mem {n : ℕ} (pt : Polynomial ℕ) (q : ℕ) {g : (Fin n → List Bool) → List Bool} (hg : Cobham g) : Cobham fun (v : Fin n → List Bool) => clockStr pt q (g v)

theorem Complexity.Lautemann.runsStr_mem {n : ℕ} (pt : Polynomial ℕ) {g : (Fin n → List Bool) → List Bool} (hg : Cobham g) : Cobham fun (v : Fin n → List Bool) => runsStr pt (g v)

theorem Complexity.Lautemann.seedStr_mem {n : ℕ} (pt : Polynomial ℕ) {g : (Fin n → List Bool) → List Bool} (hg : Cobham g) : Cobham fun (v : Fin n → List Bool) => seedStr pt (g v)

theorem Complexity.Lautemann.shiftStr_mem {n : ℕ} (pt : Polynomial ℕ) {g : (Fin n → List Bool) → List Bool} (hg : Cobham g) : Cobham fun (v : Fin n → List Bool) => shiftStr pt (g v)

theorem Complexity.Lautemann.matrixFn_mem {k : ℕ} (tm : NTM k) (pt : Polynomial ℕ) (b : Bool) : Cobham fun (v : Fin 1 → List Bool) => matrixFn tm pt b (v 0)

The matrix verdict is in the algebra.

theorem Complexity.Lautemann.matrixVerdict_mem_FP {k : ℕ} (tm : NTM k) (pt : Polynomial ℕ) (b : Bool) : (fun (z : List Bool) => [matrixVerdict tm (fun (x : ℕ) => Polynomial.eval x pt) b z]) ∈ FP

The matrix verdict is polynomial-time computable.