Executable raw-circuit witnesses for SuccinctMCSP -- proof internals

This module proves exact equivalence between the executable raw witness relation and the typed sampled-circuit semantics.

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

theorem Complexity.SuccinctMCSP.Instance.isRawCircuitWitness_encodeCircuit_internal (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)

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

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

theorem Complexity.SuccinctMCSP.Instance.isRawCircuitWitness_threshold_mono_internal (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

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

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