Erasure identities and exact consistency

The original and erased programs have identical wire namespaces. Gate equations therefore compare their traces directly, using CSLib's acyclic uniqueness theorem.

theorem Algebraic.Aggregate.eraseLine_mapWires {J : Type} {State : J → Type} {n g : ℕ} (line : Line (signature State) n g) (value : Bool) {n' g' : ℕ} (map : Wire n g → Wire n' g') : eraseLine (line.mapWires map) value = (eraseLine line value).mapWires map

theorem Algebraic.Aggregate.lines_eraseWith {J : Type} {State : J → Type} {n g : ℕ} (p : Program (signature State) n g) (values : Fin g → Bool) (gate : Fin g) : (eraseWith p values).lines gate = eraseLine (p.lines gate) (values gate)

theorem Algebraic.Aggregate.eraseLine_eval {J : Type} {State : J → Type} {n g : ℕ} [(j : J) → CommMonoid (State j)] (line : Line (signature State) n g) (value : Bool) (input : Fin n → Bool) (gates : Fin g → Bool) : (eraseLine line value).eval ordinaryInterpretation input gates = if Op.isSpecial line.op = true then value else line.eval interpretation input gates

theorem Algebraic.Aggregate.eraseWith_eval_gate {J : Type} {State : J → Type} {n g : ℕ} [(j : J) → CommMonoid (State j)] (p : Program (signature State) n g) (values : Fin g → Bool) (input : Fin n → Bool) (gate : Fin g) : (eraseWith p values).eval ordinaryInterpretation input gate = if Op.isSpecial (p.lines gate).op = true then values gate else (p.lines gate).eval interpretation input ((eraseWith p values).eval ordinaryInterpretation input)

theorem Algebraic.Aggregate.erase_fanInAtMost {J : Type} {State : J → Type} {n g : ℕ} (p : Program (signature State) n g) (a : Guess p) : (erase p a).FanInAtMost 2

theorem Algebraic.Aggregate.arity_lines_erase {J : Type} {State : J → Type} {n g : ℕ} (p : Program (signature State) n g) (a : Guess p) (gate : Fin g) : ordinarySignature.Arity ((erase p a).lines gate).op = if Op.isSpecial (p.lines gate).op = true then 0 else 2

Erased special gates have no slots; every ordinary gate retains its two slots.

theorem Algebraic.Aggregate.erase_eval_special {J : Type} {State : J → Type} {n g : ℕ} [(j : J) → CommMonoid (State j)] (p : Program (signature State) n g) (a : Guess p) (input : Fin n → Bool) (gate : SpecialGate p) : (erase p a).eval ordinaryInterpretation input ↑gate = a gate

theorem Algebraic.Aggregate.erase_eval_of_consistent {J : Type} {State : J → Type} {n g : ℕ} [(j : J) → CommMonoid (State j)] (p : Program (signature State) n g) (a : Guess p) (input : Fin n → Bool) (h : Consistent p a input) : (erase p a).eval ordinaryInterpretation input = p.eval interpretation input

theorem Algebraic.Aggregate.erase_eval_actualGuess {J : Type} {State : J → Type} {n g : ℕ} [(j : J) → CommMonoid (State j)] (p : Program (signature State) n g) (input : Fin n → Bool) : (erase p (actualGuess p input)).eval ordinaryInterpretation input = p.eval interpretation input

theorem Algebraic.Aggregate.actualGuess_consistent {J : Type} {State : J → Type} {n g : ℕ} [(j : J) → CommMonoid (State j)] (p : Program (signature State) n g) (input : Fin n → Bool) : Consistent p (actualGuess p input) input

theorem Algebraic.Aggregate.consistent_iff_eq_actualGuess {J : Type} {State : J → Type} {n g : ℕ} [(j : J) → CommMonoid (State j)] (p : Program (signature State) n g) (a : Guess p) (input : Fin n → Bool) : Consistent p a input ↔ a = actualGuess p input