Threshold normalization for MCSP -- definitions

Binary thresholds can denote values exponentially larger than their encoded width. MCSP nevertheless has an unconditional circuit-size upper bound that is polynomial in truth-table length. This layer caps thresholds at a concrete bound without changing yes/no semantics and defines the resulting polynomial raw-witness envelope.

def Complexity.MCSP.Instance.trivialCircuitSizeBound (inst : Instance) : ℕ

Coarse unconditional circuit-size bound for the represented function.

For positive arity this is the square of truth-table length plus two. Arity zero retains the separate size-zero convention.

Equations

• inst.trivialCircuitSizeBound = if inst.arity = 0 then 0 else (2 ^ inst.arity + 2) ^ 2

def Complexity.MCSP.Instance.effectiveThreshold (inst : Instance) : ℕ

Threshold capped at the unconditional circuit-size upper bound.

Equations

• inst.effectiveThreshold = min inst.threshold inst.trivialCircuitSizeBound

def Complexity.MCSP.Instance.normalizeThreshold (inst : Instance) : Instance

Replace an instance's possibly oversized threshold by its effective cap.

Equations

• inst.normalizeThreshold = inst.withThreshold inst.effectiveThreshold

def Complexity.MCSP.Instance.rawWitnessLengthPolynomial (inputLength : ℕ) : ℕ

Polynomial envelope for a normalized raw-circuit witness, expressed only in the encoded instance length.

Equations

• Complexity.MCSP.Instance.rawWitnessLengthPolynomial inputLength = 1 + (inputLength + 2) ^ 2 * (2 * (inputLength + (inputLength + 2) ^ 2) + 6)

def Complexity.MCSP.RawWitnessRelation (bits witness : List Bool) : Prop

Polynomially balanced raw-circuit relation used by the MCSP verifier.

The input must decode canonically, and the witness is checked against the semantics-preserving normalized threshold rather than an arbitrarily large binary threshold from the input.

Equations

• Complexity.MCSP.RawWitnessRelation bits witness = match Complexity.MCSP.Instance.decode? bits with | none => False | some inst => inst.normalizeThreshold.IsRawCircuitWitness witness