Bridges to the cutwidth development

This module is maintained in the library; scripts/sync_frontier.py mirrors the rest of Complexitylib/Circuits/Frontier/ from the frontier-method development and leaves it alone. It connects the frontier method to the Boolean cutwidth development of Algebraic.LowerBound.Cutwidth:

• LayoutBound.of_orderingBound: the ordering hypothesis Algebraic.Cutwidth.Multigraph.OrderingBound A η C at every slack gives LayoutBound 3 A. Numbering the vertices in the given order gives a layout, (|E| - |V|)⁺ is at most the cycle rank, and 3 log₂ |V| ≤ η |V| + K. Every ordering coefficient proved for the cutwidth development therefore transfers; layoutBound_of_orderingBound_frontier recovers layoutBound_gaussian this way.
• gaussianCoefficient_eq_frontierCoefficient: the two developments' Gaussian coefficients are the same number.
• rectangleFree_setOf: Boolean rectangle-freeness of a function is rectangle-freeness of its accepted set.
• flatSumsetBias_of_flatSumsetExtractor: a flat-source sumset extractor with error ν has signed sumset bias 2 ν.

theorem Complexity.Frontier.LayoutBound.of_orderingBound {A : ℝ} (hA : 0 ≤ A) (h : ∀ (η : ℝ), 0 < η → ∃ (C : ℝ), Algebraic.Cutwidth.Multigraph.OrderingBound A η C) : LayoutBound 3 A

From vertex orderings to layouts. The ordering hypothesis of the cutwidth development at every positive slack gives the layout hypothesis for maximum degree three, with the same coefficient.

theorem Complexity.Frontier.gaussianCoefficient_eq_frontierCoefficient : Gaussian.gaussianCoefficient = Algebraic.Cutwidth.Gaussian.frontierCoefficient

The Gaussian coefficient of the frontier method is the frontier coefficient of the cutwidth development: both are (3/(2π)) arccos ((1 + 2√2)/4).

theorem Complexity.Frontier.layoutBound_of_orderingBound_frontier : LayoutBound 3 (2 * Gaussian.gaussianCoefficient)

The cutwidth development's Gaussian ordering bound, transferred, gives the same layout coefficient as layoutBound_gaussian.

theorem Complexity.Frontier.rectangleFree_setOf {n K : ℕ} {f : Cslib.BooleanFunction n} (h : Algebraic.Cutwidth.RectangleFree f K) : RectangleFree {x : Fin n → Bool | f x = true} K

Boolean rectangle-freeness. A Boolean function that is K-rectangle-free in the sense of the cutwidth development accepts a K-rectangle-free set.

theorem Complexity.Frontier.ncard_setOf_eq_card_accepting {n : ℕ} (f : Cslib.BooleanFunction n) : {x : Cslib.BitString n | f x = true}.ncard = (Algebraic.Cutwidth.accepting f).card

The accepted set of a Boolean function has as many elements as its accepting inputs.

theorem Complexity.Frontier.flatSumsetBias_of_flatSumsetExtractor {n K : ℕ} {f : Cslib.BooleanFunction n} {ν : ℝ} (h : Algebraic.Cutwidth.FlatSumsetExtractor f K ν) : FlatSumsetBias f K (2 * ν)

Extractors have small signed sumset bias. A flat-source sumset extractor with error ν has signed sumset bias 2 ν.