Coin strings from their index

A loop over the coin strings of a verifier receives its index in unary, since that is the form a polynomial-time loop counter takes. This module turns such an index into the coin string itself: the fixed-width binary counter of SavitchBits is incremented that many times, starting from all zeros.

Nothing here is arithmetic on the index. bumpBits is the width-preserving increment already proved polynomial-time for Savitch's theorem, and iterating a polynomial-time step a polynomial number of times is iterate_mem_FP.

Main results

• Complexity.coinStr — the counter after that many increments
• Complexity.coinStr_mem_FP — in polynomial time, for any index
• Complexity.toList_coinOfIndex — it is the coin string SubsetNP names

theorem Complexity.zeroBlockFn_mem_FP {a : List Bool → List Bool} (ha : a ∈ FP) : (fun (z : List Bool) => List.replicate (a z).length false) ∈ FP

A block of zeros as wide as a computed string.

theorem Complexity.bumpBits_mem_FP : bumpBits ∈ FP

theorem Complexity.length_bumpBits_iterate (n : ℕ) (w : List Bool) : (bumpBits^[n] w).length = w.length

def Complexity.coinStr (t c : ℕ) : List Bool

The width-t counter after c increments. Total: past 2 ^ t it wraps, which never happens where it is used but keeps the function unconditional.

Equations

• Complexity.coinStr t c = Complexity.bumpBits^[c] (List.replicate t false)

theorem Complexity.coinStr_eq {t c : ℕ} (h : c < 2 ^ t) : coinStr t c = bitsOfLenLE t c

theorem Complexity.coinStr_mem_FP {t c : List Bool → ℕ} (ht : (fun (z : List Bool) => List.replicate (t z) true) ∈ FP) (hc : (fun (z : List Bool) => List.replicate (c z) true) ∈ FP) : (fun (z : List Bool) => coinStr (t z) (c z)) ∈ FP

The counter value in polynomial time. With the width and the index both supplied in unary, the counter is polynomial-time computable — with no bound on the index, so that the function is total where a loop guard has not yet been applied.

theorem Complexity.toList_coinOfIndex (t c : ℕ) (h : c < 2 ^ t) : BitString.toList (PCPVerifier.coinOfIndex ⟨c, h⟩) = bitsOfLenLE t c

The counter is the coin string. SubsetNP indexes coin strings by their little-endian binary value, which is exactly what the counter holds.

theorem Complexity.coinIndex_coinOfIndex {t : ℕ} (c : Fin (2 ^ t)) : PCPVerifier.coinIndex (PCPVerifier.coinOfIndex c) = ↑c

The index of the coin string an index names.

theorem Complexity.binValLE_toList {T : ℕ} (ρ : Fin T → Bool) : binValLE (BitString.toList ρ) = PCPVerifier.coinIndex ρ

The value of a coin string is its index.

noncomputable def Complexity.coinEquiv (T : ℕ) : Fin (2 ^ T) ≃ (Fin T → Bool)

Coin strings and their indices are in bijection.

Equations

• Complexity.coinEquiv T = { toFun := Complexity.PCPVerifier.coinOfIndex, invFun := fun (ρ : Fin T → Bool) => ⟨Complexity.PCPVerifier.coinIndex ρ, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

theorem Complexity.card_filter_coinIndex (T : ℕ) (Q : ℕ → Prop) [DecidablePred Q] : {ρ : Fin T → Bool | Q (PCPVerifier.coinIndex ρ)}.card = (Finset.filter Q (Finset.range (2 ^ T))).card

Counting coin strings is counting indices.