Threshold normalization for SuccinctMCSP -- proof internals

The main construction is a DNF formula containing one exact-input term for each positive sample. Consistency supplied by any existing witness ensures that this formula also rejects every negative sample.

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

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

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

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

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

theorem Complexity.SuccinctMCSP.Instance.rawWitnessLengthPolynomial_polyBound_internal : PolyBound rawWitnessLengthPolynomial

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

theorem Complexity.SuccinctMCSP.rawWitnessRelation_polyBalanced_internal : PolyBalanced RawWitnessRelation

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