Anti-Checker Lemma parameters -- proof internals

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.gapParameters_beta_internal (beta : PositiveRationalScale) : (gapParameters beta).beta = beta

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.gapParameters_constant_internal (beta : PositiveRationalScale) : (gapParameters beta).constant = fixedConstant

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.hardThreshold_eq_powFloor_internal (beta : PositiveRationalScale) (arity : ℕ) : hardThreshold beta arity = beta.powFloor arity

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

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

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

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

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

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

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

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

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

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