Anti-checker generator output padding

This module exposes the exact semantics and size of the circuit that prepends zero sample rows to the selected inputs. The padded circuit therefore prints the canonical AntiChecker.padInputsTo list at the published sample count.

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.unpackSample_padPackedSamples {sourceCount targetCount arity : ℕ} (hbudget : sourceCount ≤ targetCount) (input : BitString (sourceCount * arity)) (sample : Fin targetCount) : unpackSample (padPackedSamples hbudget input) sample = Fin.append (fun (x : Fin (targetCount - sourceCount)) (x_1 : Fin arity) => false) (unpackSample input) (Fin.cast ⋯ sample)

Unpacking one row after packed zero padding gives the corresponding row of the appended zero-and-source tuple.

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.unpackSamples_padPackedSamples {sourceCount targetCount arity : ℕ} (hbudget : sourceCount ≤ targetCount) (input : BitString (sourceCount * arity)) : unpackSamples (padPackedSamples hbudget input) = AntiChecker.padInputsTo targetCount (unpackSamples input)

Unpacking every row after packed zero padding agrees exactly with the canonical list-level padding operation.

@[simp]

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.eval_packedSamplePaddingCircuit {sourceCount targetCount arity : ℕ} [NeZero (sourceCount * arity)] [NeZero (targetCount * arity)] (hbudget : sourceCount ≤ targetCount) (input : BitString (sourceCount * arity)) : (packedSamplePaddingCircuit hbudget).eval input = padPackedSamples hbudget input

The zero-internal-gate padding circuit computes packed zero padding exactly.

@[simp]

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.size_packedSamplePaddingCircuit {sourceCount targetCount arity : ℕ} [NeZero (sourceCount * arity)] [NeZero (targetCount * arity)] (hbudget : sourceCount ≤ targetCount) : (packedSamplePaddingCircuit hbudget).size = targetCount * arity

Packed padding costs exactly one output gate per target output bit and no internal gates.

@[simp]

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.eval_paddedSelectionCircuit {overhead arity : ℕ} {beta : PositiveRationalScale} [NeZero arity] (family : ApproximateCounterFamily overhead beta arity) (hbudget : requiredRoundCount beta arity ≤ sampleCount beta arity) (table : BitString (2 ^ arity)) : (paddedSelectionCircuit family hbudget).snd.eval table = padPackedSamples hbudget ((fullSelectionSamplesCircuit family).snd.eval table)

The padded selection circuit first computes the required-round samples and then prepends their packed zero rows.

@[simp]

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.size_paddedSelectionCircuit {overhead arity : ℕ} {beta : PositiveRationalScale} [NeZero arity] (family : ApproximateCounterFamily overhead beta arity) (hbudget : requiredRoundCount beta arity ≤ sampleCount beta arity) : (paddedSelectionCircuit family hbudget).snd.size = (fullSelectionSamplesCircuit family).snd.size + outputBitCount beta arity

Padding adds exactly the published output width to the unpadded selection circuit's size.

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

On a target truth table, the padded circuit prints the canonical padding of a full greedy estimate-selection trace.

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.eventually_eval_paddedSelectionCircuit_isFor_of_correctCounterFamily (beta : PositiveRationalScale) : ∀ᶠ (arity : ℕ) in Filter.atTop, ∀ (harity : arity ≠ 0) (overhead : ℕ) (family : ApproximateCounterFamily overhead beta arity) (hbudget : requiredRoundCount beta arity ≤ sampleCount beta arity), family.IsCorrect → ∀ (target : BitString arity → Bool), IsHardAt beta target → AntiChecker.IsFor target (smallThreshold beta arity) (unpackSamples ((paddedSelectionCircuit family hbudget).snd.eval (truthTable target)))

For every sufficiently large positive arity, correctness of the finite counter family makes the padded circuit output an anti-checker for every hard target. This certifies the circuit's computed output, rather than merely the existence of a suitable list.