Circuits for support-masked corrections

The support circuit is shared by every corrected output. The labels are a single circuit required to be correct only on the support, so its internal sharing is preserved too. Each selected output adds one mask and four XOR gates.

theorem Cslib.Circuits.Boolean.Correction.Internal.complexity_xor_le {n : ℕ} (f g : BooleanFunction n) : (complexity interpretation fun (x : Fin n → Bool) (x_1 : Fin 1) => f x ^^ g x) ≤ ((complexity interpretation fun (x : Fin n → Bool) (x_1 : Fin 1) => f x) + complexity interpretation fun (x : Fin n → Bool) (x_1 : Fin 1) => g x) + 4

theorem Cslib.Circuits.Boolean.Correction.Internal.scalar_complexity_le {n : ℕ} (f g : BooleanFunction n) : (complexity interpretation fun (x : Fin n → Bool) (x_1 : Fin 1) => f x) ≤ (complexity interpretation fun (x : Fin n → Bool) (x_1 : Fin 1) => g x) + complexity interpretation (indicator {x : Fin n → Bool | f x ≠ g x}) + 4

def Cslib.Circuits.Boolean.Correction.Internal.oldWire {m : ℕ} (outputs : Finset (Fin m)) (j : Fin m) : Fin (m + 1 + outputs.card)

Wire carrying an old output in the correction interface.

Equations

• Cslib.Circuits.Boolean.Correction.Internal.oldWire outputs j = Fin.castAdd outputs.card (Fin.castAdd 1 j)

def Cslib.Circuits.Boolean.Correction.Internal.supportWire {m : ℕ} (outputs : Finset (Fin m)) : Fin (m + 1 + outputs.card)

Wire carrying the common support indicator.

Equations

• Cslib.Circuits.Boolean.Correction.Internal.supportWire outputs = Fin.castAdd outputs.card (Fin.natAdd m 0)

noncomputable def Cslib.Circuits.Boolean.Correction.Internal.labelWire {m : ℕ} (outputs : Finset (Fin m)) (j : Fin m) (hj : j ∈ outputs) : Fin (m + 1 + outputs.card)

Wire carrying the partial correction for an active coordinate.

Equations

• Cslib.Circuits.Boolean.Correction.Internal.labelWire outputs j hj = Fin.natAdd (m + 1) (outputs.equivFin ⟨j, hj⟩)

noncomputable def Cslib.Circuits.Boolean.Correction.Internal.patch {m : ℕ} (outputs : Finset (Fin m)) : (Fin (m + 1 + outputs.card) → Bool) → Fin m → Bool

Mask a supplied correction and XOR it into a selected output.

Equations

• One or more equations did not get rendered due to their size.

theorem Cslib.Circuits.Boolean.Correction.Internal.exists_patch {m : ℕ} (outputs : Finset (Fin m)) : ∃ (c : Circuit signature (m + 1 + outputs.card) m), c.Computes interpretation (patch outputs) ∧ c.size ≤ 5 * outputs.card

theorem Cslib.Circuits.Boolean.Correction.Internal.exists_correction {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) (support : Circuit signature n 1) (hs : support.Computes interpretation (indicator s)) (labels : Circuit signature n outputs.card) (hl : labels.ComputesOn interpretation s (errorVector f g outputs)) : ∃ (c : Circuit signature (n + m) m), (∀ (x : Fin n → Bool), c.eval interpretation (Fin.append x (g x)) = f x) ∧ c.size ≤ support.size + labels.size + 5 * outputs.card

theorem Cslib.Circuits.Boolean.Correction.Internal.complexityGiven_bound {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