Looping over the blocks of a string inside the algebra

Amplified acceptance is a majority vote over the blocks of a random seed. Both that vote and the outer disjunction over shift blocks are limited recursions over a ruler whose length is the iteration count: at the step whose tail is y, the block index is |y|, so the block itself is cut out of the source string by a drop of |y| · |τ| bits — a length smash produces — followed by a take of |τ|. No state has to be threaded through the recursion.

Main definitions

• Cobham.blockAtIdx — the j-th block of a string at a given width
• Cobham.acceptCountAux — unary count of blocks on which the path accepts
• Cobham.majorityFlag — the amplified majority verdict as a flag

Main results

• Cobham.acceptCountAux_length — the count is the number of accepting blocks
• Cobham.acceptCountAux_mem, Cobham.majorityFlag_mem — both are in the algebra

def Complexity.Cobham.blockAtIdx (w : ℕ) (s : List Bool) (j : ℕ) : List Bool

The j-th block of s at width w.

Equations

• Complexity.Cobham.blockAtIdx w s j = List.take w (List.drop (j * w) s)

def Complexity.Cobham.blockOf (τ s idx : List Bool) : List Bool

The block of s selected by the ruler idx at the width of τ.

Equations

• Complexity.Cobham.blockOf τ s idx = List.take τ.length (List.drop (Complexity.smash idx τ).length s)

@[simp]

theorem Complexity.Cobham.blockOf_eq (τ s idx : List Bool) : blockOf τ s idx = blockAtIdx τ.length s idx.length

theorem Complexity.Cobham.blockOf_mem {n : ℕ} {gτ gs gidx : (Fin n → List Bool) → List Bool} (hτ : Cobham gτ) (hs : Cobham gs) (hidx : Cobham gidx) : Cobham fun (v : Fin n → List Bool) => blockOf (gτ v) (gs v) (gidx v)

Counting accepting blocks

noncomputable def Complexity.Cobham.acceptCountAux {k : ℕ} (tm : NTM k) (u x τ s : List Bool) : List Bool → List Bool

Unary count of the blocks of s on which the path of tm accepts: one bit per accepting block. The recursion runs once per bit of ρ, and the block index at each step is the length of the remaining tail.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.Cobham.acceptCountAux tm u x τ s [] = []

theorem Complexity.Cobham.acceptCountAux_length {k : ℕ} (tm : NTM k) (u x τ s ρ : List Bool) : (acceptCountAux tm u x τ s ρ).length = ∑ j ∈ Finset.range ρ.length, if acceptChoiceFn tm u x (blockAtIdx τ.length s j) = [true] then 1 else 0

The count is the number of accepting block indices below |ρ|.

theorem Complexity.Cobham.acceptCountAux_mem {k n : ℕ} (tm : NTM k) {gu gx gτ gs gρ : (Fin n → List Bool) → List Bool} (hu : Cobham gu) (hx : Cobham gx) (hτ : Cobham gτ) (hs : Cobham gs) (hρ : Cobham gρ) : Cobham fun (v : Fin n → List Bool) => acceptCountAux tm (gu v) (gx v) (gτ v) (gs v) (gρ v)

The count is in the algebra.

The amplified verdict

noncomputable def Complexity.Cobham.majorityFlag {k : ℕ} (tm : NTM k) (u x τ s ρ : List Bool) : List Bool

The amplified majority verdict as a flag: strictly more than half of the |ρ| blocks of s accept.

Equations

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

theorem Complexity.Cobham.majorityFlag_flag {k : ℕ} (tm : NTM k) (u x τ s ρ : List Bool) : majorityFlag tm u x τ s ρ = [true] ∨ majorityFlag tm u x τ s ρ = [false]

theorem Complexity.Cobham.majorityFlag_eq_true_iff {k : ℕ} (tm : NTM k) (u x τ s ρ : List Bool) : majorityFlag tm u x τ s ρ = [true] ↔ ρ.length < 2 * (acceptCountAux tm u x τ s ρ).length

theorem Complexity.Cobham.majorityFlag_mem {k n : ℕ} (tm : NTM k) {gu gx gτ gs gρ : (Fin n → List Bool) → List Bool} (hu : Cobham gu) (hx : Cobham gx) (hτ : Cobham gτ) (hs : Cobham gs) (hρ : Cobham gρ) : Cobham fun (v : Fin n → List Bool) => majorityFlag tm (gu v) (gx v) (gτ v) (gs v) (gρ v)

noncomputable def Complexity.Cobham.verdictFlag {k : ℕ} (tm : NTM k) (b : Bool) (u x τ s ρ : List Bool) : List Bool

The verdict sought at a shift: the amplified majority, or its negation.

Equations

• Complexity.Cobham.verdictFlag tm b u x τ s ρ = bif b then Complexity.Cobham.majorityFlag tm u x τ s ρ else Complexity.notBit (Complexity.Cobham.majorityFlag tm u x τ s ρ)

theorem Complexity.Cobham.verdictFlag_flag {k : ℕ} (tm : NTM k) (b : Bool) (u x τ s ρ : List Bool) : verdictFlag tm b u x τ s ρ = [true] ∨ verdictFlag tm b u x τ s ρ = [false]

theorem Complexity.Cobham.verdictFlag_mem {k n : ℕ} (tm : NTM k) (b : Bool) {gu gx gτ gs gρ : (Fin n → List Bool) → List Bool} (hu : Cobham gu) (hx : Cobham gx) (hτ : Cobham gτ) (hs : Cobham gs) (hρ : Cobham gρ) : Cobham fun (v : Fin n → List Bool) => verdictFlag tm b (gu v) (gx v) (gτ v) (gs v) (gρ v)

Disjunction over shifts

noncomputable def Complexity.Cobham.anyShiftAux {k : ℕ} (tm : NTM k) (b : Bool) (u x τ ρ σ r wit : List Bool) : List Bool → List Bool

Disjunction of the verdict over the shift blocks of wit: the recursion runs once per bit of the shift ruler, and at each step the shift block is cut from wit at the index given by the remaining tail.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.Cobham.anyShiftAux tm b u x τ ρ σ r wit [] = [false]

theorem Complexity.Cobham.anyShiftAux_flag {k : ℕ} (tm : NTM k) (b : Bool) (u x τ ρ σ r wit ι : List Bool) : anyShiftAux tm b u x τ ρ σ r wit ι = [true] ∨ anyShiftAux tm b u x τ ρ σ r wit ι = [false]

theorem Complexity.Cobham.anyShiftAux_eq_true_iff {k : ℕ} (tm : NTM k) (b : Bool) (u x τ ρ σ r wit ι : List Bool) : anyShiftAux tm b u x τ ρ σ r wit ι = [true] ↔ ∃ i < ι.length, verdictFlag tm b u x τ (xorSuffix r (padTo σ (blockAtIdx σ.length wit i))) ρ = [true]

The disjunction is exactly an existential over shift indices.

theorem Complexity.Cobham.anyShiftAux_mem {k n : ℕ} (tm : NTM k) (b : Bool) {gu gx gτ gρ gσ gr gwit gι : (Fin n → List Bool) → List Bool} (hu : Cobham gu) (hx : Cobham gx) (hτ : Cobham gτ) (hρ : Cobham gρ) (hσ : Cobham gσ) (hr : Cobham gr) (hwit : Cobham gwit) (hι : Cobham gι) : Cobham fun (v : Fin n → List Bool) => anyShiftAux tm b (gu v) (gx v) (gτ v) (gρ v) (gσ v) (gr v) (gwit v) (gι v)

The disjunction over shifts is in the algebra.

Membership among blocks

def Complexity.Cobham.memBlockAux (τ s c : List Bool) : List Bool → List Bool

Flag: the block c occurs among the width-|τ| blocks of s indexed by the ruler.

Equations

• Complexity.Cobham.memBlockAux τ s c [] = [false]
• Complexity.Cobham.memBlockAux τ s c (head :: y) = Complexity.orBit (Complexity.Cobham.eqFlag c (Complexity.Cobham.blockOf τ s y)) (Complexity.Cobham.memBlockAux τ s c y)

theorem Complexity.Cobham.memBlockAux_flag (τ s c ι : List Bool) : memBlockAux τ s c ι = [true] ∨ memBlockAux τ s c ι = [false]

theorem Complexity.Cobham.memBlockAux_eq_true_iff (τ s c ι : List Bool) : memBlockAux τ s c ι = [true] ↔ ∃ i < ι.length, blockAtIdx τ.length s i = c

The membership test is an existential over block indices.

theorem Complexity.Cobham.memBlockAux_mem {n : ℕ} {gτ gs gc gι : (Fin n → List Bool) → List Bool} (hτ : Cobham gτ) (hs : Cobham gs) (hc : Cobham gc) (hι : Cobham gι) : Cobham fun (v : Fin n → List Bool) => memBlockAux (gτ v) (gs v) (gc v) (gι v)

The membership test is in the algebra.