Anti-Checker good-string parameter bridge

The generic good-string argument packs one small circuit for each tuple entry and composes their outputs with strict majority. This module verifies that its explicit size bound fits the Anti-Checker Lemma's hard-function threshold at all sufficiently large arities.

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

The packed survivor-tuple majority circuit fits the hard-function threshold at every sufficiently large arity.

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.eventually_hasShrinkExtension_of_isHardAt (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

At every sufficiently large arity, hardness at the Anti-Checker Lemma's threshold guarantees a one-input 1/(2n) survivor shrink from any prefix.