Polynomial circuit size hierarchy

For arbitrary real exponents 1 ≤ a < b, nonuniform SIZE(n^a) is a strict subset of SIZE(n^b). These classes allow multiplicative constants and finitely many exceptional widths. Floors convert real powers to natural gate budgets; mem_polynomialSize_iff gives the usual real-valued formulation.

The proof first establishes the exact finite interpolation theorem, then absorbs its 2 * n overhead in the gap between distinct real powers. It asserts existence of nonuniform function families, without a uniform circuit construction or an explicit hard function.

noncomputable def Algebraic.DeMorgan.polynomialBudget (degree : ℝ) (n : ℕ) : ℕ

Natural gate budget obtained by flooring a real power of the input width.

Equations

• Algebraic.DeMorgan.polynomialBudget degree n = ⌊↑n ^ degree⌋₊

@[simp]

theorem Algebraic.DeMorgan.polynomialBudget_natCast (degree : ℕ) : polynomialBudget ↑degree = fun (n : ℕ) => n ^ degree

Natural exponents recover ordinary natural-power budgets exactly.

def Algebraic.DeMorgan.polynomialSize (degree : ℝ) : Set FunctionFamily

The nonuniform class SIZE(n^degree), including constant factors.

Equations

• Algebraic.DeMorgan.polynomialSize degree = Algebraic.DeMorgan.sizeClass (Algebraic.DeMorgan.polynomialBudget degree)

theorem Algebraic.DeMorgan.mem_polynomialSize_iff (family : FunctionFamily) {degree : ℝ} (nonnegative : 0 ≤ degree) : family ∈ polynomialSize degree ↔ ∃ (constant : ℝ), ∀ᶠ (n : ℕ) in Filter.atTop, ↑(complexity (family n)) ≤ constant * ↑n ^ degree

The floored definition agrees with the usual real-valued O(n^degree) bound, for every nonnegative real degree.

theorem Algebraic.DeMorgan.polynomialBudget_eventually_le_shannon (degree : ℝ) : ∀ᶠ (n : ℕ) in Filter.atTop, polynomialBudget degree n ≤ 2 ^ n / n

Every fixed real power is eventually below the Shannon gate budget.

theorem Algebraic.DeMorgan.polynomialBudget_gap {a b : ℝ} (linear : 1 ≤ a) (separated : a < b) (constant : ℕ) : ∀ᶠ (n : ℕ) in Filter.atTop, constant * polynomialBudget a n + 2 * n + 1 ≤ polynomialBudget b n

The gap between distinct real powers above the linear scale absorbs the exact 2 * n interpolation overhead and every fixed lower-size coefficient.

theorem Algebraic.DeMorgan.polynomialSize_ssubset {a b : ℝ} (linear : 1 ≤ a) (separated : a < b) : polynomialSize a ⊂ polynomialSize b

Circuit size hierarchy for arbitrary real polynomial exponents: SIZE(n^a) is strictly contained in SIZE(n^b) whenever 1 ≤ a < b.

theorem Algebraic.DeMorgan.sizeClass_pow_ssubset {a b : ℕ} (linear : 1 ≤ a) (separated : a < b) : (sizeClass fun (n : ℕ) => n ^ a) ⊂ sizeClass fun (n : ℕ) => n ^ b

Natural-power specialization of the circuit size hierarchy.