Anti-checker generator size bounds -- proof internals

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.size_selectionRoundStateCircuit_le_common_internal {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)

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.size_selectionPrefixCircuit_le_internal {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))

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.size_paddedSelectionCircuit_le_paddedSelectionSizeBound_internal {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

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

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.eventually_size_paddedSelectionCircuit_le_generatorSizeBound_internal (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