Gap MCSP -- proof internals

theorem Complexity.GapMCSP.isYes_iff_hasCircuitAtMost_internal (inst : MCSP.Instance) : IsYes inst ↔ inst.HasCircuitAtMost

theorem Complexity.GapMCSP.IsYes.withThreshold_mono_internal (inst : MCSP.Instance) {first second : ℕ} (hthreshold : first ≤ second) (hyes : IsYes (inst.withThreshold first)) : IsYes (inst.withThreshold second)

theorem Complexity.GapMCSP.IsNo.withThreshold_anti_internal {parameters : Parameters} (hmonotone : parameters.ThresholdMonotone) (inst : MCSP.Instance) {first second : ℕ} (hthreshold : first ≤ second) (hno : IsNo parameters (inst.withThreshold second)) : IsNo parameters (inst.withThreshold first)

theorem Complexity.GapMCSP.IsNo.anti_relaxation_internal {first second : Parameters} (hrelax : first.RelaxesTo second) (inst : MCSP.Instance) (hno : IsNo second inst) : IsNo first inst

theorem Complexity.GapMCSP.yesLanguage_eq_MCSP_internal : yesLanguage = MCSP

theorem Complexity.GapMCSP.noLanguage_anti_relaxation_internal {first second : Parameters} (hrelax : first.RelaxesTo second) : noLanguage second ⊆ noLanguage first

theorem Complexity.GapMCSP.disjoint_yesLanguage_noLanguage_internal (parameters : Parameters) (hwidening : parameters.IsWidening) : Disjoint yesLanguage (noLanguage parameters)