Minimum Circuit Size Problem -- definitions

This definitions layer gives MCSP a total, canonical input format and pins its semantics to Complexitylib's exact fan-in-two circuit convention. An instance stores an arity n, a typed 2^n-entry truth table, and a size threshold. Truth-table position k denotes the input whose variable j is bit j of k, so variables are enumerated in little-endian order.

Positive arities use Basis.andOr2: primary inputs and negation flags are free, while every internal and output gate is counted. The circuit type intentionally has no zero-input member. Following CircuitFamily.size, the unique zero-input answer is therefore stored directly and assigned size zero.

The codec is total. It rejects malformed pairing, noncanonical binary natural fields, a truth table of the wrong length, and trailing data. Malformed strings are outside MCSP.

structure Complexity.MCSP.Instance : Type

A well-formed MCSP instance with a structurally exact truth-table length.

• arity : ℕ

  Number of inputs of the represented Boolean function.

• table : BitString (2 ^ self.arity)

  Function values in increasing little-endian input-index order.

• threshold : ℕ

  Maximum allowed circuit size.

def Complexity.MCSP.Instance.tableBits (inst : Instance) : List Bool

Truth-table bits as their canonical variable-length machine payload.

Equations

• inst.tableBits = inst.table.toList

def Complexity.MCSP.Instance.inputIndex {arity : ℕ} (input : BitString arity) : Fin (2 ^ arity)

Interpret an input as its little-endian truth-table index.

Equations

• Complexity.MCSP.Instance.inputIndex input = ⟨Nat.fromBitsLE input.toList, ⋯⟩

def Complexity.MCSP.Instance.inputOfIndex {arity : ℕ} (index : Fin (2 ^ arity)) : BitString arity

Decode a truth-table index as its fixed-width little-endian input.

Equations

• Complexity.MCSP.Instance.inputOfIndex index = Complexity.BitString.ofList (arity.toBitsLE ↑index) ⋯

def Complexity.MCSP.Instance.function (inst : Instance) : BitString inst.arity → Bool

The Boolean function denoted by an instance's truth table.

Equations

• inst.function input = inst.table (Complexity.MCSP.Instance.inputIndex input)

def Complexity.MCSP.Instance.ofFunction (arity threshold : ℕ) (f : BitString arity → Bool) : Instance

Package a Boolean function as its exact canonical truth table at a chosen MCSP threshold.

Equations

• Complexity.MCSP.Instance.ofFunction arity threshold f = { arity := arity, table := fun (index : Fin (2 ^ arity)) => f (Complexity.MCSP.Instance.inputOfIndex index), threshold := threshold }

def Complexity.MCSP.Instance.withThreshold (inst : Instance) (threshold : ℕ) : Instance

Replace only the size threshold of an instance.

Equations

• inst.withThreshold threshold = { arity := inst.arity, table := inst.table, threshold := threshold }

def Complexity.MCSP.Instance.encode (inst : Instance) : List Bool

Canonically encode arity, threshold, and the exact truth-table payload.

The natural fields use minimal little-endian binary and the two nested pairs make both field boundaries self-delimiting.

Equations

• inst.encode = Complexity.pair (Complexity.BinaryNatCode.encode inst.arity) (Complexity.pair (Complexity.BinaryNatCode.encode inst.threshold) inst.tableBits)

def Complexity.MCSP.Instance.decode? (bits : List Bool) : Option Instance

Decode exactly one canonical MCSP instance.

Every failure mode returns none, including a truth-table payload whose length differs from 2^arity.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Complexity.MCSP.Instance.minimumSize (inst : Instance) : ℕ

Minimum circuit size under the library's total MCSP convention.

At positive arity this is exactly Circuit.sizeComplexity Basis.andOr2. At arity zero it is zero, matching the explicit-bit convention used by CircuitFamily.

Equations

• inst.minimumSize = if harity : inst.arity = 0 then 0 else Complexity.Circuit.sizeComplexity Complexity.Basis.andOr2 inst.function

def Complexity.MCSP.Instance.HasCircuitAtMost (inst : Instance) : Prop

A direct circuit-witness formulation of an MCSP yes-instance.

For positive arity this asks for a typed circuit no larger than the threshold. At arity zero the separately stored answer has size zero, so every natural threshold accepts it.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.MCSP : Set (List Bool)

The total Minimum Circuit Size Problem over canonical encoded instances.

Malformed strings are no-instances. Positive-arity size uses Basis.andOr2; zero arity uses the explicit size-zero convention documented on MCSP.Instance.minimumSize.

Equations

• Complexity.MCSP = {bits : List Bool | match Complexity.MCSP.Instance.decode? bits with | some inst => inst.HasCircuitAtMost | none => False}