Aggregate keys and mixing across component unions

The ordinary graph omits special gates and their incident edges. Equal special-output guesses fix every omitted signal. A single vector of left-side partial aggregates then suffices for exact mixing, using only the commutative-monoid laws.

def Algebraic.Aggregate.specialWire {J : Type} {State : J → Type} {n g : ℕ} (p : Program (signature State) n g) : Wire n g → Bool

Whether a signal is the output of a special gate. Inputs are ordinary signals.

Equations

• Algebraic.Aggregate.specialWire p (Cslib.Circuits.Wire.input input) = false
• Algebraic.Aggregate.specialWire p (Cslib.Circuits.Wire.gate gate) = Algebraic.Aggregate.Op.isSpecial (p.lines gate).op

def Algebraic.Aggregate.ClosedSet {J : Type} {State : J → Type} {n g : ℕ} (p : Program (signature State) n g) (S : Finset (Wire n g)) : Prop

A union of components of the graph of ordinary-to-ordinary slots. Special-to-ordinary slots are known constants once the special outputs are guessed.

Equations

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

theorem Algebraic.Aggregate.reads_erase_iff {J : Type} {State : J → Type} {n g : ℕ} (p : Program (signature State) n g) (a : Guess p) (gate : Fin g) (wire : Wire n g) : (erase p a).Reads gate wire ↔ Op.isSpecial (p.lines gate).op = false ∧ p.Reads gate wire

Erasure deletes exactly the slots whose target gate is special.

theorem Algebraic.Aggregate.reads_erase_iff_reads_erase {J : Type} {State : J → Type} {n g : ℕ} (p : Program (signature State) n g) (a b : Guess p) (gate : Fin g) (wire : Wire n g) : (erase p a).Reads gate wire ↔ (erase p b).Reads gate wire

The erased graph is independent of the values of the guessed bits.

theorem Algebraic.Aggregate.closedSet_of_erase_closed {J : Type} {State : J → Type} {n g : ℕ} (p : Program (signature State) n g) (a : Guess p) (S : Finset (Wire n g)) (closed : ∀ (gate : Fin g) (wire : Wire n g), (erase p a).Reads gate wire → (wire ∈ S ↔ Wire.gate gate ∈ S)) : ClosedSet p S

Closure for all slots of an erased program implies ordinary component closure.

def Algebraic.Aggregate.lineAggregate {J : Type} {State : J → Type} {n g : ℕ} [(j : J) → CommMonoid (State j)] (line : Line (signature State) n g) (S : Finset (Wire n g)) (values : Wire n g → Bool) : Op.Register line.op

Multiply the contributions whose source signals lie in S, counting repeated slots.

Equations

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

def Algebraic.Aggregate.partialAggregate {J : Type} {State : J → Type} {n g : ℕ} [(j : J) → CommMonoid (State j)] (p : Program (signature State) n g) (S : Finset (Wire n g)) (input : Fin n → Bool) : Registers p

The partial aggregate vector associated to actual signal values on S.

Equations

• Algebraic.Aggregate.partialAggregate p S input gate = Algebraic.Aggregate.lineAggregate (p.lines ↑gate) S (p.trace Algebraic.Aggregate.interpretation input)

def Algebraic.Aggregate.componentKey {J : Type} {State : J → Type} {n g : ℕ} [(j : J) → CommMonoid (State j)] (p : Program (signature State) n g) (S : Finset (Wire n g)) (input : Fin n → Bool) : Guess p × Registers p

The exact rectangle key: guessed special outputs and one partial aggregate vector.

Equations

• Algebraic.Aggregate.componentKey p S input = (Algebraic.Aggregate.actualGuess p input, Algebraic.Aggregate.partialAggregate p S input)

theorem Algebraic.Aggregate.lineAggregate_partition {J : Type} {State : J → Type} {n g : ℕ} [(j : J) → CommMonoid (State j)] (line : Line (signature State) n g) (S : Finset (Wire n g)) (values : Wire n g → Bool) : lineAggregate line S values * lineAggregate line Sᶜ values = lineAggregate line Finset.univ values

theorem Algebraic.Aggregate.lineAggregate_mix {J : Type} {State : J → Type} {n g : ℕ} [(j : J) → CommMonoid (State j)] (line : Line (signature State) n g) (S : Finset (Wire n g)) (x y : Wire n g → Bool) : (lineAggregate line Finset.univ fun (w : Wire n g) => if w ∈ S then x w else y w) = lineAggregate line S x * lineAggregate line Sᶜ y

theorem Algebraic.Aggregate.line_eval_eq_of_aggregate_eq {J : Type} {State : J → Type} {n g : ℕ} [(j : J) → CommMonoid (State j)] (line : Line (signature State) n g) (hs : Op.isSpecial line.op = true) (x y : Wire n g → Bool) (h : lineAggregate line Finset.univ x = lineAggregate line Finset.univ y) : interpretation line.op (x ∘ line.wires) = interpretation line.op (y ∘ line.wires)

theorem Algebraic.Aggregate.trace_mix_of_componentKey_eq {J : Type} {State : J → Type} {n g : ℕ} [(j : J) → CommMonoid (State j)] (p : Program (signature State) n g) (S : Finset (Wire n g)) (closed : ClosedSet p S) (x y : Fin n → Bool) (key : componentKey p S x = componentKey p S y) (wire : Wire n g) : p.trace interpretation (Cutwidth.SingleCut.mix S x y) wire = if wire ∈ S then p.trace interpretation x wire else p.trace interpretation y wire

Equal component keys allow the two evaluations to be pasted along a closed set.

theorem Algebraic.Aggregate.accepts_mix_of_componentKey_eq {J : Type} {State : J → Type} {n g : ℕ} [(j : J) → CommMonoid (State j)] (p : Program (signature State) n g) (S : Finset (Wire n g)) (closed : ClosedSet p S) (out : Wire n g) (x y : Fin n → Bool) (hx : p.trace interpretation x out = true) (hy : p.trace interpretation y out = true) (key : componentKey p S x = componentKey p S y) : p.trace interpretation (Cutwidth.SingleCut.mix S x y) out = true

Accepted inputs with the same component key mix to another accepted input.