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. BinCounter turns such an index into a fixed-width binary counter; this module identifies that counter with the coin string SubsetNP names, and relates counting coin strings to counting their indices.

Main definitions

• Complexity.coinEquiv — coin strings and their indices are in bijection

Main results

• Complexity.toList_coinOfIndex — the counter is the coin string SubsetNP names
• Complexity.binValLE_toList — the value of a coin string is its index
• Complexity.card_filter_coinIndex — counting coin strings is counting indices

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.