Uniform synthesis and relative-complexity estimates

The thresholds depend only on the accuracy parameter. They are uniform in the support, its prescribed labels, and the number of untouched outputs.

theorem Complexity.CircuitSparseSynthesis.Internal.eventually_scalar_complexities (P : ℕ) : ∀ᶠ (p : ℕ) in Filter.atTop, ∀ (domain : Finset (BitString (2 * p))), domain.card ≤ 2 ^ p → P * Cslib.Circuits.complexity Cslib.Circuits.Boolean.interpretation (Cslib.Circuits.Boolean.Correction.indicator ↑domain) ≤ (P + 1) * 2 ^ p ∧ ∀ (f : BitString (2 * p) → Bool), (P * p * Cslib.Circuits.complexityOn Cslib.Circuits.Boolean.interpretation ↑domain fun (x : Fin (2 * p) → Bool) (x_1 : Fin 1) => f x) ≤ (P + 1) * 2 ^ p

theorem Complexity.CircuitSparseSynthesis.Internal.eventually_scalar_correction_nat (P : ℕ) : ∀ᶠ (p : ℕ) in Filter.atTop, ∀ (f g : BitString (2 * p) → Fin 1 → Bool), Cslib.Circuits.Boolean.Correction.rowDistance f g ≤ 2 ^ p → P * (Cslib.Circuits.complexity Cslib.Circuits.Boolean.interpretation f).dist (Cslib.Circuits.complexity Cslib.Circuits.Boolean.interpretation g) ≤ (P + 2) * 2 ^ p

theorem Complexity.CircuitSparseSynthesis.Internal.eventually_correction_nat (P : ℕ) : ∀ᶠ (p : ℕ) in Filter.atTop, ∀ (m : ℕ) (f g : BitString (2 * p) → Fin m → Bool) (domain : Finset (BitString (2 * p))) (outputs : Finset (Fin m)), domain.card ≤ 2 ^ p → outputs.card ≤ 2 * p → (∀ x ∉ domain, f x = g x) → (∀ j ∉ outputs, ∀ (x : BitString (2 * p)), f x j = g x j) → P * (Cslib.Circuits.complexity Cslib.Circuits.Boolean.interpretation f).dist (Cslib.Circuits.complexity Cslib.Circuits.Boolean.interpretation g) ≤ (3 * P + 4) * 2 ^ p