Anti-Checker good-string parameter bridge -- proof internals

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.eventually_survivorTupleMajoritySizeBound_le_hardThreshold_internal (beta : PositiveRationalScale) : ∀ᶠ (arity : ℕ) in Filter.atTop, AntiChecker.survivorTupleMajoritySizeBound arity (smallThreshold beta arity) ≤ hardThreshold beta arity

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.eventually_hasShrinkExtension_of_isHardAt_internal (beta : PositiveRationalScale) : ∀ᶠ (arity : ℕ) in Filter.atTop, ∀ (target : BitString arity → Bool) (inputs : List (BitString arity)), IsHardAt beta target → AntiChecker.HasShrinkExtension (2 * arity) target (smallThreshold beta arity) inputs