Randomized anti-checker counters

This module exposes the exact derandomization step for the anti-checker counter interface. A randomized multi-output counter with sufficiently small pointwise failure probability yields a deterministic correct counter of identical size by selecting and hardwiring one seed.

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.RandomizedApproximateCounterCircuit.exists_correct_counter {overhead arity prefixLength seedWidth : ℕ} {beta : PositiveRationalScale} (randomized : RandomizedApproximateCounterCircuit overhead beta arity prefixLength seedWidth) (hcorrect : randomized.IsCorrect) : ∃ (counter : ApproximateCounterCircuit overhead beta arity prefixLength), counter.IsCorrect ∧ counter.circuit.size = randomized.circuit.size

A randomized counter satisfying the strict pointwise failure bound yields a deterministic counter accurate on every fixed-width input. The construction preserves exact circuit size.