Executable raw-circuit witnesses for SuccinctMCSP -- definitions

This layer checks the existing machine-facing fan-in-two circuit encoding against a sampled instance. Positive-arity witnesses must be canonical raw circuits, fit the size threshold, and match every listed sample. At arity zero, the one-bit witness is the selected constant output and must satisfy every sample.

The relation is executable. Its initial code-length envelope depends on the numeric threshold; a later normalization layer will replace that threshold by a polynomial sampled-circuit upper bound before packaging the relation in FNP.

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

A canonical raw circuit, or a zero-arity constant bit, witnessing sampled circuit feasibility.

Equations

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

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

Executable Boolean checker for sampled raw-circuit witnesses.

Equations

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

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

Serialization envelope for a typed circuit within the stored threshold.

The leading one also covers the zero-arity constant witness.

Equations

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