Exact reconstruction from primary-input summaries

Acyclic gate-equation uniqueness supplies topological reconstruction. Splitting a special gate's product requires commutativity, but no inverses or cancellation.

theorem Algebraic.Aggregate.Capacity.lineSummary_eq_of_selected_agree {J : Type} {State : J → Type} {n g : ℕ} [(j : J) → CommMonoid (State j)] (line : Line (signature State) n g) (U : Finset (Fin n)) (x y : Wire n g → Bool) (h : ∀ (wire : Wire n g), selected U wire → x wire = y wire) : lineSummary line U x = lineSummary line U y

A line summary depends only on the selected primary wires.

theorem Algebraic.Aggregate.Capacity.line_eval_eq_of_summary_eq {J : Type} {State : J → Type} {n g : ℕ} [(j : J) → CommMonoid (State j)] (line : Line (signature State) n g) (U : Finset (Fin n)) (x y : Wire n g → Bool) (hs : lineSummary line U x = lineSummary line U y) (h : ∀ (wire : Wire n g), ¬selected U wire → x wire = y wire) : interpretation line.op (x ∘ line.wires) = interpretation line.op (y ∘ line.wires)

Equal summaries and equal unselected values determine the same gate output.

theorem Algebraic.Aggregate.Capacity.lineSummary_elim {J : Type} {State : J → Type} {n g : ℕ} [(j : J) → CommMonoid (State j)] (line : Line (signature State) n g) (U : Finset (Fin n)) (input : Fin n → Bool) (gates : Fin g → Bool) : lineSummary line U (Wire.elim input gates) = lineSummary line U (Wire.elim input fun (x : Fin g) => false)

Changing internal gate values does not affect a primary-input summary.

theorem Algebraic.Aggregate.Capacity.key_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)) (x y : Fin n → Bool) (h : ∀ i ∈ U, x i = y i) : key p U x = key p U y

The complete key depends only on selected primary inputs.

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

Equal keys let the other party reconstruct every gate, regardless of depth.

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

Gate outputs and unselected primary outputs are reconstructed exactly.