Executable raw-circuit witnesses for SuccinctMCSP

This module exposes the finite witness relation for sampled circuit minimization. It reuses the canonical machine-facing circuit decoder and evaluator, checks every listed sample, and agrees exactly with the typed SuccinctMCSP.Instance.HasCircuitAtMost predicate. Zero arity uses a one-bit constant witness rather than the positive-arity circuit encoding.

@[simp]

theorem Complexity.SuccinctMCSP.Instance.verifyRawCircuit_eq_true_iff (inst : Instance) (code : List Bool) : inst.verifyRawCircuit code = true ↔ inst.IsRawCircuitWitness code

The Boolean raw-circuit verifier decides its advertised relation.

theorem Complexity.SuccinctMCSP.Instance.isRawCircuitWitness_encodeCircuit (inst : Instance) [NeZero inst.arity] {internalGates : ℕ} (circuit : Circuit Basis.andOr2 inst.arity 1 internalGates) (hsize : circuit.size ≤ inst.threshold) (hsamples : inst.SamplesFunction fun (input : BitString inst.arity) => circuit.eval input 0) : inst.IsRawCircuitWitness (CircuitCode.encodeCircuit circuit)

Serializing a positive-arity typed circuit within the threshold produces a witness matching exactly the listed samples.

theorem Complexity.SuccinctMCSP.Instance.hasCircuitAtMost_of_isRawCircuitWitness (inst : Instance) [NeZero inst.arity] {code : List Bool} (hwitness : inst.IsRawCircuitWitness code) : inst.HasCircuitAtMost

Every valid positive-arity raw witness reconstructs a typed circuit within the threshold that matches every listed sample.

theorem Complexity.SuccinctMCSP.Instance.exists_isRawCircuitWitness_iff (inst : Instance) : (∃ (code : List Bool), inst.IsRawCircuitWitness code) ↔ inst.HasCircuitAtMost

Typed sampled feasibility is equivalent to existence of a finite raw witness, including the zero-arity constant convention.

theorem Complexity.SuccinctMCSP.Instance.IsRawCircuitWitness.mono (inst : Instance) {first second : ℕ} (hthreshold : first ≤ second) {code : List Bool} (hwitness : { arity := inst.arity, samples := inst.samples, threshold := first }.IsRawCircuitWitness code) : { arity := inst.arity, samples := inst.samples, threshold := second }.IsRawCircuitWitness code

Increasing the threshold preserves every valid sampled raw witness.

theorem Complexity.SuccinctMCSP.Instance.IsRawCircuitWitness.length_le (inst : Instance) {code : List Bool} (hwitness : inst.IsRawCircuitWitness code) : code.length ≤ inst.rawWitnessCodeLengthBound

Every accepted raw witness satisfies the concrete serialization envelope.

theorem Complexity.SuccinctMCSP.Instance.exists_isRawCircuitWitness_length_le (inst : Instance) (hsmall : inst.HasCircuitAtMost) : ∃ (code : List Bool), inst.IsRawCircuitWitness code ∧ code.length ≤ inst.rawWitnessCodeLengthBound

Every sampled yes-instance has a raw witness within the explicit envelope.

The envelope still depends on the numeric threshold; the normalization layer will turn it into a polynomial bound in encoded input length.