Raw truth-table MCSP -- proof internals

theorem Complexity.MCSP.rawArity_eq_of_length_eq_pow_internal (bits : List Bool) {arity : ℕ} (hlength : bits.length = 2 ^ arity) : rawArity bits = arity

theorem Complexity.MCSP.isRawTruthTable_iff_length_eq_pow_rawArity_internal (bits : List Bool) : IsRawTruthTable bits ↔ bits.length = 2 ^ rawArity bits

theorem Complexity.MCSP.rawArity_tableBits_internal (inst : Instance) : rawArity inst.tableBits = inst.arity

theorem Complexity.MCSP.rawDecode?_tableBits_internal (threshold : ℕ → ℕ) (inst : Instance) : rawDecode? threshold inst.tableBits = some (inst.withThreshold (threshold inst.arity))

theorem Complexity.MCSP.rawDecode?_eq_some_iff_internal (threshold : ℕ → ℕ) (bits : List Bool) (inst : Instance) : rawDecode? threshold bits = some inst ↔ bits = inst.tableBits ∧ inst.threshold = threshold inst.arity

theorem Complexity.MCSP.rawDecode?_eq_none_iff_internal (threshold : ℕ → ℕ) (bits : List Bool) : rawDecode? threshold bits = none ↔ ¬IsRawTruthTable bits

theorem Complexity.MCSP.rawToCanonical_tableBits_internal (threshold : ℕ → ℕ) (inst : Instance) : rawToCanonical threshold inst.tableBits = (inst.withThreshold (threshold inst.arity)).encode

theorem Complexity.MCSP.canonicalToRaw_encode_internal (inst : Instance) : canonicalToRaw inst.encode = inst.tableBits

theorem Complexity.MCSP.canonicalToRaw_rawToCanonical_internal (threshold : ℕ → ℕ) {bits : List Bool} (hraw : IsRawTruthTable bits) : canonicalToRaw (rawToCanonical threshold bits) = bits

theorem Complexity.MCSP.rawToCanonical_canonicalToRaw_encode_internal (threshold : ℕ → ℕ) (inst : Instance) : rawToCanonical threshold (canonicalToRaw inst.encode) = (inst.withThreshold (threshold inst.arity)).encode

theorem Complexity.MCSP.mem_rawAtThreshold_tableBits_iff_internal (threshold : ℕ → ℕ) (inst : Instance) : inst.tableBits ∈ rawAtThreshold threshold ↔ inst.minimumSize ≤ threshold inst.arity

theorem Complexity.MCSP.mem_rawAtThreshold_iff_exists_internal (threshold : ℕ → ℕ) (bits : List Bool) : bits ∈ rawAtThreshold threshold ↔ ∃ (inst : Instance), bits = inst.tableBits ∧ inst.minimumSize ≤ threshold inst.arity

theorem Complexity.GapMCSP.mem_rawSliceYesLanguage_tableBits_iff_internal (parameters : SliceParameters) (inst : MCSP.Instance) : inst.tableBits ∈ rawSliceYesLanguage parameters ↔ inst.minimumSize ≤ parameters.yesThreshold inst.arity

theorem Complexity.GapMCSP.mem_rawSliceNoLanguage_tableBits_iff_internal (parameters : SliceParameters) (inst : MCSP.Instance) : inst.tableBits ∈ rawSliceNoLanguage parameters ↔ parameters.noThreshold inst.arity < inst.minimumSize

theorem Complexity.GapMCSP.disjoint_rawSliceLanguages_internal (parameters : SliceParameters) (hgap : parameters.IsGap) : Disjoint (rawSliceYesLanguage parameters) (rawSliceNoLanguage parameters)

theorem Complexity.GapMCSP.mem_rawSliceYesLanguage_imp_isRawTruthTable_internal (parameters : SliceParameters) {bits : List Bool} (hmem : bits ∈ rawSliceYesLanguage parameters) : MCSP.IsRawTruthTable bits

theorem Complexity.GapMCSP.mem_rawSliceNoLanguage_imp_isRawTruthTable_internal (parameters : SliceParameters) {bits : List Bool} (hmem : bits ∈ rawSliceNoLanguage parameters) : MCSP.IsRawTruthTable bits

theorem Complexity.GapMCSP.rawSliceProblem_mapReducesVia_rawToCanonical_internal (parameters : SliceParameters) (hgap : parameters.IsGap) : { yesInstances := rawSliceYesLanguage parameters, noInstances := rawSliceNoLanguage parameters, disjoint := ⋯ }.MapReducesVia { yesInstances := sliceYesLanguage parameters, noInstances := sliceNoLanguage parameters, disjoint := ⋯ } (MCSP.rawToCanonical parameters.yesThreshold)

theorem Complexity.GapMCSP.sliceProblem_mapReducesVia_canonicalToRaw_internal (parameters : SliceParameters) (hgap : parameters.IsGap) : { yesInstances := sliceYesLanguage parameters, noInstances := sliceNoLanguage parameters, disjoint := ⋯ }.MapReducesVia { yesInstances := rawSliceYesLanguage parameters, noInstances := rawSliceNoLanguage parameters, disjoint := ⋯ } MCSP.canonicalToRaw