Anti-Checker Lemma round parameters

At every sufficiently large arity, target hardness and a semantic extension estimator accurate through the required finite prefix range generate an anti-checker. This is the combinatorial round-composition contract; constructing a small circuit that realizes the estimator is a separate conditional step.

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.IsAccurateRoundEstimator.isAccurateRequiredRoundEstimator {arity : ℕ} {beta : PositiveRationalScale} {target : BitString arity → Bool} {estimator : List (BitString arity) → BitString arity → ℕ} (hestimate : IsAccurateRoundEstimator beta target estimator) : IsAccurateRequiredRoundEstimator beta target estimator

Global round-estimator accuracy implies the bounded accuracy contract used by the anti-checker construction.

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.initialCandidateSurvivorCount_lt_two_pow_roundBlockCount {arity : ℕ} (beta : PositiveRationalScale) (target : BitString arity → Bool) : AntiChecker.candidateSurvivorCount target (smallThreshold beta arity) [] < 2 ^ roundBlockCount beta arity

The initial canonical survivor count is strictly below the power of two indexed by the selected number of halving blocks.

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.eventually_requiredRoundCount_le_sampleCount (beta : PositiveRationalScale) : ∀ᶠ (arity : ℕ) in Filter.atTop, requiredRoundCount beta arity ≤ sampleCount beta arity

The published sample count eventually covers every shrinking round needed by the canonical circuit-code cardinality bound.

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.eventually_exists_shrinkTrace_of_isHardAt (beta : PositiveRationalScale) : ∀ᶠ (arity : ℕ) in Filter.atTop, ∀ (target : BitString arity → Bool) (estimator : List (BitString arity) → BitString arity → ℕ), IsHardAt beta target → IsAccurateRoundEstimator beta target estimator → ∀ (rounds : ℕ), ∃ (inputs : List (BitString arity)), inputs.length = rounds ∧ AntiChecker.IsShrinkTrace (roundShrinkDenominator arity) target (smallThreshold beta arity) inputs

For every sufficiently large arity, any accurate round estimator produces a 1/(4n) shrink trace of any requested length for every hard target.

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.eventually_exists_requiredShrinkTrace_of_isHardAt (beta : PositiveRationalScale) : ∀ᶠ (arity : ℕ) in Filter.atTop, ∀ (target : BitString arity → Bool) (estimator : List (BitString arity) → BitString arity → ℕ), IsHardAt beta target → IsAccurateRequiredRoundEstimator beta target estimator → ∃ (inputs : List (BitString arity)), inputs.length = requiredRoundCount beta arity ∧ AntiChecker.IsShrinkTrace (roundShrinkDenominator arity) target (smallThreshold beta arity) inputs

For every sufficiently large arity, accuracy only through the required number of rounds produces the shrink trace used by the construction.

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.eventually_padInputsTo_isFor_of_isEstimateSelectionTrace (beta : PositiveRationalScale) : ∀ᶠ (arity : ℕ) in Filter.atTop, ∀ (harity : arity ≠ 0) (target : BitString arity → Bool) (estimator : List (BitString arity) → BitString arity → ℕ) (inputs : List (BitString arity)), IsHardAt beta target → IsAccurateRequiredRoundEstimator beta target estimator → inputs.length = requiredRoundCount beta arity → AntiChecker.IsEstimateSelectionTrace estimator inputs → (AntiChecker.padInputsTo (sampleCount beta arity) inputs).length = sampleCount beta arity ∧ AntiChecker.IsFor target (smallThreshold beta arity) (AntiChecker.padInputsTo (sampleCount beta arity) inputs)

For every sufficiently large positive arity, any required-length greedy estimate-selection trace from an accurate estimator becomes an anti-checker after canonical zero padding to the published sample count.

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.eventually_exists_isFor_length_eq_sampleCount_of_isHardAt (beta : PositiveRationalScale) : ∀ᶠ (arity : ℕ) in Filter.atTop, ∀ (harity : arity ≠ 0) (target : BitString arity → Bool) (estimator : List (BitString arity) → BitString arity → ℕ), IsHardAt beta target → IsAccurateRequiredRoundEstimator beta target estimator → ∃ (inputs : List (BitString arity)), inputs.length = sampleCount beta arity ∧ AntiChecker.IsFor target (smallThreshold beta arity) inputs

For every sufficiently large arity, estimator accuracy through only the required rounds yields an anti-checker of exactly the published sample count for every hard target.