Threshold slices of MCSP -- definitions

Hardness-magnification statements normally fix a circuit-size threshold as a function of the represented arity. This module retains the canonical full MCSP codec, but restricts its threshold field to the chosen function. It also gives a total re-encoding map that changes only that field.

def Complexity.MCSP.rethreshold (threshold : ℕ → ℕ) (bits : List Bool) : List Bool

Replace the threshold of every decodable MCSP instance by an arity-indexed threshold. Malformed strings are fixed.

Equations

• Complexity.MCSP.rethreshold threshold bits = match Complexity.MCSP.Instance.decode? bits with | some inst => (inst.withThreshold (threshold inst.arity)).encode | none => bits

def Complexity.MCSP.atThreshold (threshold : ℕ → ℕ) : Set (List Bool)

The canonical MCSP language restricted to instances whose encoded threshold is the prescribed function of arity.

Equations

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