SuccinctMCSP witness-class packaging

The complete normalized witness relation has an executable Boolean checker and is already polynomially balanced. Consequently, a polynomial-time machine for its paired language makes the relation an FNP relation; the generic guess-and-verify NTM construction NP.witnessNTMConstruction then places SuccinctMCSP in NP.

The verifier premise remains explicit. This module does not identify ordinary program execution with a proved polynomial-time Turing machine.

@[simp]

theorem Complexity.SuccinctMCSP.verifyRawWitness_eq_true_iff (bits witness : List Bool) : verifyRawWitness bits witness = true ↔ RawWitnessRelation bits witness

The complete Boolean checker decides the normalized raw witness relation.

theorem Complexity.SuccinctMCSP.rawWitnessRelation_mem_FNP_of_pairLang_mem_P (hverifier : pairLang RawWitnessRelation ∈ P) : RawWitnessRelation ∈ FNP

A polynomial-time paired verifier turns the normalized raw relation into an FNP relation.

theorem Complexity.SuccinctMCSP.mem_NP_of_pairLang_mem_P (hverifier : pairLang RawWitnessRelation ∈ P) : SuccinctMCSP ∈ NP

Conditional NP packaging for SuccinctMCSP.

The premise isolates the one remaining machine-level obligation: a P implementation of the paired executable checker.