Width-five branching-program codec internals

This module proves round-trip and length properties of the canonical codec. Public statements are re-exported by Complexitylib.Circuits.BranchingProgramEncoding.

theorem Complexity.BPCode.Perm5.table_length_internal : table.length = 120

Internal cardinality check for the explicit S₅ table.

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

Internal completeness of the fixed permutation table.

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

Internal proof that every canonical permutation rank fits in seven bits.

theorem Complexity.BPCode.Perm5.length_encode_internal (permutation : Equiv.Perm (Fin 5)) : (encode permutation).length = bitWidth

Internal exact length of a permutation field.

theorem Complexity.BPCode.Perm5.decodePrefix?_encode_append_internal (permutation : Equiv.Perm (Fin 5)) (suffix : List Bool) : decodePrefix? (encode permutation ++ suffix) = some (permutation, suffix)

Internal permutation-prefix round trip.

theorem Complexity.BPCode.Instr.length_encode_internal (instruction : BPInstr 5) : (encode instruction).length = instruction.var + 15

Internal exact instruction-code length.

theorem Complexity.BPCode.Instr.decodePrefix?_encode_append_internal (instruction : BPInstr 5) (suffix : List Bool) : decodePrefix? (encode instruction ++ suffix) = some (instruction, suffix)

Internal instruction-prefix round trip.

theorem Complexity.BPCode.Program.decodeInstructions?_flatMap_encode_append_internal (program : BP 5) (suffix : List Bool) : decodeInstructions? (List.length program) (List.flatMap Instr.encode program ++ suffix) = some (program, suffix)

Internal fixed-count instruction-list round trip.

theorem Complexity.BPCode.Program.decodePrefix?_encode_append_internal (program : BP 5) (suffix : List Bool) : decodePrefix? (encode program ++ suffix) = some (program, suffix)

Internal program-prefix round trip.

theorem Complexity.BPCode.Program.decode?_encode_internal (program : BP 5) : decode? (encode program) = some program

Internal exact-decoder round trip.

theorem Complexity.BPCode.Program.encode_injective_internal : Function.Injective encode

Internal proof that canonical program serialization is injective.

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

Internal proof that exact decoding rejects a nonempty trailing suffix.

theorem Complexity.BPCode.Program.length_encode_internal (program : BP 5) : (encode program).length = List.length program + 1 + (List.map (fun (instruction : BPInstr 5) => instruction.var + 15) program).sum

Internal exact program-code length.

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

Internal polynomial bound when every referenced variable is bounded.