Raw truth-table MCSP

This module exposes the input convention used by standard hardness- magnification statements: an input is exactly an N = 2^n-bit truth table, while the circuit-size thresholds are external parameters. It proves exact decoder semantics, raw/canonical round trips, and side-preserving maps in both directions between raw and metadata-bearing GapMCSP slices.

The maps below are semantic MapReducesVia witnesses. Their polynomial-time machine realizations are intentionally separate future obligations.

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

A raw truth table of length 2^arity has recovered arity exactly arity.

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

Well-formedness is equivalent to the decoder's concrete power-of-two length check at the recovered arity.

@[simp]

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

Erasing metadata from a canonical instance preserves its arity.

@[simp]

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

Decoding a canonical instance's raw table reinstalls exactly the externally chosen threshold.

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

Exact characterization of successful raw decoding.

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

Raw decoding fails exactly at non-power-of-two lengths.

@[simp]

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

Adding metadata to canonical table bits only replaces the threshold.

@[simp]

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

Erasing metadata from an encoded instance recovers its exact truth table.

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

Adding and then erasing metadata is the identity on every raw truth table.

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

Erasing and reinstalling metadata preserves the table and installs the externally chosen threshold.

@[simp]

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

Raw threshold-slice membership has the expected minimum-size semantics.

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

Every member of raw MCSP[threshold] is exactly a canonical truth table whose minimum circuit size meets the external threshold.

@[simp]

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

Exact yes-side semantics for raw GapMCSP truth tables.

@[simp]

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

Exact no-side semantics for raw GapMCSP truth tables.

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

A pointwise threshold gap makes the raw yes and no languages disjoint.

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

Every raw yes-instance has exactly 2^arity input bits for some arity.

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

Every raw no-instance has exactly 2^arity input bits for some arity.

def Complexity.GapMCSP.rawSliceProblem (parameters : SliceParameters) (hgap : parameters.IsGap) : PromiseProblem

Raw GapMCSP[s_yes,s_no] on bare truth-table inputs.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Complexity.GapMCSP.rawSliceProblem_yesInstances (parameters : SliceParameters) (hgap : parameters.IsGap) : (rawSliceProblem parameters hgap).yesInstances = rawSliceYesLanguage parameters

@[simp]

theorem Complexity.GapMCSP.rawSliceProblem_noInstances (parameters : SliceParameters) (hgap : parameters.IsGap) : (rawSliceProblem parameters hgap).noInstances = rawSliceNoLanguage parameters

theorem Complexity.GapMCSP.mem_rawSliceProblem_promise_imp_isRawTruthTable (parameters : SliceParameters) (hgap : parameters.IsGap) {bits : List Bool} (hmem : bits ∈ (rawSliceProblem parameters hgap).promise) : MCSP.IsRawTruthTable bits

Every input in the raw GapMCSP promise has length exactly 2^arity for some arity.

theorem Complexity.GapMCSP.rawSliceProblem_mapReducesVia_rawToCanonical (parameters : SliceParameters) (hgap : parameters.IsGap) : (rawSliceProblem parameters hgap).MapReducesVia (sliceProblem parameters hgap) (MCSP.rawToCanonical parameters.yesThreshold)

Adding canonical metadata preserves both promised sides of a GapMCSP slice. This is a semantic reduction, not yet an FP theorem.

theorem Complexity.GapMCSP.sliceProblem_mapReducesVia_canonicalToRaw (parameters : SliceParameters) (hgap : parameters.IsGap) : (sliceProblem parameters hgap).MapReducesVia (rawSliceProblem parameters hgap) MCSP.canonicalToRaw

Erasing canonical metadata preserves both promised sides of a GapMCSP slice. This is a semantic reduction, not yet an FP theorem.