Anti-checker generator assembly -- definitions #
This layer packages the padded selection circuit as a Generator once its
eventual finite size inequality has been supplied.
noncomputable def
Complexity.GapMCSP.Magnification.AntiCheckerLemma.generatorOfCounterFamily
{counterOverhead arity : ℕ}
{beta : PositiveRationalScale}
[NeZero arity]
(family : ApproximateCounterFamily counterOverhead beta arity)
(hbudget : requiredRoundCount beta arity ≤ sampleCount beta arity)
(hsize :
(paddedSelectionCircuit family hbudget).snd.size ≤ generatorSizeBound (generatorOverheadFromCounter counterOverhead) beta arity)
:
Generator (generatorOverheadFromCounter counterOverhead) beta arity
Package a padded selector built from one approximate-counter family as a generator with the explicitly lifted overhead.
Equations
- One or more equations did not get rendered due to their size.