Counting with a fixed supplied family

For any fixed supplied : U^n → U^k, the number of targets with conditional gate complexity at most budget is bounded by the number of circuit descriptions on n + k inputs. The bound is independent of the complexity of supplied. Dividing by the size of a nonempty target family gives a bound on the probability that a uniformly sampled target is conditionally easy.

The supplied family is fixed before choosing the target. In particular, these statements do not bound an adversarial choice supplied = target.

noncomputable def Cslib.Circuits.Circuit.conditionalFunctionsAtMost {σ : Signature} {U : Type u_2} {n k : ℕ} [Fintype σ.Op] (interpretation : Interpretation σ U) (supplied : Algebraic.Target U n k) (m budget : ℕ) : Finset (Algebraic.Target U n m)

All targets computable within a gate budget from a fixed supplied family.

Equations

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

theorem Cslib.Circuits.Circuit.mem_conditionalFunctionsAtMost_iff {σ : Signature} {U : Type u_2} {n k m : ℕ} [Fintype σ.Op] (interpretation : Interpretation σ U) (supplied : Algebraic.Target U n k) (target : Algebraic.Target U n m) (budget : ℕ) : target ∈ conditionalFunctionsAtMost interpretation supplied m budget ↔ conditionalGateComplexity interpretation target supplied ≤ ↑budget

Membership in the counted set is exactly a conditional complexity bound.

theorem Cslib.Circuits.Circuit.card_conditionalFunctionsAtMost_le {σ : Signature} {U : Type u_2} {n k : ℕ} [Fintype σ.Op] (interpretation : Interpretation σ U) (supplied : Algebraic.Target U n k) (m budget : ℕ) : (conditionalFunctionsAtMost interpretation supplied m budget).card ≤ σ.orderedBudget (n + k) m budget

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

theorem Cslib.Circuits.Circuit.card_conditionalFunctionsAtMost_le_sharpBudget {U : Type u_1} {σ : Signature} {n k : ℕ} [Fintype σ.Op] [Fintype U] (interpretation : Interpretation σ U) (supplied : Algebraic.Target U n k) (m budget : ℕ) : (conditionalFunctionsAtMost interpretation supplied m budget).card ≤ σ.sharpBudget (n + k) m budget

The factorial-improved semantic count also bounds conditional complexity.

theorem Cslib.Circuits.Circuit.exists_conditional_hard_in_family {σ : Signature} {U : Type u_2} {n k m : ℕ} [Fintype σ.Op] (interpretation : Interpretation σ U) (supplied : Algebraic.Target U n k) (family : Finset (Algebraic.Target U n m)) (budget : ℕ) (large : σ.orderedBudget (n + k) m budget < family.card) : ∃ target ∈ family, ↑budget < conditionalGateComplexity interpretation target supplied

Any target family larger than the circuit budget contains a function that remains hard after supplying supplied.

theorem Cslib.Circuits.Circuit.exists_conditional_hard_in_family_sharp {U : Type u_1} {σ : Signature} {n k m : ℕ} [Fintype σ.Op] [Fintype U] (interpretation : Interpretation σ U) (supplied : Algebraic.Target U n k) (family : Finset (Algebraic.Target U n m)) (budget : ℕ) (large : σ.sharpBudget (n + k) m budget < family.card) : ∃ target ∈ family, ↑budget < conditionalGateComplexity interpretation target supplied

Factorial-improved counting yields a conditionally hard target.

theorem Cslib.Circuits.Circuit.exists_conditional_hard {U : Type u_1} {σ : Signature} {n k : ℕ} [Fintype σ.Op] [Fintype U] (interpretation : Interpretation σ U) (supplied : Algebraic.Target U n k) (m budget : ℕ) (small : σ.orderedBudget (n + k) m budget < Nat.card U ^ (m * Nat.card U ^ n)) : ∃ (target : Algebraic.Target U n m), ↑budget < conditionalGateComplexity interpretation target supplied

Counting over the entire truth-table space yields a conditionally hard target.

theorem Cslib.Circuits.Circuit.exists_conditional_hard_for_all_given {σ : Signature} {U : Type u_2} {n k m : ℕ} [Fintype σ.Op] (interpretation : Interpretation σ U) (menu : Finset (Algebraic.Target U n k)) (family : Finset (Algebraic.Target U n m)) (budget : ℕ) (large : menu.card * σ.orderedBudget (n + k) m budget < family.card) : ∃ target ∈ family, ∀ supplied ∈ menu, ↑budget < conditionalGateComplexity interpretation target supplied

A finite menu of supplied families costs only a multiplicative factor in counting. A sufficiently large target family has a member hard for every choice from the menu, even if that choice is made after seeing the target.

theorem Cslib.Circuits.Circuit.conditional_easy_fraction_le {σ : Signature} {U : Type u_2} {n k m : ℕ} [Fintype σ.Op] (interpretation : Interpretation σ U) (supplied : Algebraic.Target U n k) (family : Finset (Algebraic.Target U n m)) (budget : ℕ) : ↑(family ∩ conditionalFunctionsAtMost interpretation supplied m budget).card / ↑family.card ≤ ↑(σ.orderedBudget (n + k) m budget) / ↑family.card

Probability bound for a uniformly sampled member of a nonempty target family, expressed as an exact rational cardinality ratio. The supplied family is fixed independently of this sampling.