Anti-checker generator size bounds

This module accounts for the complete exhaustive selector, its dependent round composition, and its final output padding. It converts a counter-family overhead k into the explicit generator overhead k + 32; the added exponent absorbs three sample-count factors and two rounds of fixed polynomial slack.

@[simp]

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.generatorOverheadSlack_eq : generatorOverheadSlack = 32

The explicit additive slack in the counter-to-generator overhead lift.

@[simp]

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.generatorOverheadFromCounter_eq (counterOverhead : ℕ) : generatorOverheadFromCounter counterOverhead = counterOverhead + 32

The full generator uses the counter overhead plus the fixed construction slack.

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.size_selectionRoundStateCircuit_le_common {counterOverhead arity prefixLength : ℕ} {beta : PositiveRationalScale} [NeZero arity] (counter : ApproximateCounterCircuit counterOverhead beta arity prefixLength) (hprefix : prefixLength + 1 ≤ requiredRoundCount beta arity) (hbudget : requiredRoundCount beta arity ≤ sampleCount beta arity) : (selectionRoundStateCircuit counter).snd.size ≤ 64 * 2 ^ arity * (counterSizeBound counterOverhead beta arity + (sampleCount beta arity + arity + 1) ^ 2)

Every used selection round has one common size bound once the required round count fits inside the published sample budget.

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.size_selectionPrefixCircuit_le {counterOverhead arity rounds : ℕ} {beta : PositiveRationalScale} [NeZero arity] (family : ApproximateCounterFamily counterOverhead beta arity) (hrounds : rounds ≤ requiredRoundCount beta arity) (hbudget : requiredRoundCount beta arity ≤ sampleCount beta arity) : (selectionPrefixCircuit family rounds hrounds).snd.size ≤ 2 ^ arity + rounds * (64 * 2 ^ arity * (counterSizeBound counterOverhead beta arity + (sampleCount beta arity + arity + 1) ^ 2))

The dependent prefix composition costs at most its truth-table copy plus the number of rounds times the common round bound.

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.size_paddedSelectionCircuit_le_paddedSelectionSizeBound {counterOverhead arity : ℕ} {beta : PositiveRationalScale} [NeZero arity] (family : ApproximateCounterFamily counterOverhead beta arity) (hbudget : requiredRoundCount beta arity ≤ sampleCount beta arity) : (paddedSelectionCircuit family hbudget).snd.size ≤ paddedSelectionSizeBound counterOverhead beta arity

The complete padded circuit lies below the explicit finite construction bound.

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.eventually_paddedSelectionSizeBound_le_generatorSizeBound (counterOverhead : ℕ) (beta : PositiveRationalScale) : ∀ᶠ (arity : ℕ) in Filter.atTop, paddedSelectionSizeBound counterOverhead beta arity ≤ generatorSizeBound (generatorOverheadFromCounter counterOverhead) beta arity

The finite construction bound is eventually at most the generator bound with the explicitly lifted overhead.

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.eventually_size_paddedSelectionCircuit_le_generatorSizeBound (counterOverhead : ℕ) (beta : PositiveRationalScale) : ∀ᶠ (arity : ℕ) in Filter.atTop, ∀ (harity : arity ≠ 0) (family : ApproximateCounterFamily counterOverhead beta arity) (hbudget : requiredRoundCount beta arity ≤ sampleCount beta arity), (paddedSelectionCircuit family hbudget).snd.size ≤ generatorSizeBound (generatorOverheadFromCounter counterOverhead) beta arity

For every sufficiently large positive arity, the actual padded selector circuit satisfies the generator interface's rounded size bound.