Internal: Shannon bridge from descriptors to typed circuits

This module pads the descriptor of a typed single-output circuit to the fixed size used by the Shannon counting argument and transfers the resulting lower bound back to Circuit.

theorem Complexity.shannon_lower_bound_circuit_internal (N : ℕ) [NeZero N] (hN : 6 ≤ N) : ∃ (f : BitString N → Bool), ∀ (G : ℕ) (c : Circuit Basis.andOr2 N 1 G), G + 1 ≤ 2 ^ N / (5 * N) → (fun (x : BitString N) => c.eval x 0) ≠ f

Internal Shannon lower bound transported to typed circuits.