Gap MCSP

Gap MCSP is a genuine promise problem over the existing canonical MCSP codec. The source threshold is part of each instance; an explicit parameter map gives the relaxed no-threshold. The public theory exposes the monotonicity directions needed for quantitative hardness-magnification reductions. Arity-indexed sliceProblem specializes this to the conventional GapMCSP[s_yes, s_no] form and provides exact table-preserving threshold re-encoding reductions.

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

The gap yes predicate is exactly ordinary MCSP membership for a decoded instance.

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

Increasing the source threshold preserves the gap yes predicate.

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

Under a monotone relaxation map, increasing the source threshold can only shrink the no side.

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

Raising the relaxed threshold shrinks the no predicate.

theorem Complexity.GapMCSP.yesLanguage_eq_MCSP : yesLanguage = MCSP

The encoded gap yes language is definitionally the existing total MCSP language; only the no side introduces a promise.

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

Pointwise raising the relaxed threshold shrinks the encoded no language.

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

Widening makes the canonical yes and no languages disjoint.

def Complexity.GapMCSP.problem (parameters : Parameters) (hwidening : parameters.IsWidening) : PromiseProblem

Canonical Gap MCSP promise problem under a widening threshold map.

Equations

• Complexity.GapMCSP.problem parameters hwidening = { yesInstances := Complexity.GapMCSP.yesLanguage, noInstances := Complexity.GapMCSP.noLanguage parameters, disjoint := ⋯ }

theorem Complexity.GapMCSP.problem_mapReducesVia_id {source target : Parameters} (hrelax : target.RelaxesTo source) (hsource : source.IsWidening) (htarget : target.IsWidening) : (problem source hsource).MapReducesVia (problem target htarget) id

If the target uses a pointwise smaller relaxed threshold, identity is a side-preserving reduction: the yes side is unchanged and the target no side is larger.