Optimal order of square-root continuity

Shannon's circuit-counting argument applied to sparse graph indicators gives a finite lower bound with constant 1 / 16. In particular, no bound uniform over all square-root-sized corrections can be little-o of the square root of the truth-table length. The witnesses are nonconstructive scalar functions.

theorem Complexity.CircuitSparseSynthesis.exists_sparse_complexity_gt {p : ℕ} (large : 4 ≤ p) : ∃ (domain : Finset (Fin (2 * p) → Bool)), domain.card = 2 ^ p ∧ 2 ^ (p - 4) < Cslib.Circuits.complexity Cslib.Circuits.Boolean.interpretation (Cslib.Circuits.Boolean.Correction.indicator ↑domain)

Some support of exactly 2 ^ p points needs more than 2 ^ (p - 4) gates.

theorem Complexity.CircuitSparseSynthesis.exists_rowDistance_eq_complexity_dist_ge {p : ℕ} (large : 4 ≤ p) : ∃ (f : (Fin (2 * p) → Bool) → Fin 1 → Bool), (Cslib.Circuits.Boolean.Correction.rowDistance f fun (x : Fin (2 * p) → Bool) (x_1 : Fin 1) => false) = 2 ^ p ∧ 2 ^ p ≤ 16 * (Cslib.Circuits.complexity Cslib.Circuits.Boolean.interpretation f).dist (Cslib.Circuits.complexity Cslib.Circuits.Boolean.interpretation fun (x : Fin (2 * p) → Bool) (x_1 : Fin 1) => false)

A square-root-sized edit of zero can change complexity by at least 2 ^ p / 16.

theorem Complexity.CircuitSparseSynthesis.not_isLittleO_of_uniform_correction_bound (bound : ℕ → ℝ) (uniform : ∀ᶠ (p : ℕ) in Filter.atTop, ∀ (f g : (Fin (2 * p) → Bool) → Fin 1 → Bool), Cslib.Circuits.Boolean.Correction.rowDistance f g ≤ 2 ^ p → ↑((Cslib.Circuits.complexity Cslib.Circuits.Boolean.interpretation f).dist (Cslib.Circuits.complexity Cslib.Circuits.Boolean.interpretation g)) ≤ bound p) : ¬bound =o[Filter.atTop] fun (p : ℕ) => 2 ^ p

No uniform scalar correction bound in this regime is little-o of 2 ^ p.