Circuit lower bounds from Gaussian layouts

Two Gaussian constructions improve the graph-ordering coefficient 1/3 of the cubic pathwidth bound. The score layout (Gaussian.Layout) proves the cubic cutwidth bound with coefficient c = (3/π)(3 - 2√2) ≈ 0.16384, giving the ordering coefficient 2c ≈ 0.32768 ≤ 20/61. The edge-score decomposition (Gaussian.Frontier) proves the cubic pathwidth bound with coefficient p = (3/(2π)) arccos ((1 + 2√2)/4) ≈ 0.14035, giving the ordering coefficient 2p ≈ 0.28070 ≤ 9/32. The counting argument then gives circuit lower bounds with coefficient 1 + 1/(2p) = 1 + π/(3 arccos((1 + 2√2)/4)) ≈ 4.5625 for every dense rectangle-free family whose threshold satisfies log₂ K = o(n), for deterministic and nondeterministic circuits.

Conditionally on subcritical band clusters of the edge-score field (Gaussian.BandSubcritical, an open percolation hypothesis), the band-jump decomposition (Gaussian.Band) multiplies the pathwidth coefficient p by exp (-w²/2) for a median band [-w, w) of edge scores. At w = 4/25 the ordering coefficient 2 exp (-w²/2) p is at most 5/18, giving the circuit coefficient 23/5 under that hypothesis.

theorem Algebraic.Cutwidth.Multigraph.exists_orderingBound_gaussian (η : ℝ) : 0 < η → ∃ (C : ℝ), OrderingBound (2 * Gaussian.cutwidthCoefficient) η C

The Gaussian graph-ordering bound. The ordering hypothesis holds with coefficient (6/π)(3 - 2√2) for every positive slack.

theorem Algebraic.Cutwidth.Multigraph.exists_orderingBound_twenty_div_sixtyOne (η : ℝ) : 0 < η → ∃ (C : ℝ), OrderingBound (20 / 61) η C

A rational ordering coefficient below 1/3. The ordering hypothesis holds with coefficient 20/61 for every positive slack.

theorem Algebraic.Cutwidth.Multigraph.exists_orderingBound_frontier (η : ℝ) : 0 < η → ∃ (C : ℝ), OrderingBound (2 * Gaussian.frontierCoefficient) η C

The edge-score graph-ordering bound. The ordering hypothesis holds with coefficient (3/π) arccos ((1 + 2√2)/4) for every positive slack.

theorem Algebraic.Cutwidth.Multigraph.exists_orderingBound_nine_div_thirtyTwo (η : ℝ) : 0 < η → ∃ (C : ℝ), OrderingBound (9 / 32) η C

The ordering coefficient 9/32. The ordering hypothesis holds with coefficient 9/32 for every positive slack.

theorem Algebraic.Cutwidth.Multigraph.exists_orderingBound_band {c : ℝ} (hc : 0 < c) (hband : ∀ (q : ℝ) (R : ℕ), 0 ≤ q → 2 * q ^ 2 < 1 → Gaussian.BandSubcritical q R c) (η : ℝ) : 0 < η → ∃ (C : ℝ), OrderingBound (2 * (Real.exp (-c ^ 2 / 2) * Gaussian.frontierCoefficient)) η C

The band-jump graph-ordering bound (conditional on Gaussian.BandSubcritical). If the band clusters of the edge-score field are subcritical for every decay rate q < 1/√2 and radius R, the ordering hypothesis holds with coefficient 2 exp (-c²/2) (3/(2π)) arccos ((1 + 2√2)/4) for every positive slack.

theorem Algebraic.Cutwidth.Multigraph.exists_orderingBound_five_div_eighteen_of_bandSubcritical (hband : ∀ (q : ℝ) (R : ℕ), 0 ≤ q → 2 * q ^ 2 < 1 → Gaussian.BandSubcritical q R (4 / 25)) (η : ℝ) : 0 < η → ∃ (C : ℝ), OrderingBound (5 / 18) η C

The ordering coefficient 5/18 (conditional on Gaussian.BandSubcritical at c = 4/25). The ordering hypothesis holds with coefficient 5/18 for every positive slack.

theorem Algebraic.Cutwidth.eventually_lt_size_of_rectangleFree_gaussian (f : (n : ℕ) → Cslib.BooleanFunction n) (K : ℕ → ℕ) (hK : (fun (n : ℕ) => Real.logb 2 ↑(K n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) (hacc : ∀ᶠ (n : ℕ) in Filter.atTop, 2 ^ (n - 2) ≤ (accepting (f n)).card) (hrect : ∀ᶠ (n : ℕ) in Filter.atTop, RectangleFree (f n) (K n)) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (circuit : Circuit Binary.signature n 1), (circuit.Computes Binary.interpretation fun (x : Fin n → Bool) (x_1 : Fin 1) => f n x) → (1 + Real.pi / (3 * Real.arccos ((1 + 2 * √2) / 4)) - ε) * ↑n < ↑circuit.size

Gaussian circuit bound. A family with at least 2 ^ (n - 2) accepting inputs that is K n-rectangle-free with log₂ K = o(n) needs more than (1 + π/(3 arccos((1 + 2√2)/4)) - ε) n binary gates for all large n.

theorem Algebraic.Cutwidth.nondet_eventually_lt_size_of_rectangleFree_gaussian (f : (n : ℕ) → Cslib.BooleanFunction n) (K : ℕ → ℕ) (hK : (fun (n : ℕ) => Real.logb 2 ↑(K n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) (hacc : ∀ᶠ (n : ℕ) in Filter.atTop, 2 ^ (n - 2) ≤ (accepting (f n)).card) (hrect : ∀ᶠ (n : ℕ) in Filter.atTop, RectangleFree (f n) (K n)) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (m : ℕ) (circuit : Circuit Binary.signature (n + m) 1), NondetComputes circuit (f n) → (1 + Real.pi / (3 * Real.arccos ((1 + 2 * √2) / 4)) - ε) * ↑n < ↑circuit.size

Gaussian bound for nondeterministic circuits. Under the same hypotheses, every nondeterministic circuit with any number of witness inputs needs more than (1 + π/(3 arccos((1 + 2√2)/4)) - ε) n gates, counting n ordinary inputs.