Executable raw-circuit witnesses for MCSP -- proof internals

This module proves exact equivalence between finite raw-circuit witnesses and the typed existential circuit semantics of MCSP.

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

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

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

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

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

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

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