Executable raw-circuit witnesses for MCSP

This module exposes the finite witness relation underlying the eventual proof that MCSP is in NP. The relation reuses the existing canonical raw-circuit decoder and evaluator and is proved equivalent to the typed MCSP semantics.

@[simp]

theorem Complexity.MCSP.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 witness relation.

theorem Complexity.MCSP.Instance.isRawCircuitWitness_encodeCircuit (inst : Instance) [NeZero inst.arity] {internalGates : ℕ} (circuit : Circuit Basis.andOr2 inst.arity 1 internalGates) (hsize : circuit.size ≤ inst.threshold) (hcomputes : circuit.Computes inst.function) : inst.IsRawCircuitWitness (CircuitCode.encodeCircuit circuit)

Serializing any typed circuit within the threshold yields a valid raw MCSP witness with identical truth-table semantics.

theorem Complexity.MCSP.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 instance threshold.

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

An instance has a sufficiently small typed circuit exactly when it has a finite canonical raw-circuit witness, including the zero-arity convention.

theorem Complexity.MCSP.Instance.IsRawCircuitWitness.mono (inst : Instance) {first second : ℕ} (hthreshold : first ≤ second) {code : List Bool} (hwitness : (inst.withThreshold first).IsRawCircuitWitness code) : (inst.withThreshold second).IsRawCircuitWitness code

Increasing only the threshold preserves every valid raw-circuit witness.

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

Every valid raw witness satisfies the concrete serialization bound; this controls all accepted witnesses, not only a selected completeness witness.

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

Every MCSP yes-instance has a raw witness within the explicit serialization bound. Threshold normalization is still required before treating this as a polynomial bound in encoded instance length.