Documentation

Complexitylib.Metacomplexity.MCSP.Magnification.AntiChecker.Parameters

Anti-Checker Lemma parameters #

This module exposes the rounded finite parameters for the selected Oliveira--Pich--Santhanam Anti-Checker Lemma. It does not assert the lemma or the existence of its multi-output generator circuit.

source
@[simp]
theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.gapParameters_beta (beta : PositiveRationalScale) :
(gapParameters beta).beta = beta
source
@[simp]
theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.gapParameters_constant (beta : PositiveRationalScale) :
(gapParameters beta).constant = fixedConstant
source
theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.hardThreshold_eq_powFloor (beta : PositiveRationalScale) (arity : ℕ) :
hardThreshold beta arity = beta.powFloor arity

The hard-function threshold is the existing floor-rounded exponential.

source
theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.smallThreshold_eq_div (beta : PositiveRationalScale) (arity : ℕ) :
smallThreshold beta arity = beta.powFloor arity / (fixedConstant * arity)

The small-circuit threshold uses the published denominator 10*n.

source
theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.smallThreshold_le_hardThreshold (beta : PositiveRationalScale) (arity : ℕ) :
smallThreshold beta arity ≤ hardThreshold beta arity

The small-circuit threshold never exceeds the hard-function threshold.

source
theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.eventually_smallThreshold_pos (beta : PositiveRationalScale) :
∀ᶠ (arity : ℕ) in Filter.atTop, 0 < smallThreshold beta arity

The small-circuit threshold is positive at every sufficiently large arity.

source
theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.sampleCount_pos (beta : PositiveRationalScale) (arity : ℕ) :
0 < sampleCount beta arity

The floor-rounded sample count is always positive.

source
theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.sampleCount_mono (beta : PositiveRationalScale) :
Monotone (sampleCount beta)

The sample count is monotone in the truth-table arity.

source
theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.sampleCount_le_upper (beta : PositiveRationalScale) (arity : ℕ) :
sampleCount beta arity ≤ sampleCountUpper beta arity

Floor rounding gives no more samples than ceiling rounding.

source
theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.sampleCountUpper_le_two_mul (beta : PositiveRationalScale) (arity : ℕ) :
sampleCountUpper beta arity ≤ 2 * sampleCount beta arity

Ceiling rounding increases the sample count by at most a factor of two.

source
theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.outputBitCount_pos (beta : PositiveRationalScale) (arity : ℕ) [NeZero arity] :
0 < outputBitCount beta arity

At positive arity, the generator's packed output width is positive.

source
theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.generatorSizeBound_eq_pow (overhead : ℕ) (beta : PositiveRationalScale) (arity : ℕ) :
generatorSizeBound overhead beta arity = 2 ^ (arity + beta.ceilMul (overhead * arity))

The generator bound is the ceiling-rounded natural version of 2^(n + k*beta*n).

source
theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.truthTableLength_le_generatorSizeBound (overhead : ℕ) (beta : PositiveRationalScale) (arity : ℕ) :
2 ^ arity ≤ generatorSizeBound overhead beta arity

The rounded generator bound is at least its truth-table input length.