Shannon bounds for canonical MCSP

The classical circuit-counting frontier is exposed directly through canonical MCSP codes. At arity at least six, some truth table is rejected at threshold 2^n / (5n). At arity at least sixteen, every truth table is accepted at threshold 18 * 2^n / n.

These are finite statements in the library's exact fan-in-two circuit model; they do not assert hardness of deciding MCSP.

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

At every arity at least six, some canonical truth table has minimum circuit size strictly above the Shannon lower threshold.

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

The Shannon lower bound gives an actual canonical MCSP no-instance at its explicit threshold.

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

Equivalently, a Boolean function packaged by the canonical truth-table constructor is rejected at the Shannon lower threshold.

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

Every canonical MCSP instance whose threshold reaches the explicit Shannon upper bound is a yes-instance.

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

Packaging any Boolean function at the Shannon upper threshold produces a canonical MCSP yes-instance.

theorem Complexity.MCSP.shannon_threshold_window (arity : ℕ) (harity : 16 ≤ arity) : (∃ (f : BitString arity → Bool), (Instance.ofFunction arity (2 ^ arity / (5 * arity)) f).encode ∉ MCSP) ∧ ∀ (f : BitString arity → Bool), (Instance.ofFunction arity (18 * 2 ^ arity / arity) f).encode ∈ MCSP

The exact finite Shannon window for canonical MCSP: at the lower threshold some truth table is rejected, while at the upper threshold every truth table is accepted. The two constants and the truth-table arity remain explicit.