Sparse synthesis and square-root continuity of circuit complexity

For 2 * p input bits and at most 2 ^ p exceptional inputs, support indicators cost at most (1 + ε) * 2 ^ p, and arbitrary scalar labels on the support cost at most (1 + ε) * 2 ^ p / p, uniformly for all large p. Correcting at most 2 * p output coordinates therefore changes the minimum De Morgan circuit size by at most (3 + ε) * 2 ^ p.

The circuit model is CSLib's: every AND, OR, NOT, and constant gate is counted; fan-out and designation of output wires are free. The underlying synthesis methods are classical. The formalization specializes shared pattern tables, partial extensions, and affine hashing to this exponential support regime. It does not assume a general vector-valued entropy synthesis theorem.

References

• A. V. Chashkin, On computing partial Boolean functions (in Russian), Mathematical Problems of Cybernetics 22 (2024), pp. 152–222, Sections 2–3: https://doi.org/10.20948/mvk-2024-152. The survey credits L. A. Sholomov for partial synthesis and O. B. Lupanov for bounded-weight synthesis. The finite budgets here use a direct specialization of those methods with polynomial auxiliary costs.

theorem Complexity.CircuitSparseSynthesis.complexity_indicator_le (ε : ℝ) (positive : 0 < ε) : ∃ (p₀ : ℕ), ∀ p ≥ p₀, ∀ (domain : Finset (Fin (2 * p) → Bool)), domain.card ≤ 2 ^ p → ↑(Cslib.Circuits.complexity Cslib.Circuits.Boolean.interpretation (Cslib.Circuits.Boolean.Correction.indicator ↑domain)) ≤ (1 + ε) * 2 ^ p

A uniform square-root-weight synthesis bound in the native De Morgan model.

theorem Complexity.CircuitSparseSynthesis.complexityOn_le (ε : ℝ) (positive : 0 < ε) : ∃ (p₀ : ℕ), ∀ p ≥ p₀, ∀ (domain : Finset (Fin (2 * p) → Bool)), domain.card ≤ 2 ^ p → ∀ (f : (Fin (2 * p) → Bool) → Bool), ↑(Cslib.Circuits.complexityOn Cslib.Circuits.Boolean.interpretation ↑domain fun (x : Fin (2 * p) → Bool) (x_1 : Fin 1) => f x) ≤ (1 + ε) * 2 ^ p / ↑p

Prescribed scalar values on a square-root-sized domain admit a shared partial circuit.

theorem Complexity.CircuitSparseSynthesis.complexity_dist_le_three_sqrt_of_cover (ε : ℝ) (positive : 0 < ε) : ∃ (p₀ : ℕ), ∀ p ≥ p₀, ∀ (m : ℕ) (f g : (Fin (2 * p) → Bool) → Fin m → Bool) (domain : Finset (Fin (2 * p) → Bool)) (outputs : Finset (Fin m)), domain.card ≤ 2 ^ p → outputs.card ≤ 2 * p → (∀ x ∉ domain, f x = g x) → (∀ j ∉ outputs, ∀ (x : Fin (2 * p) → Bool), f x j = g x j) → ↑((Cslib.Circuits.complexity Cslib.Circuits.Boolean.interpretation f).dist (Cslib.Circuits.complexity Cslib.Circuits.Boolean.interpretation g)) ≤ (3 + ε) * 2 ^ p

Uniform vector correction: at most 2 ^ p error rows and 2 * p changed coordinates.

theorem Complexity.CircuitSparseSynthesis.complexity_dist_le_three_sqrt (ε : ℝ) (positive : 0 < ε) : ∃ (p₀ : ℕ), ∀ p ≥ p₀, ∀ (m : ℕ) (f g : (Fin (2 * p) → Bool) → Fin m → Bool), Cslib.Circuits.Boolean.Correction.rowDistance f g ≤ 2 ^ p → (Cslib.Circuits.Boolean.Correction.activeOutputs f g).card ≤ 2 * p → ↑((Cslib.Circuits.complexity Cslib.Circuits.Boolean.interpretation f).dist (Cslib.Circuits.complexity Cslib.Circuits.Boolean.interpretation g)) ≤ (3 + ε) * 2 ^ p

Square-root continuity, stated using the actual erroneous rows and active outputs.