Minimum Circuit Size Problem -- proof internals

This module proves codec exactness and connects the direct existential MCSP semantics to Circuit.sizeComplexity at every positive arity.

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

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

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

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

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

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

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

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

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

Internal characterization of every rejected MCSP code.

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

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

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

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

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

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

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

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