Nonuniform circuit size for promise problems -- definitions

The completion-based lift PromiseClass (SIZE s) is the right extensional meaning of a circuit family solving a promise problem: behavior outside the promise is arbitrary. This module gives that class a direct name and separately defines eventual size bounds, so finite exceptional lengths are never hidden in an asymptotic hardness-magnification statement.

def Complexity.CircuitFamily.EventuallySizeBoundedBy {B : Basis} (family : CircuitFamily B) (bound : ℕ → ℕ) : Prop

A circuit family satisfies a size bound at every sufficiently large input length.

Equations

• family.EventuallySizeBoundedBy bound = ∀ᶠ (length : ℕ) in Filter.atTop, family.size length ≤ bound length

def Complexity.PromiseSIZEWithBasis (B : Basis) (bound : ℕ → ℕ) : Set PromiseProblem

Promise problems solvable by B-circuits within a pointwise size bound.

Equations

• Complexity.PromiseSIZEWithBasis B bound = Complexity.PromiseClass (Complexity.SIZEWithBasis B bound)

def Complexity.PromiseSIZE (bound : ℕ → ℕ) : Set PromiseProblem

Promise problems solvable by the library's fan-in-two AND/OR circuits within a pointwise size bound.

Equations

• Complexity.PromiseSIZE bound = Complexity.PromiseSIZEWithBasis Complexity.Basis.andOr2 bound

def Complexity.PromisePPoly : Set PromiseProblem

Promise problems with a completion in P/poly.

Equations

• Complexity.PromisePPoly = Complexity.PromiseClass Complexity.PPoly

def Complexity.PromiseEventuallySIZEWithBasis (B : Basis) (bound : ℕ → ℕ) : Set PromiseProblem

Promise problems solved by B-circuit families meeting a size bound at all sufficiently large lengths.

Equations

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

def Complexity.PromiseEventuallySIZE (bound : ℕ → ℕ) : Set PromiseProblem

Eventual-size promise circuits over the library's fan-in-two AND/OR basis.

Equations

• Complexity.PromiseEventuallySIZE bound = Complexity.PromiseEventuallySIZEWithBasis Complexity.Basis.andOr2 bound