Circuit-level anti-checker selection rounds

This module exposes the exact semantics and size of the fixed-candidate record circuit used by exhaustive approximate-counter minimization.

@[simp]

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.eval_candidateCounterInputCircuit {arity prefixLength : ℕ} (candidate : Fin (2 ^ arity)) (table : BitString (2 ^ arity)) (packedPrefix : BitString (prefixLength * (arity + 1))) : (candidateCounterInputCircuit arity prefixLength candidate).eval (selectionRoundInput table packedPrefix) = packLabeledSamples (candidateLabeledSamples candidate table packedPrefix)

A fixed-candidate counter input is exactly the row-major encoding of that candidate prepended to the carried labeled prefix.

@[simp]

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.eval_candidateSampleCircuit {arity prefixLength : ℕ} (candidate : Fin (2 ^ arity)) (table : BitString (2 ^ arity)) (packedPrefix : BitString (prefixLength * (arity + 1))) : (candidateSampleCircuit arity prefixLength candidate).eval (selectionRoundInput table packedPrefix) = candidateSampleBits candidate table

A fixed-candidate payload contains its input bits followed by the live truth-table label.

@[simp]

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.eval_candidateCounterRecordCircuit {overhead arity prefixLength : ℕ} {beta : PositiveRationalScale} (counter : ApproximateCounterCircuit overhead beta arity prefixLength) (candidate : Fin (2 ^ arity)) (table : BitString (2 ^ arity)) (packedPrefix : BitString (prefixLength * (arity + 1))) : (candidateCounterRecordCircuit counter candidate).snd.eval (selectionRoundInput table packedPrefix) = Fin.append (counter.circuit.eval (packLabeledSamples (candidateLabeledSamples candidate table packedPrefix))) (candidateSampleBits candidate table)

A fixed-candidate record emits the counter bits as its key and the labeled candidate as its payload.

@[simp]

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.size_candidateCounterRecordCircuit {overhead arity prefixLength : ℕ} {beta : PositiveRationalScale} (counter : ApproximateCounterCircuit overhead beta arity prefixLength) (candidate : Fin (2 ^ arity)) : (candidateCounterRecordCircuit counter candidate).snd.size = counter.circuit.size + (prefixLength + 1) * (arity + 1) + (arity + 1)

Exact cost of one fixed-candidate record: the supplied counter plus the materialized counter input and labeled payload.

@[simp]

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.selectionCandidateCount_add_one (arity : ℕ) : selectionCandidateCount arity + 1 = 2 ^ arity

The recursive tournament contains exactly one record for every truth-table input.

@[simp]

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.eval_packedCandidateCounterRecords {overhead arity prefixLength : ℕ} {beta : PositiveRationalScale} (counter : ApproximateCounterCircuit overhead beta arity prefixLength) (table : BitString (2 ^ arity)) (packedPrefix : BitString (prefixLength * (arity + 1))) : (packedCandidateCounterRecords counter).snd.eval (selectionRoundInput table packedPrefix) = BitString.packKeyedRecords (selectionCandidateCount arity) (candidateCounterKeys counter table packedPrefix) (candidateCounterPayloads table)

Parallel candidate evaluation produces the exact recursive record layout expected by the minimum tournament.

@[simp]

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.size_packedCandidateCounterRecords {overhead arity prefixLength : ℕ} {beta : PositiveRationalScale} (counter : ApproximateCounterCircuit overhead beta arity prefixLength) : (packedCandidateCounterRecords counter).snd.size = (selectionCandidateCount arity + 1) * (counter.circuit.size + (prefixLength + 1) * (arity + 1) + (arity + 1))

Exact parallel-evaluation cost: one fixed-candidate record circuit for each truth-table input.

@[simp]

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

Exhaustive selection evaluates to the semantic minimum counter record.

@[simp]

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.size_minimumCounterRecordCircuit {overhead arity prefixLength : ℕ} {beta : PositiveRationalScale} (counter : ApproximateCounterCircuit overhead beta arity prefixLength) : (minimumCounterRecordCircuit counter).snd.size = (selectionCandidateCount arity + 1) * (counter.circuit.size + (prefixLength + 1) * (arity + 1) + (arity + 1)) + ((selectionCandidateCount arity + 1) * (counterOutputWidth beta arity + (arity + 1)) + selectionCandidateCount arity * (20 * counterOutputWidth beta arity + 5 * (arity + 1) + 1))

Exact exhaustive-selector cost, separating parallel candidate evaluation from the sequential keyed-minimum tournament.

@[simp]

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.candidateSampleBits_input {arity : ℕ} (candidate : Fin (2 ^ arity)) (table : BitString (2 ^ arity)) (coordinate : Fin arity) : candidateSampleBits candidate table coordinate.castSucc = MCSP.Instance.inputOfIndex candidate coordinate

The first arity payload bits are the selected candidate input.

@[simp]

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.candidateSampleBits_output {arity : ℕ} (candidate : Fin (2 ^ arity)) (table : BitString (2 ^ arity)) : candidateSampleBits candidate table (Fin.last arity) = table candidate

The final payload bit is the selected candidate's truth-table label.

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.exists_minimumCounterRecord_eq_candidate {overhead arity prefixLength : ℕ} {beta : PositiveRationalScale} (counter : ApproximateCounterCircuit overhead beta arity prefixLength) (table : BitString (2 ^ arity)) (packedPrefix : BitString (prefixLength * (arity + 1))) : ∃ (candidate : Fin (2 ^ arity)), minimumCounterRecord counter table packedPrefix = (candidateCounterKey counter candidate table packedPrefix, candidateSampleBits candidate table)

The semantic tournament winner is one of the canonical candidate records.

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.minimumCounterRecord_key_le_candidate {overhead arity prefixLength : ℕ} {beta : PositiveRationalScale} (counter : ApproximateCounterCircuit overhead beta arity prefixLength) (table : BitString (2 ^ arity)) (packedPrefix : BitString (prefixLength * (arity + 1))) (candidate : Fin (2 ^ arity)) : (minimumCounterRecord counter table packedPrefix).1.unsignedValue ≤ (candidateCounterKey counter candidate table packedPrefix).unsignedValue

The winning counter key is no larger than the key of any candidate.

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.exists_minimumCounterRecord_candidate_isEstimateMinimizer {overhead arity prefixLength : ℕ} {beta : PositiveRationalScale} (counter : ApproximateCounterCircuit overhead beta arity prefixLength) (table : BitString (2 ^ arity)) (packedPrefix : BitString (prefixLength * (arity + 1))) : ∃ (candidate : Fin (2 ^ arity)), minimumCounterRecord counter table packedPrefix = (candidateCounterKey counter candidate table packedPrefix, candidateSampleBits candidate table) ∧ AntiChecker.IsEstimateMinimizer (counterRoundEstimate counter table packedPrefix) (MCSP.Instance.inputOfIndex candidate)

The winning record carries a canonical input minimizing the counter's natural extension estimate.

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

Circuit evaluation emits a genuine candidate record whose input globally minimizes the natural counter estimate.