Succinct Minimum Circuit Size Problem

This module exposes sampled circuit minimization. A typed instance contains an arity, a list of input/output samples, and a circuit-size threshold. Repeated inputs are retained, including contradictory constraints. Positive arities use the library's exact Basis.andOr2 convention; zero arity uses an explicit constant bit of size zero.

The binary codec is exact and total. In particular, malformed pairing, noncanonical natural fields, wrong-width sample inputs, non-singleton outputs, and any mismatch between the stored sample count and payload are rejected. Its raw-circuit verifier checks every sample and is exact for the typed semantics; threshold normalization supplies a polynomially balanced witness relation and the class wrapper records the remaining machine-level premises for NP.

@[simp]

theorem Complexity.SuccinctMCSP.Sample.matchesFunction_ofFunction {arity : ℕ} (f : BitString arity → Bool) (input : BitString arity) : (ofFunction f input).MatchesFunction f

A sample built from f is satisfied by f.

@[simp]

theorem Complexity.SuccinctMCSP.Sample.decode?_encode {arity : ℕ} (sample : Sample arity) : decode? arity sample.encode = some sample

Canonical sample encodings decode to their original typed samples.

theorem Complexity.SuccinctMCSP.Sample.decode?_eq_some_iff {arity : ℕ} (bits : List Bool) (sample : Sample arity) : decode? arity bits = some sample ↔ bits = sample.encode

Sample decoding succeeds precisely on the canonical encoding of its result.

@[simp]

theorem Complexity.SuccinctMCSP.Sample.length_encode {arity : ℕ} (sample : Sample arity) : sample.encode.length = 2 * arity + 3

Exact encoded length of one arity-bit sample.

@[simp]

theorem Complexity.SuccinctMCSP.decodeSamples?_encodeSamples {arity : ℕ} (samples : List (Sample arity)) : decodeSamples? arity samples.length (encodeSamples samples) = some samples

A canonical right-nested sample list decodes at its exact count.

theorem Complexity.SuccinctMCSP.decodeSamples?_eq_some_iff {arity count : ℕ} (bits : List Bool) (samples : List (Sample arity)) : decodeSamples? arity count bits = some samples ↔ samples.length = count ∧ bits = encodeSamples samples

Successful sample-list decoding characterizes both the exact count and canonical payload.

@[simp]

theorem Complexity.SuccinctMCSP.length_encodeSamples {arity : ℕ} (samples : List (Sample arity)) : (encodeSamples samples).length = samples.length * (4 * arity + 8)

The nested payload uses exactly 4 * arity + 8 bits per sample.

@[simp]

theorem Complexity.SuccinctMCSP.Instance.arity_ofInputs {arity threshold : ℕ} (f : BitString arity → Bool) (inputs : List (BitString arity)) : (ofInputs threshold f inputs).arity = arity

@[simp]

theorem Complexity.SuccinctMCSP.Instance.threshold_ofInputs {arity threshold : ℕ} (f : BitString arity → Bool) (inputs : List (BitString arity)) : (ofInputs threshold f inputs).threshold = threshold

@[simp]

theorem Complexity.SuccinctMCSP.Instance.length_samples_ofInputs {arity threshold : ℕ} (f : BitString arity → Bool) (inputs : List (BitString arity)) : (ofInputs threshold f inputs).samples.length = inputs.length

theorem Complexity.SuccinctMCSP.Instance.samplesFunction_ofInputs {arity threshold : ℕ} (f : BitString arity → Bool) (inputs : List (BitString arity)) : (ofInputs threshold f inputs).SamplesFunction f

The function used to label an input list satisfies every resulting sample, including repeated inputs.

@[simp]

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

Canonical sampled-instance encodings decode to their original instances.

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

Instance decoding succeeds precisely on the canonical encoding of its result.

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

Decoding rejects exactly strings that encode no sampled instance.

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

The canonical sampled-instance encoding is injective.

@[simp]

theorem Complexity.SuccinctMCSP.Instance.length_encode (inst : Instance) : inst.encode.length = inst.samples.length * (4 * inst.arity + 8) + 2 * inst.arity.size + 2 * inst.threshold.size + 2 * inst.samples.length.size + 6

Exact instance-code length, separating the linear sample payload from binary metadata.

theorem Complexity.SuccinctMCSP.Instance.hasCircuitAtMost_of_arity_eq_zero_iff (inst : Instance) (harity : inst.arity = 0) : inst.HasCircuitAtMost ↔ ∃ (output : Bool), inst.SamplesFunction fun (x : BitString inst.arity) => output

At arity zero, a sampled instance is feasible exactly when one constant bit satisfies every listed constraint.

theorem Complexity.SuccinctMCSP.Instance.hasCircuitAtMost_iff_exists_circuit (inst : Instance) [NeZero inst.arity] : inst.HasCircuitAtMost ↔ ∃ (internalGates : ℕ) (circuit : Circuit Basis.andOr2 inst.arity 1 internalGates), circuit.size ≤ inst.threshold ∧ inst.SamplesFunction fun (input : BitString inst.arity) => circuit.eval input 0

At positive arity, feasibility has exactly the advertised sampled-circuit witness semantics.

theorem Complexity.SuccinctMCSP.Instance.HasCircuitAtMost.mono (inst : Instance) {first second : ℕ} (hthreshold : first ≤ second) (hsmall : { arity := inst.arity, samples := inst.samples, threshold := first }.HasCircuitAtMost) : { arity := inst.arity, samples := inst.samples, threshold := second }.HasCircuitAtMost

Increasing the size threshold preserves sampled yes-instances.

@[simp]

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

A canonical sampled-instance code belongs to SuccinctMCSP exactly when its typed instance has a matching circuit within the threshold.

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

Every malformed sampled-instance code is rejected.

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

Membership exposes the unique decoded sampled instance and its exact typed feasibility predicate.