Sparse synthesis and the square-root continuity of circuit complexity

Consider Boolean functions on n = 2 p inputs, and sets of at most 2 ^ p inputs, the square root of the number of all inputs. For every ε > 0 and all large p:

• the indicator of such a set has a De Morgan circuit with at most (1 + ε) 2 ^ p gates (complexity_indicator_le), the case N = 2 ^ p of Lupanov's bound for functions with N ones [Lup65], Chashkin, Theorem 3.1;
• every function on such a set agrees there with a De Morgan circuit with at most (1 + ε) 2 ^ p / p gates (complexityOn_le), the case D = 2 ^ p of Sholomov's bound D / log₂ D for functions defined on D inputs [Sho69], Chashkin, Theorem 2.1.

Both bounds are asymptotically optimal Chashkin, Section 1. Chashkin states them for circuits over all binary operations; the constructions spend their leading gates on disjunctions, and the bounds are proved here for De Morgan circuits. The circuits are those of Complexity.Computability.Circuit.Boolean.SparseSynthesisConstruction; this file chooses their parameters, uniformly in the set and the function.

Together with the sparse corrections of Complexity.Computability.Circuit.Boolean.Correction, these bounds show that circuit complexity is continuous at the scale of the square root of the number of inputs: changing a function with any number of outputs on at most 2 ^ p inputs, and in at most 2 p outputs, changes its complexity by at most (3 + ε) 2 ^ p (dist_complexity_le). Indeed the indicator of the changed inputs costs (1 + ε) 2 ^ p, and each of the at most 2 p changed outputs costs (1 + ε) 2 ^ p / p on those inputs. For a single output the bound is (1 + ε) 2 ^ p (dist_complexity_single_le). The order is optimal: for p ≥ 4, by counting, some set of 2 ^ p inputs has an indicator of complexity more than 2 ^ p / 16 (exists_hard_indicator), so no continuity bound is o(2 ^ p) (not_isLittleO_of_dist_complexity_le). Consequences are that exact hardness survives sparse errors (lt_hammingDist_of_complexity_add_lt, dist_complexity_isLittleO), and that circuits of (1 + ε) 2 ^ p / p gates shatter every set of at most 2 ^ p inputs (shatters_circuitSets).

The circuit model counts every AND, OR, NOT and constant gate; fan-out and output wires are free.

Main definitions

• Cslib.Circuits.Boolean.SparseSynthesis.circuitSets: the sets whose indicators have circuits with at most s gates.

Main results

• Cslib.Circuits.Boolean.SparseSynthesis.complexity_indicator_le: sparse indicators.
• Cslib.Circuits.Boolean.SparseSynthesis.complexityOn_le: partial functions.
• Cslib.Circuits.Boolean.SparseSynthesis.dist_complexity_le: square-root continuity.
• Cslib.Circuits.Boolean.SparseSynthesis.dist_complexity_single_le: square-root continuity for a single output.
• Cslib.Circuits.Boolean.SparseSynthesis.exists_hard_indicator, Cslib.Circuits.Boolean.SparseSynthesis.not_isLittleO_of_dist_complexity_le: optimality.
• Cslib.Circuits.Boolean.SparseSynthesis.lt_hammingDist_of_complexity_add_lt, Cslib.Circuits.Boolean.SparseSynthesis.dist_complexity_isLittleO: hardness survives sparse errors.
• Cslib.Circuits.Boolean.SparseSynthesis.shatters_circuitSets, Cslib.Circuits.Boolean.SparseSynthesis.le_vcDim_circuitSets: small circuits shatter square-root-sized samples.

References

• A. V. Chashkin, On computing partial Boolean functions
• O. B. Lupanov, On an approach to the synthesis of control systems: the principle of local coding
• L. A. Sholomov, On the realization of incompletely defined Boolean functions by circuits of functional elements

Estimates

Uniform sparse and partial synthesis

theorem Cslib.Circuits.Boolean.SparseSynthesis.complexity_indicator_le (ε : ℝ) (hε : 0 < ε) : ∃ (p₀ : ℕ), ∀ p ≥ p₀, ∀ (D : Finset (BitString (2 * p))), D.card ≤ 2 ^ p → ↑(complexity interpretation (single fun (x : Fin (2 * p) → Bool) => decide (x ∈ D))) ≤ (1 + ε) * 2 ^ p

Sparse indicators. For every ε > 0 and all large p, the indicator of any set of at most 2 ^ p of the 2 ^ (2 p) inputs has a De Morgan circuit with at most (1 + ε) 2 ^ p gates. This is the case N = 2 ^ p of Lupanov's bound for functions with N ones, which is asymptotically optimal [Lup65], Chashkin, Theorem 3.1.

theorem Cslib.Circuits.Boolean.SparseSynthesis.complexityOn_le (ε : ℝ) (hε : 0 < ε) : ∃ (p₀ : ℕ), ∀ p ≥ p₀, ∀ (D : Finset (BitString (2 * p))), D.card ≤ 2 ^ p → ∀ (u : BooleanFunction (2 * p)), ↑(complexityOn interpretation (↑D) (single u)) ≤ (1 + ε) * 2 ^ p / ↑p

Partial functions. For every ε > 0 and all large p, every Boolean function on any set of at most 2 ^ p of the 2 ^ (2 p) inputs agrees on that set with a De Morgan circuit with at most (1 + ε) 2 ^ p / p gates. This is the case D = 2 ^ p of Sholomov's bound D / log₂ D for functions defined on D inputs, which is asymptotically optimal [Sho69], Chashkin, Theorem 2.1.

Square-root continuity of circuit complexity

theorem Cslib.Circuits.Boolean.SparseSynthesis.dist_complexity_le (ε : ℝ) (hε : 0 < ε) : ∃ (p₀ : ℕ), ∀ p ≥ p₀, ∀ (m : ℕ) (f g : BitString (2 * p) → BitString m), hammingDist f g ≤ 2 ^ p → hammingDist (Function.swap f) (Function.swap g) ≤ 2 * p → ↑((complexity interpretation f).dist (complexity interpretation g)) ≤ (3 + ε) * 2 ^ p

Square-root continuity of circuit complexity. For every ε > 0 and all large p, changing a Boolean function with any number of outputs on at most 2 ^ p of its 2 ^ (2 p) inputs, and in at most 2 p of its outputs, changes its De Morgan circuit complexity by at most (3 + ε) 2 ^ p, where 2 ^ p is the square root of the number of inputs. The changes are corrected by dist_complexity_le_sum_of_cover, with the indicator of the changed inputs computed by complexity_indicator_le and each changed output by complexityOn_le. The order 2 ^ p is optimal by exists_hammingDist_eq_le_dist_complexity.

theorem Cslib.Circuits.Boolean.SparseSynthesis.dist_complexity_single_le (ε : ℝ) (hε : 0 < ε) : ∃ (p₀ : ℕ), ∀ p ≥ p₀, ∀ (f g : BooleanFunction (2 * p)), hammingDist f g ≤ 2 ^ p → ↑((complexity interpretation (single f)).dist (complexity interpretation (single g))) ≤ (1 + ε) * 2 ^ p

Square-root continuity for a single output. For every ε > 0 and all large p, changing a Boolean function on at most 2 ^ p of its 2 ^ (2 p) inputs changes its De Morgan circuit complexity by at most (1 + ε) 2 ^ p.

theorem Cslib.Circuits.Boolean.SparseSynthesis.lt_hammingDist_of_complexity_add_lt (ε : ℝ) (hε : 0 < ε) : ∃ (p₀ : ℕ), ∀ p ≥ p₀, ∀ m ≤ 2 * p, ∀ (f g : BitString (2 * p) → BitString m), ↑(complexity interpretation g) + (3 + ε) * 2 ^ p < ↑(complexity interpretation f) → 2 ^ p < hammingDist f g

Exact hardness survives sparse errors. For every ε > 0 and all large p, if a function f with at most 2 p outputs on 2 p inputs has complexity more than (3 + ε) 2 ^ p above that of g, then f and g differ on more than 2 ^ p inputs.

theorem Cslib.Circuits.Boolean.SparseSynthesis.dist_complexity_isLittleO {m : ℕ → ℕ} (f g : (p : ℕ) → BitString (2 * p) → BitString (m p)) (hrows : ∀ᶠ (p : ℕ) in Filter.atTop, hammingDist (f p) (g p) ≤ 2 ^ p) (hcols : ∀ᶠ (p : ℕ) in Filter.atTop, hammingDist (Function.swap (f p)) (Function.swap (g p)) ≤ 2 * p) (hf : (fun (p : ℕ) => 2 ^ p) =o[Filter.atTop] fun (p : ℕ) => ↑(complexity interpretation (f p))) : (fun (p : ℕ) => ↑((complexity interpretation (f p)).dist (complexity interpretation (g p)))) =o[Filter.atTop] fun (p : ℕ) => ↑(complexity interpretation (f p))

Sparse changes are negligible for hard functions. If f p and g p have 2 p inputs, and eventually differ on at most 2 ^ p inputs and in at most 2 p outputs, and 2 ^ p = o(C(f p)), then |C(f p) - C(g p)| = o(C(f p)).

Optimality

theorem Cslib.Circuits.Boolean.SparseSynthesis.exists_hard_indicator {p : ℕ} (hp : 4 ≤ p) : ∃ (D : Finset (BitString (2 * p))), D.card = 2 ^ p ∧ 2 ^ (p - 4) < complexity interpretation (single fun (x : Fin (2 * p) → Bool) => decide (x ∈ D))

Hard sparse indicators. For p ≥ 4, the indicator of some set of exactly 2 ^ p of the 2 ^ (2 p) inputs has complexity more than 2 ^ p / 16. By counting, as in Shannon's lower bound: there are more sets of this size than functions with small circuits.

theorem Cslib.Circuits.Boolean.SparseSynthesis.exists_hammingDist_eq_le_dist_complexity {p : ℕ} (hp : 4 ≤ p) : ∃ (f : BooleanFunction (2 * p)), (hammingDist f fun (x : BitString (2 * p)) => false) = 2 ^ p ∧ 2 ^ p ≤ 16 * (complexity interpretation (single f)).dist (complexity interpretation (single fun (x : BitString (2 * p)) => false))

Square-root continuity is optimal. For p ≥ 4, some function on 2 p inputs differs from the constant false on exactly 2 ^ p inputs, and its complexity differs from that of the constant by at least 2 ^ p / 16.

theorem Cslib.Circuits.Boolean.SparseSynthesis.not_isLittleO_of_dist_complexity_le (b : ℕ → ℝ) (hb : ∀ᶠ (p : ℕ) in Filter.atTop, ∀ (f g : BooleanFunction (2 * p)), hammingDist f g ≤ 2 ^ p → ↑((complexity interpretation (single f)).dist (complexity interpretation (single g))) ≤ b p) : ¬b =o[Filter.atTop] fun (p : ℕ) => 2 ^ p

No sparse continuity bound is o(2 ^ p). If b p eventually bounds the change in complexity of every function on 2 p inputs changed on at most 2 ^ p inputs, then b is not o(2 ^ p).

Shattering

noncomputable def Cslib.Circuits.Boolean.SparseSynthesis.circuitSets (n s : ℕ) : Finset (Finset (BitString n))

The sets of inputs on n bits whose indicators have De Morgan circuits with at most s gates, the supports of computableFunctions n s: the concept class of circuits of size s.

@[simp]

theorem Cslib.Circuits.Boolean.SparseSynthesis.mem_circuitSets {n s : ℕ} {T : Finset (BitString n)} : T ∈ circuitSets n s ↔ ∃ (c : Circuit signature n 1), c.Computes interpretation (single fun (x : Fin n → Bool) => decide (x ∈ T)) ∧ c.size ≤ s

A set is in the concept class of circuits of size s exactly when a circuit with at most s gates computes its indicator.

theorem Cslib.Circuits.Boolean.SparseSynthesis.shatters_circuitSets (ε : ℝ) (hε : 0 < ε) : ∃ (p₀ : ℕ), ∀ p ≥ p₀, ∀ (D : Finset (BitString (2 * p))), D.card ≤ 2 ^ p → (circuitSets (2 * p) ⌊(1 + ε) * 2 ^ p / ↑p⌋₊).Shatters D

Circuits shatter square-root-sized samples. For every ε > 0 and all large p, the sets with circuits of (1 + ε) 2 ^ p / p gates shatter every set of at most 2 ^ p of the 2 ^ (2 p) inputs: every subset of the sample is cut out by such a circuit.

theorem Cslib.Circuits.Boolean.SparseSynthesis.le_vcDim_circuitSets (ε : ℝ) (hε : 0 < ε) : ∃ (p₀ : ℕ), ∀ p ≥ p₀, 2 ^ p ≤ (circuitSets (2 * p) ⌊(1 + ε) * 2 ^ p / ↑p⌋₊).vcDim

The VC dimension of small circuits. For every ε > 0 and all large p, circuits with (1 + ε) 2 ^ p / p gates on 2 p inputs have VC dimension at least 2 ^ p.