Iterable anti-checker selection rounds

This module exposes one state-preserving circuit round suitable for sequential composition across the finite approximate-counter family.

@[simp]

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.eval_selectionRoundCombinedCircuit {overhead arity prefixLength : ℕ} {beta : PositiveRationalScale} (counter : ApproximateCounterCircuit overhead beta arity prefixLength) (table : BitString (2 ^ arity)) (packedPrefix : BitString (prefixLength * (arity + 1))) : (selectionRoundCombinedCircuit counter).snd.eval (selectionRoundInput table packedPrefix) = Fin.append (selectionRoundInput table packedPrefix) ((minimumCounterRecordCircuit counter).snd.eval (selectionRoundInput table packedPrefix))

A round's combined circuit preserves the complete state before appending the exhaustive minimum record.

@[simp]

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.size_selectionRoundCombinedCircuit {overhead arity prefixLength : ℕ} {beta : PositiveRationalScale} (counter : ApproximateCounterCircuit overhead beta arity prefixLength) : (selectionRoundCombinedCircuit counter).snd.size = selectionRoundInputWidth arity prefixLength + (minimumCounterRecordCircuit counter).snd.size

Exact cost of preserving the state beside exhaustive minimization.

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.exists_eval_selectionRoundStateCircuit_eq_successor {overhead arity prefixLength : ℕ} {beta : PositiveRationalScale} (counter : ApproximateCounterCircuit overhead beta arity prefixLength) (table : BitString (2 ^ arity)) (packedPrefix : BitString (prefixLength * (arity + 1))) : ∃ (candidate : Fin (2 ^ arity)), (selectionRoundStateCircuit counter).snd.eval (selectionRoundInput table packedPrefix) = selectionRoundSuccessorInput candidate table packedPrefix ∧ AntiChecker.IsEstimateMinimizer (counterRoundEstimate counter table packedPrefix) (MCSP.Instance.inputOfIndex candidate)

One round preserves the table, prepends a genuine labeled candidate, and that candidate globally minimizes the counter estimate.

@[simp]

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.size_selectionRoundStateCircuit {overhead arity prefixLength : ℕ} {beta : PositiveRationalScale} (counter : ApproximateCounterCircuit overhead beta arity prefixLength) : (selectionRoundStateCircuit counter).snd.size = selectionRoundInputWidth arity prefixLength + (minimumCounterRecordCircuit counter).snd.size + selectionRoundInputWidth arity (prefixLength + 1)

Exact round-state cost: preserved input state, exhaustive minimization, and the projected successor state.