Conditional anti-checker counter circuits

This module exposes the exact bounded circuit-family contract used by the Anti-Checker Lemma construction. HasApproximateCounterFamilies is only the conditional conclusion to be obtained from a future NP ⊆ P/poly bridge; no such implication is asserted here.

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.counterOutputWidth_pos (beta : PositiveRationalScale) (arity : ℕ) : 0 < counterOutputWidth beta arity

Counter output width is always positive.

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.counterSizeBound_pos (overhead : ℕ) (beta : PositiveRationalScale) (arity : ℕ) : 0 < counterSizeBound overhead beta arity

The conditional counter size bound is always positive.

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.ApproximateCounterCircuit.estimate_lt_two_pow {overhead arity prefixLength : ℕ} {beta : PositiveRationalScale} (counter : ApproximateCounterCircuit overhead beta arity prefixLength) (input : BitString ((prefixLength + 1) * (arity + 1))) : counter.estimate input < 2 ^ counterOutputWidth beta arity

Every fixed-width counter output denotes a value below its width bound.

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.ApproximateCounterCircuit.outputWidth_le_sizeBound {overhead arity prefixLength : ℕ} {beta : PositiveRationalScale} (counter : ApproximateCounterCircuit overhead beta arity prefixLength) : counterOutputWidth beta arity ≤ counterSizeBound overhead beta arity

Merely printing the count bits forces the output width below the stated counter size bound.

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.ApproximateCounterCircuit.approximates {overhead arity prefixLength : ℕ} {beta : PositiveRationalScale} {counter : ApproximateCounterCircuit overhead beta arity prefixLength} (hcorrect : counter.IsCorrect) (input : BitString ((prefixLength + 1) * (arity + 1))) : AntiChecker.IsRelativeApproximation (roundPrecision arity) (candidateLabeledSurvivorCount arity (smallThreshold beta arity) (unpackLabeledSamples input)) (counter.estimate input)

Pointwise form of a counter circuit's correctness contract.

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.ApproximateCounterFamily.counter_isCorrect {overhead arity : ℕ} {beta : PositiveRationalScale} {family : ApproximateCounterFamily overhead beta arity} (hcorrect : family.IsCorrect) (prefixLength : Fin (requiredRoundCount beta arity)) : (family.counter prefixLength).IsCorrect

Correctness of a family specializes to every indexed prefix length.