Supports and labels of Boolean circuit corrections

All complexity measures are CSLib's minimum De Morgan gate counts. Constants are counted, and selecting or repeating output wires is free. Relative complexity supplies both the original input and the comparison function.

def Cslib.Circuits.Boolean.Correction.errorSupport {n m : ℕ} (f g : (Fin n → Bool) → Fin m → Bool) : Set (Fin n → Bool)

Inputs on which two output vectors differ.

Equations

• Cslib.Circuits.Boolean.Correction.errorSupport f g = {x : Fin n → Bool | f x ≠ g x}

noncomputable def Cslib.Circuits.Boolean.Correction.rowDistance {n m : ℕ} (f g : (Fin n → Bool) → Fin m → Bool) : ℕ

Number of input rows on which the two output vectors differ.

Equations

• Cslib.Circuits.Boolean.Correction.rowDistance f g = (Cslib.Circuits.Boolean.Correction.errorSupport f g).toFinset.card

noncomputable def Cslib.Circuits.Boolean.Correction.activeOutputs {n m : ℕ} (f g : (Fin n → Bool) → Fin m → Bool) : Finset (Fin m)

Output coordinates on which the two functions differ somewhere.

Equations

• Cslib.Circuits.Boolean.Correction.activeOutputs f g = {j : Fin m | ∃ (x : Fin n → Bool), f x j ≠ g x j}

noncomputable def Cslib.Circuits.Boolean.Correction.indicator {n : ℕ} (s : Set (Fin n → Bool)) : (Fin n → Bool) → Fin 1 → Bool

The indicator of a set, as a single-output target.

Equations

• Cslib.Circuits.Boolean.Correction.indicator s x x✝ = decide (x ∈ s)

noncomputable def Cslib.Circuits.Boolean.Correction.errorVector {n m : ℕ} (f g : (Fin n → Bool) → Fin m → Bool) (outputs : Finset (Fin m)) : (Fin n → Bool) → Fin outputs.card → Bool

The XOR correction restricted to a selected finite set of output coordinates.

Equations

• Cslib.Circuits.Boolean.Correction.errorVector f g outputs x j = (f x ↑(outputs.equivFin.symm j) ^^ g x ↑(outputs.equivFin.symm j))