One-way summaries of whole aggregate circuits

The primary-input summary reconstructs every gate output. One additional bit handles a designated output that is itself a selected primary input.

@[reducible, inline]

abbrev Algebraic.Aggregate.Capacity.OutputKey {J : Type} {State : J → Type} {n g : ℕ} (p : Program (signature State) n g) : Type

A summary with a spare bit for a designated primary-input output.

Equations

• Algebraic.Aggregate.Capacity.OutputKey p = (Algebraic.Aggregate.Capacity.Key p × Bool)

def Algebraic.Aggregate.Capacity.outputKey {J : Type} {State : J → Type} {n g : ℕ} [(j : J) → CommMonoid (State j)] (p : Program (signature State) n g) (U : Finset (Fin n)) (out : Wire n g) (input : Fin n → Bool) : OutputKey p

Summarize selected primary inputs, including a selected primary output if present.

Equations

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

theorem Algebraic.Aggregate.Capacity.outputKey_eq_of_inputs_agree {J : Type} {State : J → Type} {n g : ℕ} [(j : J) → CommMonoid (State j)] (p : Program (signature State) n g) (U : Finset (Fin n)) (out : Wire n g) (x y : Fin n → Bool) (h : ∀ i ∈ U, x i = y i) : outputKey p U out x = outputKey p U out y

The output summary is determined by the sending party's primary inputs.

theorem Algebraic.Aggregate.Capacity.trace_eq_of_outputKey_eq {J : Type} {State : J → Type} {n g : ℕ} [(j : J) → CommMonoid (State j)] (p : Program (signature State) n g) (U : Finset (Fin n)) (out : Wire n g) (x y : Fin n → Bool) (hk : outputKey p U out x = outputKey p U out y) (h : ∀ i ∉ U, x i = y i) : p.trace interpretation x out = p.trace interpretation y out

Equal output summaries determine the output for every fixed complementary input.

theorem Algebraic.Aggregate.Capacity.card_outputKey_le {J : Type} {State : J → Type} {n g : ℕ} [(j : J) → Fintype (State j)] (p : Program (signature State) n g) : Fintype.card (OutputKey p) ≤ 2 ^ (capacity p + 1)

The designated output costs at most one extra bit.