Counter-family extension estimators

This module connects a correct finite counter family to the exact bounded semantic estimator contract used by anti-checker round composition.

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.ApproximateCounterFamily.extensionEstimator_eq_of_length_lt {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)

Inside the required prefix range, the total estimator evaluates the counter indexed by the current prefix length.

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

Correctness of every finite counter turns the induced total estimator into the bounded accuracy contract required by round composition.

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

At every sufficiently large nonzero arity, a correct conditional counter family yields an exact-length anti-checker for every hard target.