Counting circuits relative to a supplied family

For any fixed sources : X → Fin n → U, each circuit description determines at most one target on X. The ordered-description bound therefore requires no finiteness of X or U. A finite carrier additionally permits reuse of the library's factorial-improved semantic count. These are versions of the counting method in Boyack's Lemma 2.2.2 with explicit circuit conventions and arbitrary finite arities; its displayed numerical bound is not copied.

The finite-menu and rational-fraction bounds apply to any finite target family. Interpreting a fraction as a uniform probability requires that family to be nonempty. Sources are fixed before sampling the target, though a choice from a fixed finite menu can be made afterward.

noncomputable def Cslib.Circuits.Circuit.relativeFunctionsAtMost {X : Type u_1} {σ : Signature} {U : Type u_3} {n : ℕ} [Fintype σ.Op] (interpretation : Interpretation σ U) (sources : X → Fin n → U) (m budget : ℕ) : Finset (X → Fin m → U)

Targets obtainable within a gate budget from a fixed source family.

Equations

• One or more equations did not get rendered due to their size.

theorem Cslib.Circuits.Circuit.mem_relativeFunctionsAtMost_iff {X : Type u_1} {σ : Signature} {U : Type u_3} {n m : ℕ} [Fintype σ.Op] (interpretation : Interpretation σ U) (sources : X → Fin n → U) (target : X → Fin m → U) (budget : ℕ) : target ∈ relativeFunctionsAtMost interpretation sources m budget ↔ relativeGateComplexity interpretation target sources ≤ ↑budget

The counted set is exactly the set of targets within the relative budget.

theorem Cslib.Circuits.Circuit.card_relativeFunctionsAtMost_le {X : Type u_1} {σ : Signature} {U : Type u_3} {n : ℕ} [Fintype σ.Op] (interpretation : Interpretation σ U) (sources : X → Fin n → U) (m budget : ℕ) : (relativeFunctionsAtMost interpretation sources m budget).card ≤ σ.orderedBudget n m budget

Fixed supplied functions produce at most one target per circuit description.

theorem Cslib.Circuits.Circuit.relativeFunctionsAtMost_eq_image {X : Type u_1} {U : Type u_2} {σ : Signature} {n : ℕ} [Fintype σ.Op] [Fintype U] (interpretation : Interpretation σ U) (sources : X → Fin n → U) (m budget : ℕ) : relativeFunctionsAtMost interpretation sources m budget = Finset.image (fun (h : (Fin n → U) → Fin m → U) => h ∘ sources) (functionsAtMost interpretation n m budget)

Relative easy functions are an image of ordinary easy functions.

theorem Cslib.Circuits.Circuit.card_relativeFunctionsAtMost_le_sharpBudget {X : Type u_1} {U : Type u_2} {σ : Signature} {n : ℕ} [Fintype σ.Op] [Fintype U] (interpretation : Interpretation σ U) (sources : X → Fin n → U) (m budget : ℕ) : (relativeFunctionsAtMost interpretation sources m budget).card ≤ σ.sharpBudget n m budget

The factorial-improved count also bounds relative complexity. It counts semantic total extensions before restricting them to the supplied values.

theorem Cslib.Circuits.Circuit.card_relativeFunctionsAtMost_le_min {X : Type u_1} {U : Type u_2} {σ : Signature} {n : ℕ} [Fintype σ.Op] [Fintype U] (interpretation : Interpretation σ U) (sources : X → Fin n → U) (m budget : ℕ) : (relativeFunctionsAtMost interpretation sources m budget).card ≤ min (σ.orderedBudget n m budget) (σ.sharpBudget n m budget)

Either counting bound may be better at a particular finite budget, so their minimum is also a valid bound.

theorem Cslib.Circuits.Circuit.exists_relative_hard_in_family_of_card_lt {X : Type u_1} {σ : Signature} {U : Type u_3} {n m : ℕ} [Fintype σ.Op] (interpretation : Interpretation σ U) (sources : X → Fin n → U) (family : Finset (X → Fin m → U)) (budget : ℕ) (large : (relativeFunctionsAtMost interpretation sources m budget).card < family.card) : ∃ target ∈ family, ↑budget < relativeGateComplexity interpretation target sources

Any upper bound on the easy set gives a hard target in a larger family.

theorem Cslib.Circuits.Circuit.exists_relative_hard_in_family {X : Type u_1} {σ : Signature} {U : Type u_3} {n m : ℕ} [Fintype σ.Op] (interpretation : Interpretation σ U) (sources : X → Fin n → U) (family : Finset (X → Fin m → U)) (budget : ℕ) (large : σ.orderedBudget n m budget < family.card) : ∃ target ∈ family, ↑budget < relativeGateComplexity interpretation target sources

Ordered-description counting against any finite target family.

theorem Cslib.Circuits.Circuit.exists_relative_hard_in_family_sharp {X : Type u_1} {U : Type u_2} {σ : Signature} {n m : ℕ} [Fintype σ.Op] [Fintype U] (interpretation : Interpretation σ U) (sources : X → Fin n → U) (family : Finset (X → Fin m → U)) (budget : ℕ) (large : σ.sharpBudget n m budget < family.card) : ∃ target ∈ family, ↑budget < relativeGateComplexity interpretation target sources

Factorial-improved counting against any finite target family.

theorem Cslib.Circuits.Circuit.exists_relative_hard_for_all_sources {X : Type u_1} {σ : Signature} {U : Type u_3} {n m : ℕ} [Fintype σ.Op] (interpretation : Interpretation σ U) (menu : Finset (X → Fin n → U)) (family : Finset (X → Fin m → U)) (budget : ℕ) (large : menu.card * σ.orderedBudget n m budget < family.card) : ∃ target ∈ family, ∀ sources ∈ menu, ↑budget < relativeGateComplexity interpretation target sources

A sufficiently large family contains a target hard for every source family in a fixed finite menu.

theorem Cslib.Circuits.Circuit.relative_easy_fraction_le {X : Type u_1} {σ : Signature} {U : Type u_3} {n m : ℕ} [Fintype σ.Op] (interpretation : Interpretation σ U) (sources : X → Fin n → U) (family : Finset (X → Fin m → U)) (budget : ℕ) : ↑(family ∩ relativeFunctionsAtMost interpretation sources m budget).card / ↑family.card ≤ ↑(σ.orderedBudget n m budget) / ↑family.card

Exact rational bound for the easy fraction of a finite target family.

theorem Cslib.Circuits.Circuit.relative_easy_fraction_le_sharp {X : Type u_1} {U : Type u_2} {σ : Signature} {n m : ℕ} [Fintype σ.Op] [Fintype U] (interpretation : Interpretation σ U) (sources : X → Fin n → U) (family : Finset (X → Fin m → U)) (budget : ℕ) : ↑(family ∩ relativeFunctionsAtMost interpretation sources m budget).card / ↑family.card ≤ ↑(σ.sharpBudget n m budget) / ↑family.card

The factorial-improved count also bounds the uniform fraction.