Randomized anti-checker counters -- definitions

A randomized approximate counter circuit receives a random seed before the fixed-width labeled-sample input and prints a little-endian count estimate. Its correctness contract bounds, separately for every input, the uniform probability that the estimate violates the existing relative-error predicate.

The failure exponent includes one bit of strict union-bound slack. This is the exact finite contract needed to select one seed that is accurate on every fixed-width input simultaneously.

def Complexity.GapMCSP.Magnification.AntiCheckerLemma.CounterOutputIsAccurate {arity prefixLength : ℕ} (beta : PositiveRationalScale) (input : BitString ((prefixLength + 1) * (arity + 1))) (output : BitString (counterOutputWidth beta arity)) : Prop

A counter output relatively approximates the labeled survivor count for one fixed-width input.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Complexity.GapMCSP.Magnification.AntiCheckerLemma.instDecidableCounterOutputIsAccurate {arity prefixLength : ℕ} (beta : PositiveRationalScale) (input : BitString ((prefixLength + 1) * (arity + 1))) (output : BitString (counterOutputWidth beta arity)) : Decidable (CounterOutputIsAccurate beta input output)

Equations

• Complexity.GapMCSP.Magnification.AntiCheckerLemma.instDecidableCounterOutputIsAccurate beta input output = id (id inferInstance)

structure Complexity.GapMCSP.Magnification.AntiCheckerLemma.RandomizedApproximateCounterCircuit (overhead : ℕ) (beta : PositiveRationalScale) (arity prefixLength seedWidth : ℕ) : Type

A size-bounded randomized counter with random bits placed before its labeled-sample input. Correctness is kept as the separate IsCorrect predicate below, mirroring ApproximateCounterCircuit.

• internalGates : ℕ

  Number of internal gates in the randomized counter circuit.

• circuit : Circuit Basis.andOr2 (seedWidth + (prefixLength + 1) * (arity + 1)) (counterOutputWidth beta arity) self.internalGates

  Seed-prefix circuit that prints a little-endian count estimate.

• size_le : self.circuit.size ≤ counterSizeBound overhead beta arity

  The same conditional size bound used by deterministic counters.

def Complexity.GapMCSP.Magnification.AntiCheckerLemma.RandomizedApproximateCounterCircuit.failureEvent {overhead arity prefixLength seedWidth : ℕ} {beta : PositiveRationalScale} (counter : RandomizedApproximateCounterCircuit overhead beta arity prefixLength seedWidth) (input : BitString ((prefixLength + 1) * (arity + 1))) : Finset (BitString seedWidth)

Seeds on which the randomized counter violates relative accuracy at one fixed input.

Equations

• counter.failureEvent input = counter.circuit.badSeedEvent (Complexity.GapMCSP.Magnification.AntiCheckerLemma.CounterOutputIsAccurate beta) input

def Complexity.GapMCSP.Magnification.AntiCheckerLemma.RandomizedApproximateCounterCircuit.IsCorrect {overhead arity prefixLength seedWidth : ℕ} {beta : PositiveRationalScale} (counter : RandomizedApproximateCounterCircuit overhead beta arity prefixLength seedWidth) : Prop

Every fixed input has failure probability at most one over 2^(inputWidth + 1), leaving strict slack for a union bound over all inputs.

Equations

• counter.IsCorrect = ∀ (input : Complexity.BitString ((prefixLength + 1) * (arity + 1))), Complexity.eventProb (counter.failureEvent input) ≤ 1 / 2 ^ ((prefixLength + 1) * (arity + 1) + 1)