Raw truth-table MCSP -- definitions

Hardness-magnification papers conventionally give MCSP only the N = 2^n truth-table bits and fix the circuit-size threshold externally. The canonical MCSP.Instance codec instead stores arity and threshold metadata. This module defines the raw convention and total maps between the two representations.

A raw string is well formed exactly when its length is a power of two. Its arity is recovered by base-two logarithm. Malformed lengths are outside both sides of every raw gap problem; no arbitrary threshold or arity is assigned to them.

def Complexity.MCSP.IsRawTruthTable (bits : List Bool) : Prop

A list is a raw truth table when its length is exactly 2^arity for some arity. In particular, the empty list is not a raw truth table.

Equations

• Complexity.MCSP.IsRawTruthTable bits = ∃ (arity : ℕ), bits.length = 2 ^ arity

def Complexity.MCSP.rawArity (bits : List Bool) : ℕ

Recover the arity of a prospective raw truth table from its length.

Equations

• Complexity.MCSP.rawArity bits = Nat.log 2 bits.length

def Complexity.MCSP.rawDecode? (threshold : ℕ → ℕ) (bits : List Bool) : Option Instance

Decode a raw truth table at an externally supplied arity-indexed threshold.

The decoder succeeds only at exact power-of-two lengths.

Equations

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

def Complexity.MCSP.rawAtThreshold (threshold : ℕ → ℕ) : Language

Raw MCSP[threshold]: the input contains only its truth-table bits.

Equations

• Complexity.MCSP.rawAtThreshold threshold = {bits : List Bool | match Complexity.MCSP.rawDecode? threshold bits with | some inst => inst.HasCircuitAtMost | none => False}

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

Add canonical arity and threshold metadata to a raw truth table. Malformed raw strings are sent to the empty, noncanonical code.

Equations

• Complexity.MCSP.rawToCanonical threshold bits = match Complexity.MCSP.rawDecode? threshold bits with | some inst => inst.encode | none => []

def Complexity.MCSP.canonicalToRaw (bits : List Bool) : List Bool

Erase arity and threshold metadata from a canonical MCSP code. Malformed canonical strings are sent to the empty, malformed raw string.

Equations

• Complexity.MCSP.canonicalToRaw bits = match Complexity.MCSP.Instance.decode? bits with | some inst => inst.tableBits | none => []

def Complexity.GapMCSP.rawSliceYesLanguage (parameters : SliceParameters) : Language

Yes side of raw GapMCSP[s_yes,s_no].

Equations

• Complexity.GapMCSP.rawSliceYesLanguage parameters = Complexity.MCSP.rawAtThreshold parameters.yesThreshold

def Complexity.GapMCSP.rawSliceNoLanguage (parameters : SliceParameters) : Language

No side of raw GapMCSP[s_yes,s_no]. The input has no encoded threshold; the no cutoff is supplied entirely by the problem parameters.

Equations

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