Finite iteration of anti-checker selection rounds

This module exposes exact base and successor equations for the dependent composition of prefix-length counter-selection circuits.

@[simp]

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.eval_selectionPrefixCircuit_zero {overhead arity : ℕ} {beta : PositiveRationalScale} (family : ApproximateCounterFamily overhead beta arity) (hrounds : 0 ≤ requiredRoundCount beta arity) (table : BitString (2 ^ arity)) : (selectionPrefixCircuit family 0 hrounds).snd.eval table = selectionRoundInput table (emptyLabeledPrefix arity)

Zero selection rounds preserve the truth table and attach the empty labeled prefix.

@[simp]

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.size_selectionPrefixCircuit_zero {overhead arity : ℕ} {beta : PositiveRationalScale} (family : ApproximateCounterFamily overhead beta arity) (hrounds : 0 ≤ requiredRoundCount beta arity) : (selectionPrefixCircuit family 0 hrounds).snd.size = 2 ^ arity

The initial state-copy circuit has exactly one output gate per truth-table bit.

@[simp]

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.eval_selectionPrefixCircuit_succ {overhead arity rounds : ℕ} {beta : PositiveRationalScale} (family : ApproximateCounterFamily overhead beta arity) (hrounds : rounds + 1 ≤ requiredRoundCount beta arity) (table : BitString (2 ^ arity)) : (selectionPrefixCircuit family (rounds + 1) hrounds).snd.eval table = (selectionRoundStateCircuit (family.counter (selectionPrefixCounterIndex hrounds))).snd.eval ((selectionPrefixCircuit family rounds ⋯).snd.eval table)

A nonempty prefix circuit evaluates the previous prefix circuit and then the counter-selection round indexed by that prefix length.

@[simp]

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.size_selectionPrefixCircuit_succ {overhead arity rounds : ℕ} {beta : PositiveRationalScale} (family : ApproximateCounterFamily overhead beta arity) (hrounds : rounds + 1 ≤ requiredRoundCount beta arity) : (selectionPrefixCircuit family (rounds + 1) hrounds).snd.size = (selectionPrefixCircuit family rounds ⋯).snd.size + (selectionRoundStateCircuit (family.counter (selectionPrefixCounterIndex hrounds))).snd.size

Serial composition gives exact additive size at every successor round.

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.candidateLabeledSamples_truthTable_packTargetSamples {arity prefixLength : ℕ} (target : BitString arity → Bool) (inputs : Fin prefixLength → BitString arity) (input : BitString arity) : candidateLabeledSamples (MCSP.Instance.inputIndex input) (truthTable target) (packTargetSamples target inputs) = fun (sample : Fin (prefixLength + 1)) => SuccinctMCSP.Sample.ofFunction target (Fin.cons input inputs sample)

Prepending a candidate to a target-labeled packed vector agrees exactly with the candidate-prefix encoding used by the counter circuit.

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.selectionRoundSuccessorInput_truthTable_packTargetSamples {arity prefixLength : ℕ} (target : BitString arity → Bool) (inputs : Fin prefixLength → BitString arity) (candidate : Fin (2 ^ arity)) : selectionRoundSuccessorInput candidate (truthTable target) (packTargetSamples target inputs) = selectionTraceState target (Fin.cons (MCSP.Instance.inputOfIndex candidate) inputs)

On a canonical target truth table, the round successor state is precisely the state obtained by consing the selected input.

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.counterRoundEstimate_truthTable_packTargetSamples {overhead arity prefixLength : ℕ} {beta : PositiveRationalScale} (counter : ApproximateCounterCircuit overhead beta arity prefixLength) (target : BitString arity → Bool) (inputs : Fin prefixLength → BitString arity) (input : BitString arity) : counterRoundEstimate counter (truthTable target) (packTargetSamples target inputs) input = counter.estimate (packTargetSamples target (Fin.cons input inputs))

The circuit-level counter estimate on a canonical state is the counter's semantic estimate of the target-labeled cons extension.

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.counterRoundEstimate_eq_extensionEstimator {overhead arity rounds : ℕ} {beta : PositiveRationalScale} (family : ApproximateCounterFamily overhead beta arity) (target : BitString arity → Bool) (inputs : Fin rounds → BitString arity) (hrounds : rounds + 1 ≤ requiredRoundCount beta arity) : counterRoundEstimate (family.counter (selectionPrefixCounterIndex hrounds)) (truthTable target) (packTargetSamples target inputs) = family.extensionEstimator target (List.ofFn inputs)

At every bounded prefix, the circuit-level round estimate is exactly the existing total estimator induced by the counter family.

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.exists_eval_selectionPrefixCircuit_isEstimateSelectionTrace {overhead arity rounds : ℕ} {beta : PositiveRationalScale} (family : ApproximateCounterFamily overhead beta arity) (target : BitString arity → Bool) (hrounds : rounds ≤ requiredRoundCount beta arity) : ∃ (inputs : Fin rounds → BitString arity), (selectionPrefixCircuit family rounds hrounds).snd.eval (truthTable target) = selectionTraceState target inputs ∧ AntiChecker.IsEstimateSelectionTrace (family.extensionEstimator target) (List.ofFn inputs)

Every bounded prefix circuit realizes a sequence of genuine greedy estimate-minimizing choices for the counter family's induced estimator.

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.exists_eval_fullSelectionStateCircuit_isEstimateSelectionTrace {overhead arity : ℕ} {beta : PositiveRationalScale} (family : ApproximateCounterFamily overhead beta arity) (target : BitString arity → Bool) : ∃ (inputs : Fin (requiredRoundCount beta arity) → BitString arity), (fullSelectionStateCircuit family).snd.eval (truthTable target) = selectionTraceState target inputs ∧ AntiChecker.IsEstimateSelectionTrace (family.extensionEstimator target) (List.ofFn inputs)

The full state circuit realizes an estimate-selection trace of the exact length required by the anti-checker argument.

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.unpackSample_selectionTraceState_projection {arity rounds : ℕ} (target : BitString arity → Bool) (inputs : Fin rounds → BitString arity) (sample : Fin rounds) : unpackSample (selectionTraceState target inputs ∘ selectionSampleOutputMap arity rounds) sample = inputs sample

Projecting a canonical selection state to sample inputs recovers each selected input exactly.

@[simp]

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.eval_fullSelectionSamplesCircuit {overhead arity : ℕ} {beta : PositiveRationalScale} [NeZero arity] (family : ApproximateCounterFamily overhead beta arity) (table : BitString (2 ^ arity)) : (fullSelectionSamplesCircuit family).snd.eval table = (fullSelectionStateCircuit family).snd.eval table ∘ selectionSampleOutputMap arity (requiredRoundCount beta arity)

The projected circuit evaluates by selecting the sample-input coordinates from the full iterated state.

@[simp]

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.size_fullSelectionSamplesCircuit {overhead arity : ℕ} {beta : PositiveRationalScale} [NeZero arity] (family : ApproximateCounterFamily overhead beta arity) : (fullSelectionSamplesCircuit family).snd.size = (fullSelectionStateCircuit family).snd.size + requiredRoundCount beta arity * arity

Projecting away the labels and carried truth table costs exactly one output gate per required-round sample bit.

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.exists_eval_fullSelectionSamplesCircuit_isEstimateSelectionTrace {overhead arity : ℕ} {beta : PositiveRationalScale} [NeZero arity] (family : ApproximateCounterFamily overhead beta arity) (target : BitString arity → Bool) : ∃ (inputs : Fin (requiredRoundCount beta arity) → BitString arity), unpackSamples ((fullSelectionSamplesCircuit family).snd.eval (truthTable target)) = List.ofFn inputs ∧ AntiChecker.IsEstimateSelectionTrace (family.extensionEstimator target) (List.ofFn inputs)

The projected circuit prints exactly the inputs of a full greedy estimate-selection trace.