Weighted circuit complexity from supplied values

A source family sources : X → Fin n → U supplies exactly the inputs available to a circuit computing target : X → Fin m → U. The common domain may be arbitrary. No coordinates of X are implicitly available, and supplying the sources has no cost. The minimum of Program.cost over implementing circuits is recorded in ℕ∞, with ⊤ when no circuit exists.

Operation costs may be zero. Consequently, zero weighted complexity need not mean that the target is obtained by wiring. Even with an empty common domain, a syntactic circuit must exist; vacuous correctness alone does not provide outputs from zero inputs over an empty signature.

Unit costs recover native support complexity by taking the support subtype as the common domain. Supplying both raw inputs and helper values recovers native ecomplexityGiven. These bridges require no chosen extension of the target outside the range of the sources.

The model allows arbitrary finite gate arities and natural-number weights. Every output must be wired; constants must be supplied or implemented by gates. In particular, the syntax does not use Boyack's convention assigning zero to disconnected vertices.

Main definitions

• Cslib.Circuits.Circuit.ComputesFrom: computation from exactly the supplied source family.
• Cslib.Circuits.ecomplexityFrom: minimum weighted cost of such a computation.

Main results

• Cslib.Circuits.ecomplexityFrom_le_iff: every finite budget has a circuit witness.
• Cslib.Circuits.ecomplexityFrom_comp_le: composition through an intermediate supplied family.
• Cslib.Circuits.ecomplexityFrom_map_le: homomorphisms cannot increase source complexity; ecomplexityFrom_map_eq gives equality for injective homomorphisms.
• Cslib.Circuits.ecomplexityFrom_unit_subtype, Cslib.Circuits.ecomplexityFrom_unit_append: bridges to native circuit complexity.

References

• Ported from Complexity/Relative.lean in S. Schlesinger, Algebraic circuit formalizations in Complexitylib. Homomorphism transport adapts LowerBound/Fusion/Comap.lean from the same development.
• S. W. Boyack, The Robustness of Combinatorial Measures of Boolean Matrix Complexity, Definition 2.1 and Proposition 2.2, pp. 29–30, for computation relative to supplied functions and its composition inequality.

def Cslib.Circuits.Circuit.ComputesFrom {σ : Signature} {U : Type u} {X : Type w} {n m : ℕ} (c : Circuit σ n m) (I : Interpretation σ U) (target : X → Fin m → U) (sources : X → Fin n → U) : Prop

Compute the target family from exactly the supplied values, without implicit raw inputs.

theorem Cslib.Circuits.Circuit.ComputesFrom.map {σ : Signature} {U : Type u} {X : Type w} {n m : ℕ} {I : Interpretation σ U} {target : X → Fin m → U} {sources : X → Fin n → U} {V : Type z} {J : Interpretation σ V} {c : Circuit σ n m} (hc : c.ComputesFrom I target sources) (h : Homomorphism I J) : c.ComputesFrom J (fun (x : X) => h.map ∘ target x) fun (x : X) => h.map ∘ sources x

The same circuit computes the homomorphic image of the supplied-source problem.

theorem Cslib.Circuits.Circuit.computesFrom_map_iff {σ : Signature} {U : Type u} {X : Type w} {n m : ℕ} {I : Interpretation σ U} {target : X → Fin m → U} {sources : X → Fin n → U} {V : Type z} {J : Interpretation σ V} (c : Circuit σ n m) (h : Homomorphism I J) (hinj : Function.Injective h.map) : (c.ComputesFrom J (fun (x : X) => h.map ∘ target x) fun (x : X) => h.map ∘ sources x) ↔ c.ComputesFrom I target sources

An injective homomorphism also reflects computation of the supplied-source problem.

theorem Cslib.Circuits.Circuit.ComputesFrom.agrees_on_fibers {σ : Signature} {U : Type u} {X : Type w} {n m : ℕ} {I : Interpretation σ U} {target : X → Fin m → U} {sources : X → Fin n → U} {c : Circuit σ n m} (hc : c.ComputesFrom I target sources) {x y : X} (h : sources x = sources y) : target x = target y

Equal supplied values must give equal target values.

theorem Cslib.Circuits.Circuit.ComputesFrom.comp {σ : Signature} {U : Type u} {X : Type w} {n m p : ℕ} {I : Interpretation σ U} {sources : X → Fin n → U} {c : Circuit σ n m} {d : Circuit σ m p} {f : X → Fin m → U} {g : X → Fin p → U} (hc : c.ComputesFrom I f sources) (hd : d.ComputesFrom I g f) : (d.comp c).ComputesFrom I g sources

Compose computations through an intermediate supplied family.

theorem Cslib.Circuits.Circuit.ComputesFrom.append {σ : Signature} {U : Type u} {X : Type w} {n m p : ℕ} {I : Interpretation σ U} {sources : X → Fin n → U} {c : Circuit σ n m} {d : Circuit σ n p} {f : X → Fin m → U} {g : X → Fin p → U} (hc : c.ComputesFrom I f sources) (hd : d.ComputesFrom I g sources) : (c.append d).ComputesFrom I (fun (x : X) => Fin.append (f x) (g x)) sources

Compute two target families from the same supplied values.

@[simp]

theorem Cslib.Circuits.Circuit.computesFrom_subtype_iff {σ : Signature} {U : Type u} {n m : ℕ} {I : Interpretation σ U} (c : Circuit σ n m) (S : Set (Fin n → U)) (f : (Fin n → U) → Fin m → U) : c.ComputesFrom I (fun (x : ↑S) => f ↑x) Subtype.val ↔ c.ComputesOn I S f

theorem Cslib.Circuits.Circuit.computesFrom_iff_computesOn_range {σ : Signature} {U : Type u} {X : Type w} {n m : ℕ} {I : Interpretation σ U} {target : X → Fin m → U} {sources : X → Fin n → U} (c : Circuit σ n m) (f : (Fin n → U) → Fin m → U) (hf : ∀ (x : X), f (sources x) = target x) : c.ComputesFrom I target sources ↔ c.ComputesOn I (Set.range sources) f

An explicitly supplied extension identifies source computation with computation on its range.

noncomputable def Cslib.Circuits.ecomplexityFrom {σ : Signature} {U : Type u} {X : Type w} {n m : ℕ} (I : Interpretation σ U) (cost : σ.Op → ℕ) (target : X → Fin m → U) (sources : X → Fin n → U) : ℕ∞

Minimum weighted cost of computing a target from the supplied values, or ⊤ if no circuit does so. Every operation has finite natural-number cost; supplying the sources is free.

theorem Cslib.Circuits.ecomplexityFrom_le_of_computesFrom {σ : Signature} {U : Type u} {X : Type w} {n m : ℕ} {I : Interpretation σ U} {cost : σ.Op → ℕ} {target : X → Fin m → U} {sources : X → Fin n → U} (c : Circuit σ n m) (hc : c.ComputesFrom I target sources) : ecomplexityFrom I cost target sources ≤ ↑(c.program.cost cost)

theorem Cslib.Circuits.ecomplexityFrom_ne_top_iff {σ : Signature} {U : Type u} {X : Type w} {n m : ℕ} {I : Interpretation σ U} {cost : σ.Op → ℕ} {target : X → Fin m → U} {sources : X → Fin n → U} : ecomplexityFrom I cost target sources ≠ ⊤ ↔ ∃ (c : Circuit σ n m), c.ComputesFrom I target sources

@[simp]

theorem Cslib.Circuits.ecomplexityFrom_eq_top_iff {σ : Signature} {U : Type u} {X : Type w} {n m : ℕ} {I : Interpretation σ U} {cost : σ.Op → ℕ} {target : X → Fin m → U} {sources : X → Fin n → U} : ecomplexityFrom I cost target sources = ⊤ ↔ ¬∃ (c : Circuit σ n m), c.ComputesFrom I target sources

theorem Cslib.Circuits.exists_computesFrom_cost_eq_ecomplexityFrom {σ : Signature} {U : Type u} {X : Type w} {n m : ℕ} {I : Interpretation σ U} {cost : σ.Op → ℕ} {target : X → Fin m → U} {sources : X → Fin n → U} (h : ∃ (c : Circuit σ n m), c.ComputesFrom I target sources) : ∃ (c : Circuit σ n m), c.ComputesFrom I target sources ∧ ↑(c.program.cost cost) = ecomplexityFrom I cost target sources

A representable target has a circuit attaining its minimum weighted cost.

theorem Cslib.Circuits.ecomplexityFrom_le_iff {σ : Signature} {U : Type u} {X : Type w} {n m : ℕ} {I : Interpretation σ U} {cost : σ.Op → ℕ} {target : X → Fin m → U} {sources : X → Fin n → U} {k : ℕ} : ecomplexityFrom I cost target sources ≤ ↑k ↔ ∃ (c : Circuit σ n m), c.ComputesFrom I target sources ∧ c.program.cost cost ≤ k

Every finite weighted budget is witnessed by a circuit.

theorem Cslib.Circuits.le_ecomplexityFrom_iff {σ : Signature} {U : Type u} {X : Type w} {n m : ℕ} {I : Interpretation σ U} {cost : σ.Op → ℕ} {target : X → Fin m → U} {sources : X → Fin n → U} {k : ℕ∞} : k ≤ ecomplexityFrom I cost target sources ↔ ∀ (c : Circuit σ n m), c.ComputesFrom I target sources → k ≤ ↑(c.program.cost cost)

A lower bound holds exactly when it holds for every implementing circuit.

theorem Cslib.Circuits.ecomplexityFrom_map_le {σ : Signature} {U : Type u} {X : Type w} {n m : ℕ} {I : Interpretation σ U} {V : Type z} {J : Interpretation σ V} (h : Homomorphism I J) (weight : σ.Op → ℕ) (target : X → Fin m → U) (sources : X → Fin n → U) : (ecomplexityFrom J weight (fun (x : X) => h.map ∘ target x) fun (x : X) => h.map ∘ sources x) ≤ ecomplexityFrom I weight target sources

Applying a homomorphism to every supplied and target value cannot increase complexity. The operation weights and implementing circuit are unchanged; the map need not be injective.

theorem Cslib.Circuits.ecomplexityFrom_map_eq {σ : Signature} {U : Type u} {X : Type w} {n m : ℕ} {I : Interpretation σ U} {V : Type z} {J : Interpretation σ V} (h : Homomorphism I J) (hinj : Function.Injective h.map) (weight : σ.Op → ℕ) (target : X → Fin m → U) (sources : X → Fin n → U) : (ecomplexityFrom J weight (fun (x : X) => h.map ∘ target x) fun (x : X) => h.map ∘ sources x) = ecomplexityFrom I weight target sources

An injective homomorphism preserves supplied-source complexity, including infinity.

theorem Cslib.Circuits.ecomplexityFrom_mono_cost {σ : Signature} {U : Type u} {X : Type w} {n m : ℕ} {I : Interpretation σ U} {cost cost' : σ.Op → ℕ} {target : X → Fin m → U} {sources : X → Fin n → U} (h : ∀ (op : σ.Op), cost op ≤ cost' op) : ecomplexityFrom I cost target sources ≤ ecomplexityFrom I cost' target sources

@[simp]

theorem Cslib.Circuits.ecomplexityFrom_wiring {σ : Signature} {U : Type u} {X : Type w} {n m : ℕ} {I : Interpretation σ U} {cost : σ.Op → ℕ} (sources : X → Fin n → U) (select : Fin m → Fin n) : ecomplexityFrom I cost (fun (x : X) => sources x ∘ select) sources = 0

Selecting, permuting or duplicating supplied values is free.

@[simp]

theorem Cslib.Circuits.ecomplexityFrom_self {σ : Signature} {U : Type u} {X : Type w} {n : ℕ} {I : Interpretation σ U} {cost : σ.Op → ℕ} (sources : X → Fin n → U) : ecomplexityFrom I cost sources sources = 0

theorem Cslib.Circuits.ecomplexityFrom_eq_top_of_fiber_collision {σ : Signature} {U : Type u} {X : Type w} {n m : ℕ} {I : Interpretation σ U} {cost : σ.Op → ℕ} {target : X → Fin m → U} {sources : X → Fin n → U} {x y : X} (h : sources x = sources y) (hne : target x ≠ target y) : ecomplexityFrom I cost target sources = ⊤

If the sources identify two points distinguished by the target, no implementation exists.

theorem Cslib.Circuits.ecomplexityFrom_comp_le {σ : Signature} {U : Type u} {X : Type w} {n m p : ℕ} {I : Interpretation σ U} {cost : σ.Op → ℕ} (f : X → Fin m → U) (g : X → Fin p → U) (sources : X → Fin n → U) : ecomplexityFrom I cost g sources ≤ ecomplexityFrom I cost f sources + ecomplexityFrom I cost g f

Computing through an intermediate family adds at most the two weighted complexities.

theorem Cslib.Circuits.ecomplexityFrom_append_le {σ : Signature} {U : Type u} {X : Type w} {n m p : ℕ} {I : Interpretation σ U} {cost : σ.Op → ℕ} (f : X → Fin m → U) (g : X → Fin p → U) (sources : X → Fin n → U) : ecomplexityFrom I cost (fun (x : X) => Fin.append (f x) (g x)) sources ≤ ecomplexityFrom I cost f sources + ecomplexityFrom I cost g sources

Computing two families from the same sources costs at most the sum of their complexities.

theorem Cslib.Circuits.ecomplexityFrom_unit_subtype {σ : Signature} {U : Type u} {n m : ℕ} {I : Interpretation σ U} (S : Set (Fin n → U)) (f : (Fin n → U) → Fin m → U) : ecomplexityFrom I (fun (x : σ.Op) => 1) (fun (x : ↑S) => f ↑x) Subtype.val = ecomplexityOn I S f

Unit weights and the support subtype recover native support complexity.

theorem Cslib.Circuits.ecomplexityFrom_unit_append {σ : Signature} {U : Type u} {n m : ℕ} {I : Interpretation σ U} {k : ℕ} (f : (Fin n → U) → Fin m → U) (g : (Fin n → U) → Fin k → U) : (ecomplexityFrom I (fun (x : σ.Op) => 1) f fun (x : Fin n → U) => Fin.append x (g x)) = ecomplexityGiven I f g

Unit weights with raw inputs and helpers recover native relative complexity.