Counter-family extension estimators -- proof internals

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.ApproximateCounterFamily.extensionEstimator_eq_of_length_lt_internal {overhead arity : ℕ} {beta : PositiveRationalScale} (family : ApproximateCounterFamily overhead beta arity) (target : BitString arity → Bool) (inputs : List (BitString arity)) (input : BitString arity) (hlength : inputs.length < requiredRoundCount beta arity) : family.extensionEstimator target inputs input = (family.counter ⟨inputs.length, hlength⟩).estimate (packTargetSamples target (input :: inputs).get)

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.ApproximateCounterFamily.isAccurateRequiredRoundEstimator_internal {overhead arity : ℕ} {beta : PositiveRationalScale} {family : ApproximateCounterFamily overhead beta arity} (hcorrect : family.IsCorrect) (target : BitString arity → Bool) : IsAccurateRequiredRoundEstimator beta target (family.extensionEstimator target)

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