Absorbing aggregate budgets in a circuit lower bound

This numerical layer takes the density-preserving slice and its accepting-input bound as explicit hypotheses. Sublinear aggregate budgets and rectangle thresholds preserve the leading coefficient of the underlying graph-ordering bound.

theorem Algebraic.Cutwidth.Aggregate.log_bound_of_count {A η C N : ℝ} (hAη : 0 ≤ A + η) (hC : 0 ≤ C) (hN : 1 ≤ N) {m g D K : ℕ} (hK : 0 < K) (hcount : 2 ^ (↑m - 2) ≤ (N * 2 ^ ((A + η) * max (↑g - ↑m) 0 + 3 * Real.logb 2 N + C + 3) + 1) * 2 ^ (↑D + 1) * ↑K ^ 2) : ↑m ≤ (A + η) * max (↑g - ↑m) 0 + 4 * Real.logb 2 N + C + ↑D + 2 * Real.logb 2 ↑K + 7

Taking logarithms of the finite aggregate-count bound costs seven constant bits.

def Algebraic.Cutwidth.Aggregate.SliceBound (A η C : ℝ) (n g D K : ℕ) : Prop

The finite slice information needed by the asymptotic numerical argument.

Equations

• One or more equations did not get rendered due to their size.

theorem Algebraic.Cutwidth.Aggregate.SliceBound.mono_budget {A η C : ℝ} {n g D D' K : ℕ} (h : SliceBound A η C n g D K) (hD : D ≤ D') : SliceBound A η C n g D' K

Increasing the allowed aggregate budget preserves the finite slice bound.

theorem Algebraic.Cutwidth.Aggregate.lt_size_of_sliceBound {A η θ C : ℝ} (hA : 0 < A) (hη : 0 ≤ η) (hηθ : η ≤ A ^ 2 * θ / 2) (hθ : 0 ≤ θ) (hθA : θ ≤ 1 / A) (hC : 0 ≤ C) {n g D K : ℕ} (hK : 1 < K) (hslice : SliceBound A η C n g D K) (hlog : (A + η + 2) * ↑D + (A + η + 3) * Real.logb 2 ↑K + 4 * Real.logb 2 ↑n + (4 * Real.logb 2 (4 + 3 / A) + C + 4 * (A + η) + 11) < A * θ / 2 * ↑n) : (1 + 1 / A - θ) * ↑n < ↑g

A positive linear slack absorbs the explicit logarithmic and aggregate remainders.

theorem Algebraic.Cutwidth.Aggregate.eventually_lt_size_of_sliceBound {A : ℝ} (hA : 0 < A) (Good : ℕ → ℕ → Prop) (D K : ℕ → ℕ) (hD : (fun (n : ℕ) => ↑(D n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) (hK : (fun (n : ℕ) => Real.logb 2 ↑(K n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) (hKtwo : ∀ᶠ (n : ℕ) in Filter.atTop, 1 < K n) (hslices : ∀ (η : ℝ), 0 < η → ∃ (C : ℝ), 0 ≤ C ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (g : ℕ), Good n g → SliceBound A η C n g (D n) (K n)) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (g : ℕ), Good n g → (1 + 1 / A - ε) * ↑n < ↑g

Any family of circuit sizes admitting the finite slice estimate at every positive ordering slack has leading coefficient 1 + 1/A when its aggregate budget and logarithmic rectangle threshold are sublinear.