Shannon counting bounds

Exact ordered-syntax counts are converted here into semantic bounds for an arbitrary finite interpretation and an arbitrary finite family of targets.

@[reducible, inline]

abbrev Algebraic.BoundedCircuit (σ : Signature) (n m G : ℕ) : Type u_1

A circuit with a gate count chosen from 0, ..., G.

Equations

• Algebraic.BoundedCircuit σ n m G = ((g : Fin (G + 1)) × { circuit : Cslib.Circuits.Circuit σ n m // circuit.size = ↑g })

def Algebraic.BoundedCircuit.eval {σ : Signature} {n m G : ℕ} {U : Type u_2} (circuit : BoundedCircuit σ n m G) (interpretation : Interpretation σ U) : Target U n m

Evaluate a circuit whose internal gate count is bounded by G.

Equations

• circuit.eval interpretation = (↑circuit.snd).eval interpretation

noncomputable def Cslib.Circuits.Circuit.functionsAtMost {U : Type u_1} {σ : Signature} [Fintype σ.Op] [Fintype U] (interpretation : Interpretation σ U) (n m G : ℕ) : Finset (Algebraic.Target U n m)

Functions computed by circuits with at most G internal gates.

Equations

• Cslib.Circuits.Circuit.functionsAtMost interpretation n m G = Finset.image (fun (circuit : Algebraic.BoundedCircuit σ n m G) => circuit.eval interpretation) Finset.univ

def Cslib.Circuits.Signature.orderedBudget (σ : Signature) [Fintype σ.Op] (n m G : ℕ) : ℕ

Number of topologically ordered circuit descriptions with at most G internal gates.

Equations

• σ.orderedBudget n m G = ∑ g ∈ Finset.range (G + 1), (∏ j ∈ Finset.range g, σ.lineCount (n + j)) * (n + g) ^ m

theorem Cslib.Circuits.Circuit.mem_functionsAtMost_iff {U : Type u_1} {σ : Signature} {n m G : ℕ} [Fintype σ.Op] [Fintype U] {interpretation : Interpretation σ U} {target : Algebraic.Target U n m} : target ∈ functionsAtMost interpretation n m G ↔ ∃ (circuit : Circuit σ n m), circuit.size ≤ G ∧ circuit.ComputesWith interpretation target

theorem Cslib.Circuits.Circuit.not_mem_functionsAtMost_iff {U : Type u_1} {σ : Signature} {n m G : ℕ} [Fintype σ.Op] [Fintype U] {interpretation : Interpretation σ U} {target : Algebraic.Target U n m} : target ∉ functionsAtMost interpretation n m G ↔ GateHard interpretation G target

Being absent from the easy-function set is exactly gate hardness at the corresponding budget.

theorem Algebraic.BoundedCircuit.card {σ : Signature} {n m G : ℕ} [Fintype σ.Op] : Fintype.card (BoundedCircuit σ n m G) = σ.orderedBudget n m G

Exact number of ordered circuits with at most G internal gates.

theorem Cslib.Circuits.Circuit.card_functionsAtMost_le {U : Type u_1} {σ : Signature} {n m G : ℕ} [Fintype σ.Op] [Fintype U] (interpretation : Interpretation σ U) : (functionsAtMost interpretation n m G).card ≤ σ.orderedBudget n m G

Semantic functions are no more numerous than their ordered descriptions.

theorem Cslib.Circuits.Circuit.exists_hard_in_family_of_card_lt {U : Type u_1} {σ : Signature} {n m G : ℕ} [Fintype σ.Op] [Fintype U] (interpretation : Interpretation σ U) (family : Finset (Algebraic.Target U n m)) (large : (functionsAtMost interpretation n m G).card < family.card) : ∃ target ∈ family, GateHard interpretation G target

Any family larger than the set of functions available within budget contains a target outside that budget.

theorem Cslib.Circuits.Circuit.exists_hard_of_card_lt {U : Type u_1} {σ : Signature} {n m G : ℕ} [Fintype σ.Op] [Fintype U] (interpretation : Interpretation σ U) (small : (functionsAtMost interpretation n m G).card < Algebraic.Target.count U n m) : ∃ (target : Algebraic.Target U n m), GateHard interpretation G target

If the easy functions do not fill the whole target space, some target lies outside the gate budget.

theorem Cslib.Circuits.Circuit.exists_hard_in_family {U : Type u_1} {σ : Signature} {n m G : ℕ} [Fintype σ.Op] [Fintype U] (interpretation : Interpretation σ U) (family : Finset (Algebraic.Target U n m)) (large : σ.orderedBudget n m G < family.card) : ∃ target ∈ family, GateHard interpretation G target

A family larger than the ordered-syntax budget contains a hard target.