Threshold normalization for SuccinctMCSP -- definitions

A satisfiable sample list has a direct DNF interpolant whose size is linear in the number of samples times their arity. Capping the stored threshold at this bound therefore preserves sampled feasibility and prevents oversized binary thresholds from inflating circuit witnesses.

The final raw witness relation additionally enforces a polynomial code-length cap. This matters for an empty sample list at a huge binary-encoded arity: a one-gate raw circuit could otherwise contain an unnecessarily huge unary wire reference even though a fixed constant gate is a sufficient witness.

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

Linear-size upper bound for a circuit interpolating any consistent sample list.

Equations

• inst.trivialCircuitSizeBound = 1 + inst.samples.length * (3 * inst.arity + 2)

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

Threshold capped at the sampled interpolation bound.

Equations

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

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

Replace only the threshold by its semantics-preserving effective cap.

Equations

• inst.normalizeThreshold = { arity := inst.arity, samples := inst.samples, threshold := inst.effectiveThreshold }

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

Polynomial envelope imposed on the canonical raw witness code.

Equations

• Complexity.SuccinctMCSP.Instance.rawWitnessLengthPolynomial inputLength = 1 + inputLength * (4 * inputLength + 6)

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

Polynomially balanced raw witness relation for encoded SuccinctMCSP.

The instance is decoded canonically, checked at its normalized threshold, and the raw code itself must fit the explicit polynomial envelope.

Equations

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