Threshold normalization for SuccinctMCSP

This module caps sampled-circuit thresholds at a semantics-preserving linear interpolation bound. A direct DNF uses one exact-input term per positive sample; an existing witness guarantees that no negative sample has the same input as a positive one. The resulting normalized raw witness relation is polynomially balanced in the canonical instance-code length, including empty sample lists at very large binary-encoded arities.

theorem Complexity.SuccinctMCSP.Instance.hasCircuitAtMost_trivialCircuitSizeBound (inst : Instance) (hsmall : inst.HasCircuitAtMost) : { arity := inst.arity, samples := inst.samples, threshold := inst.trivialCircuitSizeBound }.HasCircuitAtMost

Every feasible instance remains feasible at the explicit sampled DNF upper bound. Contradictory instances are not claimed to become feasible.

theorem Complexity.SuccinctMCSP.Instance.effectiveThreshold_le_threshold (inst : Instance) : inst.effectiveThreshold ≤ inst.threshold

The effective threshold never exceeds the threshold supplied in the code.

theorem Complexity.SuccinctMCSP.Instance.effectiveThreshold_le_trivialCircuitSizeBound (inst : Instance) : inst.effectiveThreshold ≤ inst.trivialCircuitSizeBound

The effective threshold never exceeds the sampled interpolation bound.

@[simp]

theorem Complexity.SuccinctMCSP.Instance.hasCircuitAtMost_normalizeThreshold_iff (inst : Instance) : inst.normalizeThreshold.HasCircuitAtMost ↔ inst.HasCircuitAtMost

Capping the threshold at the sampled interpolation bound preserves feasibility in both directions.

theorem Complexity.SuccinctMCSP.Instance.trivialCircuitSizeBound_le_encodeLength (inst : Instance) : inst.trivialCircuitSizeBound ≤ inst.encode.length

The sampled interpolation bound is no larger than the canonical instance code itself.

theorem Complexity.SuccinctMCSP.Instance.rawWitnessLengthPolynomial_polyBound : PolyBound rawWitnessLengthPolynomial

The explicit normalized raw-witness envelope is polynomial.

theorem Complexity.SuccinctMCSP.Instance.exists_normalizedRawWitness_length_le_encode (inst : Instance) (hsmall : inst.HasCircuitAtMost) : ∃ (code : List Bool), inst.normalizeThreshold.IsRawCircuitWitness code ∧ code.length ≤ rawWitnessLengthPolynomial inst.encode.length

Every sampled yes-instance has a normalized raw witness whose code is polynomially bounded by the canonical instance-code length.

theorem Complexity.SuccinctMCSP.rawWitnessRelation_polyBalanced : PolyBalanced RawWitnessRelation

The normalized raw witness relation is polynomially balanced.

theorem Complexity.SuccinctMCSP.mem_iff_exists_rawWitnessRelation (bits : List Bool) : bits ∈ SuccinctMCSP ↔ ∃ (witness : List Bool), RawWitnessRelation bits witness

SuccinctMCSP membership is exactly existence of a normalized, polynomially bounded raw witness.