The Minimum Circuit Size Problem

This module exposes a canonical, total MCSP syntax and its exact relationship to the library's Boolean circuit complexity measure.

Main definitions

• MCSP.Instance -- arity, a structurally exact truth table, and threshold
• MCSP.Instance.encode / decode? -- canonical total binary codec
• MCSP.Instance.ofFunction -- exact function-to-truth-table packaging
• MCSP.Instance.function -- little-endian truth-table semantics
• MCSP.Instance.HasCircuitAtMost -- direct circuit-witness predicate
• MCSP.Instance.verifyRawCircuit -- executable canonical witness checker
• MCSP.Instance.normalizeThreshold -- semantics-preserving threshold cap
• MCSP.atThreshold -- arity-indexed canonical threshold slices
• GapMCSP.problem -- two-threshold MCSP promise with explicit relaxation
• GapMCSP.sliceProblem -- conventional GapMCSP[s_yes, s_no] slices
• MCSP -- encoded language, with malformed strings rejected

The zero-arity case is explicit: its one truth-table bit is stored directly and has size zero, matching CircuitFamily. Positive arities use Basis.andOr2 and agree exactly with Circuit.sizeComplexity.

@[simp]

theorem Complexity.MCSP.Instance.length_tableBits (inst : Instance) : inst.tableBits.length = 2 ^ inst.arity

Every instance carries exactly 2^arity truth-table bits.

@[simp]

theorem Complexity.MCSP.Instance.inputIndex_inputOfIndex {arity : ℕ} (index : Fin (2 ^ arity)) : inputIndex (inputOfIndex index) = index

Converting a truth-table index to an input and back recovers the index.

@[simp]

theorem Complexity.MCSP.Instance.inputOfIndex_inputIndex {arity : ℕ} (input : BitString arity) : inputOfIndex (inputIndex input) = input

Converting a fixed-length input to its truth-table index and back recovers the input.

@[simp]

theorem Complexity.MCSP.Instance.function_inputOfIndex (inst : Instance) (index : Fin (2 ^ inst.arity)) : inst.function (inputOfIndex index) = inst.table index

Evaluating the represented function on index k returns truth-table entry k under the canonical little-endian enumeration.

@[simp]

theorem Complexity.MCSP.Instance.arity_ofFunction (arity threshold : ℕ) (f : BitString arity → Bool) : (ofFunction arity threshold f).arity = arity

@[simp]

theorem Complexity.MCSP.Instance.threshold_ofFunction (arity threshold : ℕ) (f : BitString arity → Bool) : (ofFunction arity threshold f).threshold = threshold

@[simp]

theorem Complexity.MCSP.Instance.function_ofFunction (arity threshold : ℕ) (f : BitString arity → Bool) : (ofFunction arity threshold f).function = f

Reading the canonical truth table of a packaged Boolean function recovers that function exactly.

@[simp]

theorem Complexity.MCSP.Instance.function_withThreshold (inst : Instance) (threshold : ℕ) : (inst.withThreshold threshold).function = inst.function

Changing the threshold does not change the represented function.

@[simp]

theorem Complexity.MCSP.Instance.decode?_encode (inst : Instance) : decode? inst.encode = some inst

Canonical MCSP encodings decode to their original instances.

theorem Complexity.MCSP.Instance.decode?_eq_some_iff (bits : List Bool) (inst : Instance) : decode? bits = some inst ↔ bits = inst.encode

Exact decoding accepts precisely canonical encodings.

theorem Complexity.MCSP.Instance.decode?_eq_none_iff (bits : List Bool) : decode? bits = none ↔ ¬∃ (inst : Instance), bits = inst.encode

Decoding rejects exactly those strings that are not canonical encodings of any well-formed MCSP instance.

theorem Complexity.MCSP.Instance.encode_injective : Function.Injective encode

Canonical MCSP instance encoding is injective.

@[simp]

theorem Complexity.MCSP.Instance.length_encode (inst : Instance) : inst.encode.length = 2 ^ inst.arity + 2 * inst.arity.size + 2 * inst.threshold.size + 4

Exact encoded length, exposing truth-table length 2^n separately from the logarithmic-width arity and threshold fields.

theorem Complexity.MCSP.Instance.tableLength_le_encodeLength (inst : Instance) : 2 ^ inst.arity ≤ inst.encode.length

The truth-table payload is no longer than the complete instance code.

theorem Complexity.MCSP.Instance.minimumSize_of_arity_eq_zero (inst : Instance) (harity : inst.arity = 0) : inst.minimumSize = 0

Zero-input Boolean functions use the explicit size-zero family convention.

theorem Complexity.MCSP.Instance.minimumSize_eq_sizeComplexity (inst : Instance) [NeZero inst.arity] : inst.minimumSize = Circuit.sizeComplexity Basis.andOr2 inst.function

At every positive arity, MCSP uses exactly the existing fan-in-two circuit complexity measure.

theorem Complexity.MCSP.Instance.hasCircuitAtMost_of_arity_eq_zero (inst : Instance) (harity : inst.arity = 0) : inst.HasCircuitAtMost

Every zero-arity instance is a yes-instance at every natural threshold.

theorem Complexity.MCSP.Instance.hasCircuitAtMost_iff_sizeComplexity_le (inst : Instance) [NeZero inst.arity] : inst.HasCircuitAtMost ↔ Circuit.sizeComplexity Basis.andOr2 inst.function ≤ inst.threshold

At positive arity, the direct circuit-witness semantics agrees with the minimum circuit-size inequality.

theorem Complexity.MCSP.Instance.hasCircuitAtMost_iff_minimumSize_le (inst : Instance) : inst.HasCircuitAtMost ↔ inst.minimumSize ≤ inst.threshold

The total witness semantics agrees with the total minimum-size convention, including arity zero.

theorem Complexity.MCSP.Instance.HasCircuitAtMost.mono (inst : Instance) {first second : ℕ} (hthreshold : first ≤ second) (hsmall : (inst.withThreshold first).HasCircuitAtMost) : (inst.withThreshold second).HasCircuitAtMost

Increasing the threshold preserves MCSP yes-instances.

@[simp]

theorem Complexity.MCSP.mem_encode_iff (inst : Instance) : inst.encode ∈ MCSP ↔ inst.HasCircuitAtMost

A canonical instance code belongs to MCSP exactly when the decoded instance has a circuit at most its threshold.

theorem Complexity.MCSP.mem_encode_iff_minimumSize_le (inst : Instance) : inst.encode ∈ MCSP ↔ inst.minimumSize ≤ inst.threshold

Membership of a canonical code is exactly its total minimum-size inequality, including the explicit zero-arity convention.

theorem Complexity.MCSP.mem_encode_iff_sizeComplexity_le (inst : Instance) [NeZero inst.arity] : inst.encode ∈ MCSP ↔ Circuit.sizeComplexity Basis.andOr2 inst.function ≤ inst.threshold

At positive arity, canonical encoded MCSP membership agrees exactly with the library's existing fan-in-two size complexity.

theorem Complexity.MCSP.mem_encode_of_arity_eq_zero (inst : Instance) (harity : inst.arity = 0) : inst.encode ∈ MCSP

The canonical code of every zero-arity instance is in MCSP.

theorem Complexity.MCSP.not_mem_of_decode?_eq_none {bits : List Bool} (hdecode : Instance.decode? bits = none) : bits ∉ MCSP

Every malformed instance code is rejected by the total MCSP language.

theorem Complexity.MCSP.mem_iff_exists (bits : List Bool) : bits ∈ MCSP ↔ ∃ (inst : Instance), Instance.decode? bits = some inst ∧ inst.HasCircuitAtMost

Decoded language membership has an explicit unique-instance witness.