Conditional anti-checker counter circuits -- definitions

For each sample-prefix length, an approximate counter circuit maps the fixed-width labeled-sample encoding to a little-endian estimate of the number of surviving canonical small-circuit codes. The circuit family and its size bound are an explicit conditional interface: this file does not assert that NP ⊆ P/poly supplies such families.

def Complexity.GapMCSP.Magnification.AntiCheckerLemma.counterOutputWidth (beta : PositiveRationalScale) (arity : ℕ) : ℕ

Number of output bits allocated to one approximate survivor count.

Equations

• Complexity.GapMCSP.Magnification.AntiCheckerLemma.counterOutputWidth beta arity = Complexity.GapMCSP.Magnification.AntiCheckerLemma.roundBlockCount beta arity + 1

instance Complexity.GapMCSP.Magnification.AntiCheckerLemma.instNeZeroNatCounterOutputWidth (beta : PositiveRationalScale) (arity : ℕ) : NeZero (counterOutputWidth beta arity)

def Complexity.GapMCSP.Magnification.AntiCheckerLemma.counterSizeBound (overhead : ℕ) (beta : PositiveRationalScale) (arity : ℕ) : ℕ

Ceiling-rounded 2^(k*beta*n) size bound for one counter circuit.

Equations

• Complexity.GapMCSP.Magnification.AntiCheckerLemma.counterSizeBound overhead beta arity = beta.powCeil (overhead * arity)

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

One size-bounded approximate counter circuit for prefixes of length prefixLength + 1.

• internalGates : ℕ

  Number of internal gates in the counter circuit.

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

  Circuit from packed labeled samples to a little-endian count estimate.

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

  Conditional per-counter circuit size bound.

def Complexity.GapMCSP.Magnification.AntiCheckerLemma.ApproximateCounterCircuit.estimate {overhead arity prefixLength : ℕ} {beta : PositiveRationalScale} (counter : ApproximateCounterCircuit overhead beta arity prefixLength) (input : BitString ((prefixLength + 1) * (arity + 1))) : ℕ

Natural estimate printed by a counter circuit on one packed sample vector.

Equations

• counter.estimate input = Complexity.GapMCSP.Magnification.AntiCheckerLemma.counterValue (counter.circuit.eval input)

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

A counter circuit relatively approximates the labeled survivor count on every fixed-width input.

Equations

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

structure Complexity.GapMCSP.Magnification.AntiCheckerLemma.ApproximateCounterFamily (overhead : ℕ) (beta : PositiveRationalScale) (arity : ℕ) : Type

One approximate counter circuit for every prefix length used by the anti-checker construction.

• counter (prefixLength : Fin (requiredRoundCount beta arity)) : ApproximateCounterCircuit overhead beta arity ↑prefixLength

  Counter for the next extension of a prefix of the indexed length.

def Complexity.GapMCSP.Magnification.AntiCheckerLemma.ApproximateCounterFamily.IsCorrect {overhead arity : ℕ} {beta : PositiveRationalScale} (family : ApproximateCounterFamily overhead beta arity) : Prop

Every counter in the finite family satisfies its approximation contract.

Equations

• family.IsCorrect = ∀ (prefixLength : Fin (Complexity.GapMCSP.Magnification.AntiCheckerLemma.requiredRoundCount beta arity)), (family.counter prefixLength).IsCorrect

def Complexity.GapMCSP.Magnification.AntiCheckerLemma.ExistsCorrectCounterFamilyAt (overhead : ℕ) (beta : PositiveRationalScale) (arity : ℕ) : Prop

A correct bounded counter family exists at one arity.

Equations

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

def Complexity.GapMCSP.Magnification.AntiCheckerLemma.HasApproximateCounterFamilies : Prop

Quantifier structure of the conditional approximate-counter conclusion: one overhead works for every positive rational scale at all sufficiently large arities. This proposition is defined but not proved here.

Equations

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