Directed simulation overhead

For finite source signatures, the local overhead of a realization is the largest operation-gadget size, normalized to be at least one. The normalization is essential because free output wires allow projections to have zero-gate implementations. Taking the infimum over realizations gives an extended-natural directed overhead; ⊤ means that no realization exists. Its logarithm is an extended-real directed distance satisfying the triangle inequality.

def Algebraic.Realization.overhead {σ : Signature} {U : Type u_2} {τ : Signature} [Fintype σ.Op] {source : Interpretation σ U} {target : Interpretation τ U} (realization : Realization σ τ source target) : ℕ

Maximum selected gadget size, normalized to be at least one.

Equations

• realization.overhead = max 1 (Finset.univ.sup fun (op : σ.Op) => (realization.operation op).size)

theorem Algebraic.Realization.one_le_overhead {σ : Signature} {U : Type u_2} {τ : Signature} [Fintype σ.Op] {source : Interpretation σ U} {target : Interpretation τ U} (realization : Realization σ τ source target) : 1 ≤ realization.overhead

theorem Algebraic.Realization.operation_size_le_overhead {σ : Signature} {U : Type u_2} {τ : Signature} [Fintype σ.Op] {source : Interpretation σ U} {target : Interpretation τ U} (realization : Realization σ τ source target) (op : σ.Op) : (realization.operation op).size ≤ realization.overhead

@[simp]

theorem Algebraic.Realization.overhead_id {σ : Signature} {U : Type u_2} [Fintype σ.Op] (interpretation : Interpretation σ U) : (id interpretation).overhead = 1

theorem Algebraic.Realization.overhead_comp {σ : Signature} {U : Type u_2} {τ : Signature} {υ : Signature} [Fintype σ.Op] [Fintype τ.Op] {source : Interpretation σ U} {middle : Interpretation τ U} {target : Interpretation υ U} (outer : Realization τ υ middle target) (inner : Realization σ τ source middle) : (outer.comp inner).overhead ≤ outer.overhead * inner.overhead

Local overhead is submultiplicative under realization composition.

noncomputable def Cslib.Circuits.Interpretation.simulationOverhead {σ : Signature} {U : Type u_2} {τ : Signature} [Fintype σ.Op] (source : Interpretation σ U) (target : Interpretation τ U) : ℕ∞

Optimal normalized local overhead for realizing source in target. The value is ⊤ if no realization exists.

Equations

• source.simulationOverhead target = ⨅ (realization : Algebraic.Realization σ τ source target), ↑realization.overhead

theorem Cslib.Circuits.Interpretation.simulationOverhead_le {σ : Signature} {U : Type u_2} {τ : Signature} [Fintype σ.Op] {source : Interpretation σ U} {target : Interpretation τ U} (realization : Algebraic.Realization σ τ source target) : source.simulationOverhead target ≤ ↑realization.overhead

theorem Cslib.Circuits.Interpretation.one_le_simulationOverhead {σ : Signature} {U : Type u_2} {τ : Signature} [Fintype σ.Op] (source : Interpretation σ U) (target : Interpretation τ U) : 1 ≤ source.simulationOverhead target

@[simp]

theorem Cslib.Circuits.Interpretation.simulationOverhead_self {σ : Signature} {U : Type u_2} [Fintype σ.Op] (interpretation : Interpretation σ U) : interpretation.simulationOverhead interpretation = 1

theorem Cslib.Circuits.Interpretation.simulationOverhead_lt_top_iff {σ : Signature} {U : Type u_2} {τ : Signature} [Fintype σ.Op] (source : Interpretation σ U) (target : Interpretation τ U) : source.simulationOverhead target < ⊤ ↔ Nonempty (Algebraic.Realization σ τ source target)

A directed overhead is finite exactly when a realization exists.

theorem Cslib.Circuits.Interpretation.simulationOverhead_lt_top_of_functionallyComplete {σ : Signature} {U : Type u_2} {τ : Signature} [Fintype σ.Op] (source : Interpretation σ U) (target : Interpretation τ U) (complete : target.FunctionallyComplete) : source.simulationOverhead target < ⊤

Every interpretation has finite directed overhead into a functionally complete target interpretation.

theorem Cslib.Circuits.Interpretation.simulationOverhead_triangle {σ : Signature} {U : Type u_2} {τ : Signature} {υ : Signature} [Fintype σ.Op] [Fintype τ.Op] (source : Interpretation σ U) (middle : Interpretation τ U) (target : Interpretation υ U) : source.simulationOverhead target ≤ source.simulationOverhead middle * middle.simulationOverhead target

Multiplicative triangle inequality for optimal local overhead.

noncomputable def Cslib.Circuits.Interpretation.simulationDistance {σ : Signature} {U : Type u_2} {τ : Signature} [Fintype σ.Op] (source : Interpretation σ U) (target : Interpretation τ U) : EReal

Logarithmic directed distance associated with optimal local overhead.

Equations

• source.simulationDistance target = (↑(source.simulationOverhead target)).log

@[simp]

theorem Cslib.Circuits.Interpretation.simulationDistance_self {σ : Signature} {U : Type u_2} [Fintype σ.Op] (interpretation : Interpretation σ U) : interpretation.simulationDistance interpretation = 0

theorem Cslib.Circuits.Interpretation.simulationDistance_nonnegative {σ : Signature} {U : Type u_2} {τ : Signature} [Fintype σ.Op] (source : Interpretation σ U) (target : Interpretation τ U) : 0 ≤ source.simulationDistance target

theorem Cslib.Circuits.Interpretation.simulationDistance_triangle {σ : Signature} {U : Type u_2} {τ : Signature} {υ : Signature} [Fintype σ.Op] [Fintype τ.Op] (source : Interpretation σ U) (middle : Interpretation τ U) (target : Interpretation υ U) : source.simulationDistance target ≤ source.simulationDistance middle + middle.simulationDistance target

Additive triangle inequality for logarithmic directed distance.