Documentation

Complexitylib.Circuits.BranchingProgramEncoding

Canonical encoding of width-five branching programs #

This module exposes the machine-facing codec used by the uniform Barrington track. Every S₅ permutation is ranked in a fixed computable table and stored in seven bits. Instructions add a terminated-unary variable index, and a program adds a terminated-unary instruction count.

The exact decoder is a left inverse, serialization is injective, nonempty trailing data is rejected, and the code length is explicit. Consequently the remaining uniformity proof can target one stable bit format without carrying finite permutation proofs on the machine tape.

Main results #

source
theorem Complexity.BPCode.Perm5.table_length :
table.length = 120

The explicit permutation table has exactly 5! = 120 entries.

source
theorem Complexity.BPCode.Perm5.mem_table (permutation : Equiv.Perm (Fin 5)) :
permutation ∈ table

Every permutation of Fin 5 occurs in the fixed table.

source
theorem Complexity.BPCode.Perm5.index_lt_two_pow (permutation : Equiv.Perm (Fin 5)) :
index permutation < 2 ^ bitWidth

Every canonical table position fits in the seven-bit field.

source
@[simp]
theorem Complexity.BPCode.Perm5.length_encode (permutation : Equiv.Perm (Fin 5)) :
(encode permutation).length = bitWidth

Every encoded permutation field has the fixed width of seven bits.

source
@[simp]
theorem Complexity.BPCode.Perm5.decodePrefix?_encode_append (permutation : Equiv.Perm (Fin 5)) (suffix : List Bool) :
decodePrefix? (encode permutation ++ suffix) = some (permutation, suffix)

Decoding an encoded permutation in front of any suffix recovers both.

source
@[simp]
theorem Complexity.BPCode.Instr.length_encode (instruction : BPInstr 5) :
(encode instruction).length = instruction.var + 15

An instruction uses its unary variable length plus fourteen permutation bits, for a total of var + 15.

source
@[simp]
theorem Complexity.BPCode.Instr.decodePrefix?_encode_append (instruction : BPInstr 5) (suffix : List Bool) :
decodePrefix? (encode instruction ++ suffix) = some (instruction, suffix)

Decoding an encoded instruction in front of any suffix recovers both.

source
@[simp]
theorem Complexity.BPCode.Program.decodeInstructions?_flatMap_encode_append (program : BP 5) (suffix : List Bool) :
decodeInstructions? (List.length program) (List.flatMap Instr.encode program ++ suffix) = some (program, suffix)

Fixed-count decoding consumes exactly the requested encoded instructions.

source
@[simp]
theorem Complexity.BPCode.Program.decodePrefix?_encode_append (program : BP 5) (suffix : List Bool) :
decodePrefix? (encode program ++ suffix) = some (program, suffix)

Prefix decoding preserves a caller-supplied suffix.

source
@[simp]
theorem Complexity.BPCode.Program.decode?_encode (program : BP 5) :
decode? (encode program) = some program

Exact decoding is a left inverse of canonical serialization.

source
theorem Complexity.BPCode.Program.encode_injective :
Function.Injective encode

Canonical program serialization is injective.

source
theorem Complexity.BPCode.Program.decode?_encode_append_eq_none (program : BP 5) {suffix : List Bool} (hsuffix : suffix ≠ []) :
decode? (encode program ++ suffix) = none

Exact decoding rejects nonempty trailing data.

source
@[simp]
theorem Complexity.BPCode.Program.length_encode (program : BP 5) :
(encode program).length = List.length program + 1 + (List.map (fun (instruction : BPInstr 5) => instruction.var + 15) program).sum

Exact code length: one unary count field plus all instruction fields.

source
theorem Complexity.BPCode.Program.length_encode_le (program : BP 5) (variableBound : ℕ) (hvars : ∀ instruction ∈ program, instruction.var ≤ variableBound) :
(encode program).length ≤ List.length program + 1 + List.length program * (variableBound + 15)

If all variable indices are bounded, serialization has the corresponding linear-in-program-length bound.