Anti-Checker Lemma round parameters -- proof internals

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

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

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

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

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

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

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