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 repository's generic guess-and-verify NTM construction then places SuccinctMCSP in NP.

Both machine-level premises remain 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 (hwitness : NP.WitnessNTMConstruction) (hverifier : pairLang RawWitnessRelation ∈ P) : SuccinctMCSP ∈ NP

Conditional NP packaging for SuccinctMCSP.

The premises isolate the two remaining machine-level obligations: the generic FNP witness NTM construction and a P implementation of the paired executable checker.