Succinct MCSP -- proof internals

This module proves exactness of the nested sampled-instance codec and the basic semantic facts used by the public SuccinctMCSP interface.

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

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

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

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

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

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

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

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

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

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

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

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

theorem Complexity.SuccinctMCSP.Instance.length_encode_internal (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

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

theorem Complexity.SuccinctMCSP.Instance.hasCircuitAtMost_iff_exists_circuit_internal (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

theorem Complexity.SuccinctMCSP.Instance.hasCircuitAtMost_threshold_mono_internal (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