Bitstring codecs for seeds and shift tuples

The Lautemann characterization quantifies over seeds Fin m → Bool and over tuples of shifts Fin t → Fin m → Bool, while the polynomial hierarchy quantifies over bitstrings. This file provides the two codecs and their round-trip lemmas: listOfSeed/seedOfList for a single seed, and listOfShifts/shiftsOfList for a tuple, flattened in row-major order.

Decoding is total — out-of-range positions read as false — so a decoder is available on every bitstring, and the length equations pin down the well-formed encodings.

def Complexity.Lautemann.listOfSeed {m : ℕ} (s : Fin m → Bool) : List Bool

Encode a seed as a bitstring, one bit per position.

Equations

• Complexity.Lautemann.listOfSeed s = List.map s (List.finRange m)

def Complexity.Lautemann.seedOfList (m : ℕ) (r : List Bool) : Fin m → Bool

Decode a bitstring as a seed, reading out-of-range positions as false.

Equations

• Complexity.Lautemann.seedOfList m r j = r.getD (↑j) false

@[simp]

theorem Complexity.Lautemann.length_listOfSeed {m : ℕ} (s : Fin m → Bool) : (listOfSeed s).length = m

theorem Complexity.Lautemann.getD_listOfSeed {m : ℕ} (s : Fin m → Bool) (idx : ℕ) (h : idx < m) : (listOfSeed s).getD idx false = s ⟨idx, h⟩

Reading an encoded seed at an in-range position returns that bit.

@[simp]

theorem Complexity.Lautemann.seedOfList_listOfSeed {m : ℕ} (s : Fin m → Bool) : seedOfList m (listOfSeed s) = s

def Complexity.Lautemann.flattenShifts {t m : ℕ} (u : Fin t → Fin m → Bool) : Fin (t * m) → Bool

Flatten a tuple of shifts into a single seed of length t * m, in row-major order.

Equations

• Complexity.Lautemann.flattenShifts u kk = if h : 0 < m then u ⟨↑kk / m, ⋯⟩ ⟨↑kk % m, ⋯⟩ else false

def Complexity.Lautemann.listOfShifts {t m : ℕ} (u : Fin t → Fin m → Bool) : List Bool

Encode a tuple of shifts as a bitstring of length t * m.

Equations

• Complexity.Lautemann.listOfShifts u = Complexity.Lautemann.listOfSeed (Complexity.Lautemann.flattenShifts u)

def Complexity.Lautemann.shiftsOfList (t m : ℕ) (w : List Bool) : Fin t → Fin m → Bool

Decode a bitstring as a tuple of shifts, reading out-of-range positions as false.

Equations

• Complexity.Lautemann.shiftsOfList t m w i j = w.getD (↑i * m + ↑j) false

@[simp]

theorem Complexity.Lautemann.length_listOfShifts {t m : ℕ} (u : Fin t → Fin m → Bool) : (listOfShifts u).length = t * m

@[simp]

theorem Complexity.Lautemann.shiftsOfList_listOfShifts {t m : ℕ} (u : Fin t → Fin m → Bool) : shiftsOfList t m (listOfShifts u) = u