GapMCSP hardness-magnification parameters -- definitions

This module instantiates the finite parameters from Oliveira--Pich--Santhanam's GapMCSP magnification theorem. For a positive rational beta and positive constant c, the yes threshold is

2^floor(beta*n) / (c*n)

and the no threshold is 2^floor(beta*n). A separate positive rational epsilon gives the rounded natural size bound corresponding to N^(1+epsilon) on raw input length N = 2^n.

structure Complexity.GapMCSP.Magnification.Parameters : Type

Finite GapMCSP thresholds corresponding to the published magnification frontier.

• beta : PositiveRationalScale

  Positive rational exponent beta.

• constant : ℕ

  Universal denominator constant c.

• constant_pos : 0 < self.constant

  The constant is at least one.

def Complexity.GapMCSP.Magnification.Parameters.yesThreshold (parameters : Parameters) (arity : ℕ) : ℕ

Small-circuit cutoff 2^floor(beta*n)/(c*n).

Equations

• parameters.yesThreshold arity = parameters.beta.powFloor arity / (parameters.constant * arity)

def Complexity.GapMCSP.Magnification.Parameters.noThreshold (parameters : Parameters) (arity : ℕ) : ℕ

Large-circuit cutoff 2^floor(beta*n).

Equations

• parameters.noThreshold arity = parameters.beta.powFloor arity

def Complexity.GapMCSP.Magnification.Parameters.sliceParameters (parameters : Parameters) : SliceParameters

The arity-indexed raw GapMCSP slice at the selected finite parameters.

Equations

• parameters.sliceParameters = { yesThreshold := parameters.yesThreshold, noThreshold := parameters.noThreshold }

def Complexity.GapMCSP.Magnification.circuitBound (epsilon : PositiveRationalScale) : ℕ → ℕ

Rounded natural circuit bound corresponding to N^(1+epsilon).

Equations

• Complexity.GapMCSP.Magnification.circuitBound epsilon = epsilon.onePlusCeilPowAtLength

def Complexity.GapMCSP.Magnification.circuitBoundAtArity (epsilon : PositiveRationalScale) (arity : ℕ) : ℕ

The same circuit bound written at raw truth-table arity n.

Equations

• Complexity.GapMCSP.Magnification.circuitBoundAtArity epsilon arity = epsilon.onePlusCeilPow arity