Anti-Checker Lemma parameters -- definitions

This layer fixes natural-number versions of the four scales in Oliveira--Pich-- Santhanam's Anti-Checker Lemma: the hard-function threshold, the smaller circuit threshold met by the generated samples, the number of samples, and the size of the multi-output generator circuit.

Thresholds and sample counts round exponents down. The generator's upper size bound rounds its overhead exponent up, so it does not understate the published upper bound. The two choices differ by at most a factor of two through the general PositiveRationalScale API.

def Complexity.GapMCSP.Magnification.AntiCheckerLemma.fixedConstant : ℕ

The explicit constant 10 used by the published Anti-Checker Lemma.

Equations

• Complexity.GapMCSP.Magnification.AntiCheckerLemma.fixedConstant = 10

def Complexity.GapMCSP.Magnification.AntiCheckerLemma.gapParameters (beta : PositiveRationalScale) : Parameters

GapMCSP parameters at exponent beta and the Anti-Checker Lemma's fixed denominator constant.

Equations

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

def Complexity.GapMCSP.Magnification.AntiCheckerLemma.hardThreshold (beta : PositiveRationalScale) (arity : ℕ) : ℕ

Hard-function cutoff 2^floor(beta*n).

Equations

• Complexity.GapMCSP.Magnification.AntiCheckerLemma.hardThreshold beta arity = (Complexity.GapMCSP.Magnification.AntiCheckerLemma.gapParameters beta).noThreshold arity

def Complexity.GapMCSP.Magnification.AntiCheckerLemma.smallThreshold (beta : PositiveRationalScale) (arity : ℕ) : ℕ

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

Equations

• Complexity.GapMCSP.Magnification.AntiCheckerLemma.smallThreshold beta arity = (Complexity.GapMCSP.Magnification.AntiCheckerLemma.gapParameters beta).yesThreshold arity

def Complexity.GapMCSP.Magnification.AntiCheckerLemma.sampleCount (beta : PositiveRationalScale) (arity : ℕ) : ℕ

Floor-rounded sample count 2^floor(10*beta*n).

Equations

• Complexity.GapMCSP.Magnification.AntiCheckerLemma.sampleCount beta arity = beta.powFloor (Complexity.GapMCSP.Magnification.AntiCheckerLemma.fixedConstant * arity)

def Complexity.GapMCSP.Magnification.AntiCheckerLemma.sampleCountUpper (beta : PositiveRationalScale) (arity : ℕ) : ℕ

Ceiling-rounded companion to sampleCount, used to expose rounding slack.

Equations

• Complexity.GapMCSP.Magnification.AntiCheckerLemma.sampleCountUpper beta arity = beta.powCeil (Complexity.GapMCSP.Magnification.AntiCheckerLemma.fixedConstant * arity)

def Complexity.GapMCSP.Magnification.AntiCheckerLemma.outputBitCount (beta : PositiveRationalScale) (arity : ℕ) : ℕ

Number of output bits needed to print all fixed-width sample inputs.

Equations

• Complexity.GapMCSP.Magnification.AntiCheckerLemma.outputBitCount beta arity = Complexity.GapMCSP.Magnification.AntiCheckerLemma.sampleCount beta arity * arity

def Complexity.GapMCSP.Magnification.AntiCheckerLemma.generatorSizeBound (overhead : ℕ) (beta : PositiveRationalScale) (arity : ℕ) : ℕ

Ceiling-rounded generator size 2^n * 2^ceil(k*beta*n).

Equations

• Complexity.GapMCSP.Magnification.AntiCheckerLemma.generatorSizeBound overhead beta arity = 2 ^ arity * beta.powCeil (overhead * arity)

instance Complexity.GapMCSP.Magnification.AntiCheckerLemma.instNeZeroNatSampleCount (beta : PositiveRationalScale) (arity : ℕ) : NeZero (sampleCount beta arity)

instance Complexity.GapMCSP.Magnification.AntiCheckerLemma.instNeZeroNatOutputBitCount (beta : PositiveRationalScale) (arity : ℕ) [NeZero arity] : NeZero (outputBitCount beta arity)