Randomized anti-checker counters -- proof internals

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.RandomizedApproximateCounterCircuit.exists_correct_counter_internal {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