Finite circuit size hierarchy

Shannon counting supplies a hard endpoint, and the truth-table cube supplies intermediate complexities. The finite theorem uses the exact sharp census. The eventual theorem crosses every threshold from 1 through 2^n / n, with additive overshoot at most 2 * n. Complexity counts all internal gates of the De Morgan signature, exactly as in the counting theorem.

theorem Algebraic.DeMorgan.exists_complexity_between_of_sharpBudget {n : ℕ} (threshold : ℕ) (positive : 1 ≤ threshold) (small : signature.sharpBudget n 1 threshold < Target.count Bool n 1) : ∃ (function : ScalarFunction Bool n), threshold < complexity function ∧ complexity function ≤ threshold + 2 * n

Exact finite hierarchy criterion, retaining the factorial-improved Shannon census as the sufficient condition for a hard endpoint.

theorem Algebraic.DeMorgan.eventually_exists_complexity_between : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (threshold : ℕ), 1 ≤ threshold → threshold ≤ 2 ^ n / n → ∃ (function : ScalarFunction Bool n), threshold < complexity function ∧ complexity function ≤ threshold + 2 * n

At every sufficiently large width, all thresholds through the Shannon scale are attained to within an additive 2 * n gates.