Documentation

Complexitylib.Metacomplexity.MCSP.Magnification.AntiChecker.Generator.Assembly

Anti-checker generator assembly #

This module packages the padded selector into the public generator interface. It proves the complete conditional construction: correct approximate-counter families yield correct size-bounded anti-checker generators with overhead k + 32.

source
theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.eventually_exists_generatorOfCounterFamily_isCorrect (counterOverhead : ℕ) (beta : PositiveRationalScale) :
∀ᶠ (arity : ℕ) in Filter.atTop, ∀ (harity : arity ≠ 0) (family : ApproximateCounterFamily counterOverhead beta arity), family.IsCorrect → ∃ (generator : Generator (generatorOverheadFromCounter counterOverhead) beta arity), generator.IsCorrect

At every sufficiently large positive arity, each correct counter family packages as a correct generator with the lifted overhead.

source
theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.eventually_existsCorrectGeneratorAt_of_existsCorrectCounterFamilyAt (counterOverhead : ℕ) (beta : PositiveRationalScale) :
∀ᶠ (arity : ℕ) in Filter.atTop, ExistsCorrectCounterFamilyAt counterOverhead beta arity → ExistsCorrectGeneratorAt (generatorOverheadFromCounter counterOverhead) beta arity

Eventually, existence of a correct counter family at one arity implies existence of a correct generator at that arity.

source
theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.hasGenerators_of_hasApproximateCounterFamilies :
HasApproximateCounterFamilies → HasGenerators

The conditional approximate-counter conclusion implies the complete Anti-Checker Lemma generator conclusion. No complexity-class containment is used in this circuit-assembly implication.