Executable raw-circuit witnesses for MCSP -- definitions

This layer turns the mathematical MCSP predicate into a finite witness relation over the existing machine-facing circuit syntax. Positive-arity witnesses must be exact canonical CircuitCode.RawCircuit encodings, satisfy the size threshold, and agree with every truth-table entry. The unique zero-arity function uses the empty witness, matching its size-zero convention.

verifyRawCircuit is executable, but this module does not yet claim a machine time bound or membership in NP. In particular, its code-length bound still depends on the numeric threshold; oversized binary thresholds must be normalized before the final NP packaging.

def Complexity.MCSP.Instance.IsRawCircuitWitness (inst : Instance) (code : List Bool) : Prop

A canonical encoded raw circuit witnesses that an MCSP instance is small.

At positive arity, verification checks syntax, size, and all 2^arity truth-table entries. At arity zero, the unique canonical witness is empty.

Equations

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

@[instance_reducible]

instance Complexity.MCSP.Instance.instDecidableIsRawCircuitWitness (inst : Instance) (code : List Bool) : Decidable (inst.IsRawCircuitWitness code)

Equations

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

def Complexity.MCSP.Instance.verifyRawCircuit (inst : Instance) (code : List Bool) : Bool

Executable Boolean checker for the raw-circuit witness relation.

Equations

• inst.verifyRawCircuit code = decide (inst.IsRawCircuitWitness code)

def Complexity.MCSP.Instance.rawWitnessCodeLengthBound (inst : Instance) : ℕ

Concrete code-length envelope obtained by serializing a typed circuit no larger than the instance threshold. This is not yet polynomial in encoded input length when the binary threshold is oversized.

Equations

• inst.rawWitnessCodeLengthBound = 1 + inst.threshold * (2 * (inst.arity + inst.threshold) + 6)