Relative circuit complexity under sparse corrections

A correction consists of a support indicator and a partial vector of error labels. Its cost is their joint synthesis cost plus five gates per active output: one mask and a four-gate XOR. Output wires and fan-out are free.

These are finite composition theorems. Sharp estimates for sparse indicators and partial scalar functions are separate synthesis results, treated by A. V. Chashkin, On computing partial Boolean functions (in Russian), Mathematical Problems of Cybernetics 22 (2024), pp. 152–222, https://doi.org/10.20948/mvk-2024-152.

theorem Cslib.Circuits.Boolean.Correction.complexity_dist_le_indicator {n : ℕ} (f g : (Fin n → Bool) → Fin 1 → Bool) : (complexity interpretation f).dist (complexity interpretation g) ≤ complexity interpretation (indicator (errorSupport f g)) + 4

A scalar correction is its support indicator; applying it costs four XOR gates.

theorem Cslib.Circuits.Boolean.Correction.complexityGiven_le_of_cover {n m : ℕ} (f g : (Fin n → Bool) → Fin m → Bool) (s : Set (Fin n → Bool)) (outputs : Finset (Fin m)) (outside : ∀ x ∉ s, f x = g x) (unchanged : ∀ j ∉ outputs, ∀ (x : Fin n → Bool), f x j = g x j) : complexityGiven interpretation f g ≤ complexity interpretation (indicator s) + complexityOn interpretation s (errorVector f g outputs) + 5 * outputs.card

A support and a partial vector correction bound the cost of correcting g into f.

theorem Cslib.Circuits.Boolean.Correction.complexityGiven_le {n m : ℕ} (f g : (Fin n → Bool) → Fin m → Bool) : complexityGiven interpretation f g ≤ complexity interpretation (indicator (errorSupport f g)) + complexityOn interpretation (errorSupport f g) (errorVector f g (activeOutputs f g)) + 5 * (activeOutputs f g).card

The canonical error support and active output set give a relative correction bound.

theorem Cslib.Circuits.Boolean.Correction.errorVector_comm {n m : ℕ} (f g : (Fin n → Bool) → Fin m → Bool) (outputs : Finset (Fin m)) : errorVector f g outputs = errorVector g f outputs

The error vector is unchanged when the two functions are exchanged.

theorem Cslib.Circuits.Boolean.Correction.complexity_dist_le_of_cover {n m : ℕ} (f g : (Fin n → Bool) → Fin m → Bool) (s : Set (Fin n → Bool)) (outputs : Finset (Fin m)) (outside : ∀ x ∉ s, f x = g x) (unchanged : ∀ j ∉ outputs, ∀ (x : Fin n → Bool), f x j = g x j) : (complexity interpretation f).dist (complexity interpretation g) ≤ complexity interpretation (indicator s) + complexityOn interpretation s (errorVector f g outputs) + 5 * outputs.card

Correcting either direction bounds the absolute change in minimum circuit size.

theorem Cslib.Circuits.Boolean.Correction.complexity_dist_le {n m : ℕ} (f g : (Fin n → Bool) → Fin m → Bool) : (complexity interpretation f).dist (complexity interpretation g) ≤ complexity interpretation (indicator (errorSupport f g)) + complexityOn interpretation (errorSupport f g) (errorVector f g (activeOutputs f g)) + 5 * (activeOutputs f g).card

Sparse vector correction with the exact support and the exact active output set.

theorem Cslib.Circuits.Boolean.Correction.complexity_dist_le_sum_of_cover {n m : ℕ} (f g : (Fin n → Bool) → Fin m → Bool) (s : Set (Fin n → Bool)) (outputs : Finset (Fin m)) (outside : ∀ x ∉ s, f x = g x) (unchanged : ∀ j ∉ outputs, ∀ (x : Fin n → Bool), f x j = g x j) : (complexity interpretation f).dist (complexity interpretation g) ≤ (complexity interpretation (indicator s) + ∑ j : Fin outputs.card, complexityOn interpretation s fun (x : Fin n → Bool) (x_1 : Fin 1) => errorVector f g outputs x j) + 5 * outputs.card

Scalar synthesis on the support can supply each label separately.