Reusing circuits in synthesis arguments

Ordered families let each member of a synthesized family use all preceding members, with the total budget given by the sum of the step budgets (Synthesis.ordered_family). Applied to the gates of a program, they rebuild the program from gatewise bounds (Program.synthesis_of_steps). In particular a concrete circuit supplies a synthesis bound for its designated outputs, which connects circuit composition with constructions using shared wires.

The rules Synthesis.with_sources, Synthesis.sequence and Synthesis.ordered_family, and the program lemmas Program.wireFunction_mem_before, Program.synthesis_step and Program.synthesis_of_steps, come from Cslib.Computability.Circuit.Synthesis at commit 2a4389b of the author's CSLib fork (branch complexitylib-integration); upstream CSLib does not have them.

theorem Cslib.Circuits.Synthesis.with_sources {σ : Signature} {U : Type u} {n : ℕ} {I : Interpretation σ U} {s t : Set ((Fin n → U) → U)} {a : ℕ} (h : Synthesis I s t a) : Synthesis I s (s ∪ t) a

A synthesis retains its sources alongside its targets.

theorem Cslib.Circuits.Synthesis.sequence {σ : Signature} {U : Type u} {n : ℕ} {I : Interpretation σ U} {k : ℕ} (stages : Fin (k + 1) → Set ((Fin n → U) → U)) (cost : Fin k → ℕ) (step : ∀ (j : Fin k), Synthesis I (stages j.castSucc) (stages j.succ) (cost j)) : Synthesis I (stages 0) (stages (Fin.last k)) (∑ j : Fin k, cost j)

Compose an indexed sequence of syntheses, adding their gate budgets.

theorem Cslib.Circuits.Synthesis.ordered_family {σ : Signature} {U : Type u} {n : ℕ} {I : Interpretation σ U} {s : Set ((Fin n → U) → U)} {k : ℕ} (f : Fin k → (Fin n → U) → U) (cost : Fin k → ℕ) (step : ∀ (j : Fin k), Synthesis I (s ∪ f '' {i : Fin k | i < j}) {f j} (cost j)) : Synthesis I s (Set.range f) (∑ j : Fin k, cost j)

Synthesize a family in order, allowing each function to use all preceding ones.

theorem Cslib.Circuits.Program.wireFunction_mem_before {σ : Signature} {U : Type u} {n : ℕ} {I : Interpretation σ U} {g : ℕ} (p : Program σ n g) (j : Fin g) (wire : Wire n g) (hwire : ↑wire.index < n + ↑j) : p.wireFunction I wire ∈ inputs n ∪ p.gateFunction I '' {i : Fin g | i < j}

A preceding wire is either an input or a preceding gate function.

theorem Cslib.Circuits.Program.synthesis_step {σ : Signature} {U : Type u} {n : ℕ} {I : Interpretation σ U} {g : ℕ} (p : Program σ n g) (j : Fin g) : Synthesis I (inputs n ∪ p.gateFunction I '' {i : Fin g | i < j}) {p.gateFunction I j} 1

Each program gate can be synthesized from the inputs and preceding gates.

theorem Cslib.Circuits.Program.synthesis_of_steps {σ : Signature} {U : Type u} {n : ℕ} {I : Interpretation σ U} {g : ℕ} (p : Program σ n g) (cost : Fin g → ℕ) (step : ∀ (j : Fin g), Synthesis I (inputs n ∪ p.gateFunction I '' {i : Fin g | i < j}) {p.gateFunction I j} (cost j)) : Synthesis I (inputs n) (available I p) (∑ j : Fin g, cost j)

Rebuild a program from gatewise synthesis bounds, retaining every wire function.

theorem Cslib.Circuits.Circuit.synthesis {σ : Signature} {U : Type} {n m : ℕ} {I : Interpretation σ U} (c : Circuit σ n m) : Synthesis I (inputs n) (Set.range fun (j : Fin m) (x : Fin n → U) => c.eval I x j) c.size

Rebuild the circuit's outputs within its existing gate budget.

theorem Cslib.Circuits.Circuit.Computes.synthesis {σ : Signature} {U : Type} {n m : ℕ} {I : Interpretation σ U} {c : Circuit σ n m} {f : (Fin n → U) → Fin m → U} (hc : c.Computes I f) : Synthesis I (inputs n) (Set.range fun (j : Fin m) (x : Fin n → U) => f x j) c.size

A circuit computing f supplies a synthesis bound for all coordinates of f.