Arity-indexed Gap MCSP slices -- definitions

These are the explicit GapMCSP[s_yes, s_no] promise problems used in hardness-magnification statements. Both thresholds are functions of the represented Boolean-function arity. The input remains a canonical full MCSP code, with its threshold field forced to s_yes.

structure Complexity.GapMCSP.SliceParameters : Type

The two arity-indexed thresholds of a Gap MCSP slice.

• yesThreshold : ℕ → ℕ

  Circuit-size threshold on the yes side.

• noThreshold : ℕ → ℕ

  Strict circuit-size threshold on the no side.

def Complexity.GapMCSP.SliceParameters.IsGap (parameters : SliceParameters) : Prop

The no threshold is at least the yes threshold at every arity.

Equations

• parameters.IsGap = ∀ (arity : ℕ), parameters.yesThreshold arity ≤ parameters.noThreshold arity

def Complexity.GapMCSP.SliceParameters.ReducesTo (source target : SliceParameters) : Prop

Exact parameter order supporting table-preserving rethreshold reductions. The target accepts at least as many small functions and rejects at least as many large functions as the source.

Equations

• source.ReducesTo target = ((∀ (arity : ℕ), source.yesThreshold arity ≤ target.yesThreshold arity) ∧ ∀ (arity : ℕ), target.noThreshold arity ≤ source.noThreshold arity)

def Complexity.GapMCSP.sliceYesLanguage (parameters : SliceParameters) : Language

Yes side of GapMCSP[s_yes, s_no].

Equations

• Complexity.GapMCSP.sliceYesLanguage parameters = Complexity.MCSP.atThreshold parameters.yesThreshold

def Complexity.GapMCSP.sliceNoLanguage (parameters : SliceParameters) : Language

No side of GapMCSP[s_yes, s_no]. The encoded threshold is forced to the yes threshold; the second parameter only determines the semantic no cutoff.

Equations

• One or more equations did not get rendered due to their size.