Reconstruction from Boolean primary-input messages

The receiver reconstructs the actual circuit in topological order. The proof uses only the partial parity or conjunction at each gate and the complementary inputs.

theorem Algebraic.Aggregate.Geometry.lineSummary_eq_of_selected_agree {n g : ℕ} (line : Line signature n g) (U : Finset (Fin n)) (x y : Wire n g → Bool) (h : ∀ (w : Wire n g), Capacity.selected U w → x w = y w) : lineSummary line U x = lineSummary line U y

A message depends only on selected primary wire values.

theorem Algebraic.Aggregate.Geometry.line_eval_eq_of_summary_eq {n g : ℕ} (line : Line signature n g) (U : Finset (Fin n)) (x y : Wire n g → Bool) (hs : lineSummary line U x = lineSummary line U y) (h : ∀ (w : Wire n g), ¬Capacity.selected U w → x w = y w) : interpretation line.op (x ∘ line.wires) = interpretation line.op (y ∘ line.wires)

Partial summaries and the other wire values determine each gate's output.

theorem Algebraic.Aggregate.Geometry.lineSummary_elim {n g : ℕ} (line : Line signature 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)

The gate valuation is irrelevant to primary-input summaries.

theorem Algebraic.Aggregate.Geometry.key_eq_of_inputs_agree {n g : ℕ} (p : Program signature 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 whole gate message is determined by selected primary inputs.

theorem Algebraic.Aggregate.Geometry.eval_eq_of_key_eq {n g : ℕ} (p : Program signature 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 messages and equal complementary inputs give identical gate traces.

theorem Algebraic.Aggregate.Geometry.outputKey_eq_of_inputs_agree {n g : ℕ} (p : Program signature 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

Include the optional output bit without reading complementary inputs.

theorem Algebraic.Aggregate.Geometry.trace_eq_of_outputKey_eq {n g : ℕ} (p : Program signature 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

The complete output is determined by the Boolean message and complementary inputs.