Scalar continuity and robustness of circuit hardness

A scalar correction is determined by its support, so its leading constant is one. The vector bound transfers exact lower bounds to circuits making at most square-root-many row errors. Complexity much larger than the correction budget is preserved up to a vanishing relative error, uniformly in the edits.

theorem Complexity.CircuitSparseSynthesis.complexity_dist_le_sqrt (ε : ℝ) (positive : 0 < ε) : ∃ (p₀ : ℕ), ∀ p ≥ p₀, ∀ (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)) ≤ (1 + ε) * 2 ^ p

Scalar square-root continuity has leading constant one.

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

A sufficiently large exact lower bound forces more than 2 ^ p row errors. The output width is at most 2 * p, so every comparison has few active outputs.

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

The same exact-to-approximate transfer with the sharper scalar constant.

theorem Complexity.CircuitSparseSynthesis.complexity_dist_isLittleO {m : ℕ → ℕ} (f g : (p : ℕ) → (Fin (2 * p) → Bool) → Fin (m p) → Bool) (rows : ∀ᶠ (p : ℕ) in Filter.atTop, Cslib.Circuits.Boolean.Correction.rowDistance (f p) (g p) ≤ 2 ^ p) (outputs : ∀ᶠ (p : ℕ) in Filter.atTop, (Cslib.Circuits.Boolean.Correction.activeOutputs (f p) (g p)).card ≤ 2 * p) (hard : (fun (p : ℕ) => 2 ^ p) =o[Filter.atTop] fun (p : ℕ) => ↑(Cslib.Circuits.complexity Cslib.Circuits.Boolean.interpretation (f p))) : (fun (p : ℕ) => ↑((Cslib.Circuits.complexity Cslib.Circuits.Boolean.interpretation (f p)).dist (Cslib.Circuits.complexity Cslib.Circuits.Boolean.interpretation (g p)))) =o[Filter.atTop] fun (p : ℕ) => ↑(Cslib.Circuits.complexity Cslib.Circuits.Boolean.interpretation (f p))

Sparse edits have vanishing relative cost when 2 ^ p = o(C(f p)).