The frontier method for the explicit hard family

The cutwidth development constructs one uniformly polynomial-time Boolean family, Algebraic.Cutwidth.Extractor.sourceReductionHardFamily: balanced padding of a flat-source sumset extractor with sublinear entropy. Its accepted sets satisfy the three hypotheses of the frontier method (sourceReductionHardFamily_frontierHypotheses): they are rectangle-free with a threshold of logarithm o(n), and they accept exactly half of the cube.

So every general lower bound of Complexity.Frontier applies to this explicit family:

• sourceReductionHardFamily_lt_innerSize_gaussian: every circuit of fan-in two, over any basis and with any accepting set, has more than (L - ε) n gates of positive arity, L = 1 + π/(3 arccos ((1 + 2√2)/4)) ≈ 4.5625. Constant gates are free.
• sourceReductionHardFamily_lt_innerSize_degree: for every fan-in r ≥ 2, (r - 1) s > (1 + 1/A_(r+1) - ε) n with the Gaussian degree coefficient A_d = 3d/(2d-3) · arccos(2√(d-1)/d)/π < 3/4; in particular more than (7/4 - ε) n gates at fan-in three (sourceReductionHardFamily_lt_innerSize_fanInThree), and the simpler spanning-tree bound (r - 1) s > (2 - ε) n (sourceReductionHardFamily_lt_innerSize_all_fanIn).
• sourceReductionHardFamily_lt_innerSize_nondeterministic: the Gaussian coefficient for verifier circuits over any basis, uniformly in the number of witness inputs.
• sourceReductionHardFamily_lt_innerGates_aggregate: the Gaussian coefficient with sublinearly many monoid-aggregate gates of unbounded fan-in, which are not counted.

The unpadded extractor Algebraic.Cutwidth.Extractor.sourceReductionFamily, which is also uniformly polynomial-time computable, has signed sumset bias 2 · 35/72 (flatSumsetBias_of_flatSumsetExtractor in Frontier.Cutwidth). The weighted frontier bound then gives explicit average-case hardness (sourceReductionFamily_agreement_le): every circuit of fan-in two over any basis with at most (L - ε) n gates of positive arity agrees with it on at most a 71/72 + 2^(-γ n) fraction of inputs.

The cutwidth development proves the first bound for the full binary basis, counting every gate (Algebraic.Cutwidth.sourceReductionHardFamily_eventually_lt_size_gaussian). rectangleFree_setOf (Frontier.Cutwidth) translates its Boolean rectangle-freeness to the frontier method's. This module is maintained in the library, not mirrored from upstream.

theorem Complexity.Frontier.sourceReductionHardFamily_frontierHypotheses : ∃ (K : ℕ → ℕ), (∀ᶠ (n : ℕ) in Filter.atTop, RectangleFree {x : Fin n → Bool | Algebraic.Cutwidth.Extractor.sourceReductionHardFamily n x = true} (K n)) ∧ ((fun (n : ℕ) => Real.log ↑(K n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) ∧ (fun (n : ℕ) => ↑n * Real.log ↑(Nat.card Bool) - Real.log ↑{x : Fin n → Bool | Algebraic.Cutwidth.Extractor.sourceReductionHardFamily n x = true}.ncard) =o[Filter.atTop] fun (n : ℕ) => ↑n

The explicit family satisfies the hypotheses of the frontier method: its accepted sets are eventually rectangle-free with a threshold of logarithm o(n), and their logarithmic density deficit is o(n) (it is the constant log 2).

theorem Complexity.Frontier.sourceReductionHardFamily_lt_innerSize_gaussian {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (σ : Cslib.Circuits.Signature) (I : Cslib.Circuits.Interpretation σ Bool) (Acc : Set Bool) (c : Cslib.Circuits.Circuit σ n 1), c.FanInAtMost 2 → Decides c I Acc {x : Fin n → Bool | Algebraic.Cutwidth.Extractor.sourceReductionHardFamily n x = true} → (1 + Real.pi / (3 * Real.arccos ((1 + 2 * √2) / 4)) - ε) * ↑n < ↑c.innerSize

The Gaussian bound for the explicit family, over any basis. For every ε > 0 and all large n, every circuit of fan-in at most two deciding the explicit family, over any basis on Bool and with any accepting set, has more than (L - ε) n gates of positive arity, where L = 1 + π/(3 arccos ((1 + 2√2)/4)) ≈ 4.5625.

theorem Complexity.Frontier.sourceReductionHardFamily_lt_innerSize_all_fanIn {ε : ℝ} {r : ℕ} (hr : 2 ≤ r) (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (σ : Cslib.Circuits.Signature) (I : Cslib.Circuits.Interpretation σ Bool) (Acc : Set Bool) (c : Cslib.Circuits.Circuit σ n 1), c.FanInAtMost r → Decides c I Acc {x : Fin n → Bool | Algebraic.Cutwidth.Extractor.sourceReductionHardFamily n x = true} → (2 - ε) * ↑n < (↑r - 1) * ↑c.innerSize

Every fixed fan-in, for the explicit family. For every r ≥ 2, every circuit of fan-in at most r deciding the explicit family, over any basis on Bool, satisfies (r - 1) s > (2 - ε) n, where s counts the gates of positive arity.

theorem Complexity.Frontier.sourceReductionHardFamily_lt_innerSize_degree {ε : ℝ} {r : ℕ} (hr : 2 ≤ r) (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (σ : Cslib.Circuits.Signature) (I : Cslib.Circuits.Interpretation σ Bool) (Acc : Set Bool) (c : Cslib.Circuits.Circuit σ n 1), c.FanInAtMost r → Decides c I Acc {x : Fin n → Bool | Algebraic.Cutwidth.Extractor.sourceReductionHardFamily n x = true} → (1 + 1 / Gaussian.degreeCoefficient (r + 1) - ε) * ↑n < (↑r - 1) * ↑c.innerSize

Every fixed fan-in, with the Gaussian degree coefficient, for the explicit family. For every r ≥ 2, every circuit of fan-in at most r deciding the explicit family, over any basis on Bool, satisfies (r - 1) s > (1 + 1/A_(r+1) - ε) n, where s counts the gates of positive arity and A_d = 3d/(2d-3) · arccos(2√(d-1)/d)/π (Gaussian.degreeCoefficient).

theorem Complexity.Frontier.sourceReductionHardFamily_lt_innerSize_fanInThree {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (σ : Cslib.Circuits.Signature) (I : Cslib.Circuits.Interpretation σ Bool) (Acc : Set Bool) (c : Cslib.Circuits.Circuit σ n 1), c.FanInAtMost 3 → Decides c I Acc {x : Fin n → Bool | Algebraic.Cutwidth.Extractor.sourceReductionHardFamily n x = true} → (7 / 4 - ε) * ↑n < ↑c.innerSize

Ternary gates, for the explicit family. Every circuit of fan-in at most three deciding the explicit family, over any basis on Bool, has more than (7/4 - ε) n gates of positive arity.

theorem Complexity.Frontier.sourceReductionHardFamily_lt_innerSize_nondeterministic {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (k : ℕ) (σ : Cslib.Circuits.Signature) (I : Cslib.Circuits.Interpretation σ Bool) (Acc : Set Bool) (c : Cslib.Circuits.Circuit σ (n + k) 1), c.FanInAtMost 2 → NondeterministicDecides c I Acc {x : Fin n → Bool | Algebraic.Cutwidth.Extractor.sourceReductionHardFamily n x = true} → (1 + Real.pi / (3 * Real.arccos ((1 + 2 * √2) / 4)) - ε) * ↑n < ↑c.innerSize

Verifier circuits for the explicit family. The Gaussian coefficient holds for nondeterministic circuits of fan-in two over any basis on Bool, uniformly in the number k of witness inputs, which are not counted in n.

theorem Complexity.Frontier.sourceReductionHardFamily_lt_innerGates_aggregate {ε : ℝ} {β : ℕ → ℝ} (hβ : β =o[Filter.atTop] fun (n : ℕ) => ↑n) (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (σ : Cslib.Circuits.Signature) (I : Cslib.Circuits.Interpretation σ Bool) (Acc : Set Bool) (c : Cslib.Circuits.Circuit σ n 1) (special : ℕ → Prop) (T : Type) [inst : CommMonoid T] [Finite T], (∀ (g : Fin c.size), ¬special ↑g → σ.Arity (c.program.lines g).op ≤ 2) → (∀ (g : Fin c.size), special ↑g → Aggregates (I (c.program.lines g).op) T) → ↑(Nat.card { g : Fin c.size // special ↑g }) * Real.log ↑(Nat.card T) ≤ β n → Decides c I Acc {x : Fin n → Bool | Algebraic.Cutwidth.Extractor.sourceReductionHardFamily n x = true} → (1 + Real.pi / (3 * Real.arccos ((1 + 2 * √2) / 4)) - ε) * ↑n < ↑(erase special c.program).innerGates.card

Aggregate gates for the explicit family. The Gaussian coefficient holds for circuits over any basis on Bool whose ordinary gates have fan-in at most two and whose special gates of unbounded fan-in aggregate in a finite commutative monoid T, provided the special gates carry o(n) bits of monoid state. Only the ordinary gates of positive arity are counted.

theorem Complexity.Frontier.sourceReductionFamily_agreement_le {ε : ℝ} (hε : 0 < ε) : ∃ (γ : ℝ), 0 < γ ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (σ : Cslib.Circuits.Signature) (I : Cslib.Circuits.Interpretation σ Bool) (c : Cslib.Circuits.Circuit σ n 1), c.FanInAtMost 2 → ↑c.innerSize ≤ (1 + Real.pi / (3 * Real.arccos ((1 + 2 * √2) / 4)) - ε) * ↑n → (agreement (Algebraic.Cutwidth.Extractor.sourceReductionFamily n) fun (x : Fin n → Bool) => c.eval I x 0) ≤ 71 / 72 + 2 ^ (-γ * ↑n)

Average-case hardness of the explicit extractor. For every ε > 0 there is γ > 0 such that for all large n, every circuit of fan-in two, over any basis on Bool, with at most (L - ε) n gates of positive arity agrees with the explicit extractor on at most a 71/72 + 2^(-γ n) fraction of inputs, where L = 1 + π/(3 arccos ((1 + 2√2)/4)) ≈ 4.5625.