Encodings of whole circuit families

This module adds the length-zero wrapper around the positive-arity circuit codec. A leading tag distinguishes the explicit empty-input answer from an ordinary encoded circuit.

def Complexity.CircuitFamily.encodeAt (F : CircuitFamily Basis.andOr2) (n : ℕ) : List Bool

Encode the member of an AND/OR circuit family at input length n.

The zero-length member is the tag false followed by its explicit answer. Positive lengths use the tag true followed by the ordinary circuit code.

Equations

• F.encodeAt 0 = [false, F.emptyOutput]
• F.encodeAt n.succ = true :: Complexity.CircuitCode.encodeCircuit (F.circuit (n + 1))

@[simp]

theorem Complexity.CircuitFamily.encodeAt_zero (F : CircuitFamily Basis.andOr2) : F.encodeAt 0 = [false, F.emptyOutput]

The length-zero member encodes as the false tag followed by the explicit answer bit.

@[simp]

theorem Complexity.CircuitFamily.encodeAt_succ (F : CircuitFamily Basis.andOr2) (n : ℕ) : F.encodeAt (n + 1) = true :: CircuitCode.encodeCircuit (F.circuit (n + 1))

A positive-length member encodes as the true tag followed by its circuit's code.

def Complexity.CircuitCode.evalFamilyCode (code input : List Bool) : Option Bool

Evaluate a tagged family code on a variable-length input.

The zero tag is accepted only for the empty input and must carry exactly one answer bit. The positive tag is accepted only for a nonempty input and delegates to the exact-arity circuit evaluator.

Equations

• Complexity.CircuitCode.evalFamilyCode [false, answer] input = if input.isEmpty = true then some answer else none
• Complexity.CircuitCode.evalFamilyCode (true :: circuitCode) input = if input.isEmpty = true then none else Complexity.CircuitCode.evalCode input.length circuitCode input
• Complexity.CircuitCode.evalFamilyCode code input = if input.isEmpty = true then none else none

def Complexity.CircuitCode.evalFamilyPair? (z : List Bool) : Option Bool

Decode one self-delimiting machine input into a tagged family code and its argument, then evaluate the code. Malformed outer pairs and malformed inner circuit codes both return none.

Equations

• Complexity.CircuitCode.evalFamilyPair? z = (Complexity.unpair? z).bind fun (x : List Bool × List Bool) => match x with | (code, input) => Complexity.CircuitCode.evalFamilyCode code input

@[simp]

theorem Complexity.CircuitCode.evalFamilyPair?_pair (code input : List Bool) : evalFamilyPair? (pair code input) = evalFamilyCode code input

Evaluating a canonical pair delegates directly to the tagged family-code evaluator.

theorem Complexity.CircuitCode.evalFamilyCode_nil_isSome_iff (code : List Bool) : (evalFamilyCode code []).isSome = true ↔ ∃ (answer : Bool), code = [false, answer]

On the empty input, successful evaluation is exactly a canonical zero tag carrying one answer bit.

theorem Complexity.CircuitCode.evalFamilyCode_isSome_iff_of_ne_nil (code input : List Bool) (hne : input ≠ []) : (evalFamilyCode code input).isSome = true ↔ ∃ (circuit : RawCircuit), code = true :: circuit.encode ∧ RawCircuit.WellFormed input.length circuit

On a nonempty input, successful evaluation is exactly a positive tag carrying a canonical, topologically well-formed circuit code.

@[simp]

theorem Complexity.CircuitCode.evalFamilyCode_encodeAt (F : CircuitFamily Basis.andOr2) {n : ℕ} (input : BitString n) : evalFamilyCode (F.encodeAt n) input.toList = some (F.function n input)

Tagged family encoding handles the explicit empty-input bit and agrees with the typed circuit at every positive input length.

@[simp]

theorem Complexity.CircuitCode.evalFamilyCode_encodeAt_length (F : CircuitFamily Basis.andOr2) (input : List Bool) : evalFamilyCode (F.encodeAt input.length) input = some (F.evalList input)

Machine-facing list form of evalFamilyCode_encodeAt: selecting the member at the supplied input's length agrees with CircuitFamily.evalList.

theorem Complexity.CircuitCode.evalFamilyPair?_encodeAt (F : CircuitFamily Basis.andOr2) (input : List Bool) : evalFamilyPair? (pair (F.encodeAt input.length) input) = some (F.evalList input)

Pairing a family member's canonical code with its input evaluates to the family's Boolean answer.

theorem Complexity.CircuitCode.encodeAt_zero_length (F : CircuitFamily Basis.andOr2) : (F.encodeAt 0).length = 2

The length-zero tagged code has exactly two bits: the tag and the answer.

@[simp]

theorem Complexity.CircuitCode.encodeAt_succ_length (F : CircuitFamily Basis.andOr2) (n : ℕ) : (F.encodeAt (n + 1)).length = (encodeCircuit (F.circuit (n + 1))).length + 1

A positive-length tagged code is one bit (the tag) longer than the underlying circuit code.

theorem Complexity.CircuitCode.encodeAt_succ_length_le (F : CircuitFamily Basis.andOr2) (n : ℕ) : (F.encodeAt (n + 1)).length ≤ 2 + F.size (n + 1) * (2 * (n + 1 + F.size (n + 1)) + 6)

The positive-length tagged family code inherits the concrete polynomial bound for its member circuit.

theorem Complexity.CircuitCode.encodeAt_length_le (F : CircuitFamily Basis.andOr2) (n : ℕ) : (F.encodeAt n).length ≤ 2 + F.size n * (2 * (n + F.size n) + 6)

Every tagged family code satisfies the concrete length bound, including the explicit two-bit code at input length zero.

theorem Complexity.CircuitCode.encodeAt_length_bigO (F : CircuitFamily Basis.andOr2) {d : ℕ} (hsize : BigO F.size fun (x : ℕ) => x ^ d) : BigO (fun (n : ℕ) => (F.encodeAt n).length) fun (x : ℕ) => x ^ (2 * (d + 1))

Polynomial-size families have polynomial-length tagged member encodings.