Shannon bounds for canonical MCSP -- proof internals

This module transports the library's exact Shannon circuit bounds to the canonical MCSP truth-table encoding.

theorem Complexity.MCSP.exists_minimumSize_gt_shannonLower_internal (arity : ℕ) (harity : 6 ≤ arity) : ∃ (inst : Instance), inst.arity = arity ∧ inst.threshold = 2 ^ arity / (5 * arity) ∧ inst.minimumSize > 2 ^ arity / (5 * arity)

theorem Complexity.MCSP.exists_not_mem_at_shannonLower_internal (arity : ℕ) (harity : 6 ≤ arity) : ∃ (inst : Instance), inst.arity = arity ∧ inst.threshold = 2 ^ arity / (5 * arity) ∧ inst.encode ∉ MCSP

theorem Complexity.MCSP.exists_ofFunction_not_mem_at_shannonLower_internal (arity : ℕ) (harity : 6 ≤ arity) : ∃ (f : BitString arity → Bool), (Instance.ofFunction arity (2 ^ arity / (5 * arity)) f).encode ∉ MCSP

theorem Complexity.MCSP.mem_encode_of_shannonUpper_le_threshold_internal (inst : Instance) (harity : 16 ≤ inst.arity) (hthreshold : 18 * 2 ^ inst.arity / inst.arity ≤ inst.threshold) : inst.encode ∈ MCSP

theorem Complexity.MCSP.ofFunction_mem_at_shannonUpper_internal (arity : ℕ) (harity : 16 ≤ arity) (f : BitString arity → Bool) : (Instance.ofFunction arity (18 * 2 ^ arity / arity) f).encode ∈ MCSP