Anti-checker generator assembly -- proof internals #
theorem
Complexity.GapMCSP.Magnification.AntiCheckerLemma.eventually_exists_generatorOfCounterFamily_isCorrect_internal
(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
theorem
Complexity.GapMCSP.Magnification.AntiCheckerLemma.eventually_existsCorrectGeneratorAt_of_existsCorrectCounterFamilyAt_internal
(counterOverhead : ℕ)
(beta : PositiveRationalScale)
:
∀ᶠ (arity : ℕ) in Filter.atTop, ExistsCorrectCounterFamilyAt counterOverhead beta arity →
ExistsCorrectGeneratorAt (generatorOverheadFromCounter counterOverhead) beta arity