Gap MCSP -- definitions

A canonical MCSP instance already contains a source threshold s. Gap MCSP keeps the yes side minimumSize ≤ s and parameterizes the no side by an explicit relaxed threshold sigma(arity, s). This retains both scales needed by hardness magnification instead of collapsing the promise to an ordinary language.

structure Complexity.GapMCSP.Parameters : Type

Quantitative relaxation of an MCSP source threshold.

• relaxedThreshold : ℕ → ℕ → ℕ

  No-instances must have minimum size strictly above this threshold.

def Complexity.GapMCSP.Parameters.IsWidening (parameters : Parameters) : Prop

The target threshold is never smaller than the source threshold. This is exactly what makes the two promised sides disjoint.

Equations

• parameters.IsWidening = ∀ (arity threshold : ℕ), threshold ≤ parameters.relaxedThreshold arity threshold

def Complexity.GapMCSP.Parameters.ThresholdMonotone (parameters : Parameters) : Prop

Increasing the source threshold cannot decrease its relaxed image.

Equations

• parameters.ThresholdMonotone = ∀ (arity : ℕ), Monotone (parameters.relaxedThreshold arity)

def Complexity.GapMCSP.Parameters.RelaxesTo (first second : Parameters) : Prop

Pointwise order on relaxed-threshold maps.

Equations

• first.RelaxesTo second = ∀ (arity threshold : ℕ), first.relaxedThreshold arity threshold ≤ second.relaxedThreshold arity threshold

def Complexity.GapMCSP.IsYes (inst : MCSP.Instance) : Prop

Promised yes condition at the source threshold stored in the instance.

Equations

• Complexity.GapMCSP.IsYes inst = (inst.minimumSize ≤ inst.threshold)

def Complexity.GapMCSP.IsNo (parameters : Parameters) (inst : MCSP.Instance) : Prop

Promised no condition above the relaxed target threshold.

Equations

• Complexity.GapMCSP.IsNo parameters inst = (parameters.relaxedThreshold inst.arity inst.threshold < inst.minimumSize)

def Complexity.GapMCSP.yesLanguage : Language

Canonically encoded yes language. Malformed MCSP encodings lie outside the promise rather than being assigned to the no side.

Equations

• Complexity.GapMCSP.yesLanguage = {bits : List Bool | match Complexity.MCSP.Instance.decode? bits with | some inst => Complexity.GapMCSP.IsYes inst | none => False}

def Complexity.GapMCSP.noLanguage (parameters : Parameters) : Language

Canonically encoded no language for a chosen threshold relaxation.

Equations

• Complexity.GapMCSP.noLanguage parameters = {bits : List Bool | match Complexity.MCSP.Instance.decode? bits with | some inst => Complexity.GapMCSP.IsNo parameters inst | none => False}