Depth-sensitive counting

Instead of enumerating circuit syntax, this file closes the set of scalar functions under one operation layer. Every depth-d circuit output belongs to that closure, yielding interpretation-sensitive depth lower bounds.

Semantic closure by depth

noncomputable def Algebraic.Depth.projections {U : Type u_1} [Fintype U] (n : ℕ) : Finset (ScalarFunction U n)

Coordinate projections, which are the scalar functions available at depth zero.

Equations

• Algebraic.Depth.projections n = Finset.image (fun (input : Fin n) (values : Fin n → U) => values input) Finset.univ

def Algebraic.Depth.applyOperation {σ : Signature} {U : Type u_2} {n : ℕ} (interpretation : Interpretation σ U) (op : σ.Op) (arguments : Fin (σ.Arity op) → ScalarFunction U n) : ScalarFunction U n

Pointwise application of one interpreted operation to scalar functions.

Equations

• Algebraic.Depth.applyOperation interpretation op arguments input = interpretation op fun (k : Fin (σ.Arity op)) => arguments k input

noncomputable def Algebraic.Depth.operationClosure {U : Type u_1} {σ : Signature} {n : ℕ} [Fintype σ.Op] [Fintype U] (interpretation : Interpretation σ U) (prior : Finset (ScalarFunction U n)) : Finset (ScalarFunction U n)

Scalar functions obtained by applying one primitive operation to functions from prior.

Equations

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

noncomputable def Algebraic.Depth.functions {U : Type u_1} {σ : Signature} [Fintype σ.Op] [Fintype U] (interpretation : Interpretation σ U) (n a✝ : ℕ) : Finset (ScalarFunction U n)

Scalar functions available by depth d, with projections retained at every layer.

Equations

• Algebraic.Depth.functions interpretation n 0 = Algebraic.Depth.projections n
• Algebraic.Depth.functions interpretation n depth.succ = Algebraic.Depth.projections n ∪ Algebraic.Depth.operationClosure interpretation (Algebraic.Depth.functions interpretation n depth)

@[simp]

theorem Algebraic.Depth.card_projections_le {U : Type u_1} {n : ℕ} [Fintype U] : (projections n).card ≤ n

theorem Algebraic.Depth.card_operationClosure_le {U : Type u_1} {σ : Signature} {n : ℕ} [Fintype σ.Op] [Fintype U] (interpretation : Interpretation σ U) (prior : Finset (ScalarFunction U n)) : (operationClosure interpretation prior).card ≤ σ.lineCount prior.card

theorem Algebraic.Depth.card_functions_succ_le {U : Type u_1} {σ : Signature} [Fintype σ.Op] [Fintype U] (interpretation : Interpretation σ U) (n depth : ℕ) : (functions interpretation n (depth + 1)).card ≤ n + σ.lineCount (functions interpretation n depth).card

theorem Algebraic.Depth.applyOperation_mem_operationClosure {U : Type u_1} {σ : Signature} {n : ℕ} [Fintype σ.Op] [Fintype U] (interpretation : Interpretation σ U) (prior : Finset (ScalarFunction U n)) (op : σ.Op) (arguments : Fin (σ.Arity op) → ScalarFunction U n) (present : ∀ (k : Fin (σ.Arity op)), arguments k ∈ prior) : applyOperation interpretation op arguments ∈ operationClosure interpretation prior

theorem Algebraic.Depth.applyOperation_mem_functions_succ {U : Type u_1} {σ : Signature} {n : ℕ} [Fintype σ.Op] [Fintype U] (interpretation : Interpretation σ U) (depth : ℕ) (op : σ.Op) (arguments : Fin (σ.Arity op) → ScalarFunction U n) (present : ∀ (k : Fin (σ.Arity op)), arguments k ∈ functions interpretation n depth) : applyOperation interpretation op arguments ∈ functions interpretation n (depth + 1)

Applying an operation to depth-d functions produces a depth-d + 1 function.

theorem Algebraic.Depth.operationClosure_mono {U : Type u_1} {σ : Signature} {n : ℕ} [Fintype σ.Op] [Fintype U] (interpretation : Interpretation σ U) : Monotone (operationClosure interpretation)

theorem Algebraic.Depth.projection_mem_functions {U : Type u_1} {σ : Signature} {n : ℕ} [Fintype σ.Op] [Fintype U] (interpretation : Interpretation σ U) (input : Fin n) (depth : ℕ) : (fun (values : Fin n → U) => values input) ∈ functions interpretation n depth

theorem Algebraic.Depth.functions_subset_succ {U : Type u_1} {σ : Signature} [Fintype σ.Op] [Fintype U] (interpretation : Interpretation σ U) (n depth : ℕ) : functions interpretation n depth ⊆ functions interpretation n (depth + 1)

theorem Algebraic.Depth.functions_mono {U : Type u_1} {σ : Signature} [Fintype σ.Op] [Fintype U] (interpretation : Interpretation σ U) (n : ℕ) : Monotone (functions interpretation n)

Soundness for programs and circuits

theorem Cslib.Circuits.Program.gateFunction_mem_depthFunctions {U : Type u_1} {σ : Signature} {n g : ℕ} [Fintype σ.Op] [Fintype U] (program : Program σ n g) (interpretation : Interpretation σ U) (gate : Fin g) : program.gateFunction interpretation gate ∈ Algebraic.Depth.functions interpretation n (program.depths gate)

theorem Cslib.Circuits.Program.wireFunction_mem_depthFunctions {U : Type u_1} {σ : Signature} {n g : ℕ} [Fintype σ.Op] [Fintype U] (program : Program σ n g) (interpretation : Interpretation σ U) (wire : Wire n g) : program.wireFunction interpretation wire ∈ Algebraic.Depth.functions interpretation n (program.wireDepths wire)

theorem Cslib.Circuits.Circuit.outputFunction_mem_depthFunctions {U : Type u_1} {σ : Signature} {n m : ℕ} [Fintype σ.Op] [Fintype U] (circuit : Circuit σ n m) (interpretation : Interpretation σ U) (output : Fin m) : circuit.outputFunction interpretation output ∈ Algebraic.Depth.functions interpretation n (circuit.outputDepths output)

noncomputable def Algebraic.Depth.targets {U : Type u_1} {σ : Signature} [Fintype σ.Op] [Fintype U] (interpretation : Interpretation σ U) (n m depth : ℕ) : Finset (Target U n m)

Multi-output targets assembled from scalar functions available by depth.

Equations

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

theorem Algebraic.Depth.card_targets_le {U : Type u_1} {σ : Signature} [Fintype σ.Op] [Fintype U] (interpretation : Interpretation σ U) (n m depth : ℕ) : (targets interpretation n m depth).card ≤ (functions interpretation n depth).card ^ m

theorem Cslib.Circuits.Circuit.eval_mem_depth_targets {U : Type u_1} {σ : Signature} {n m : ℕ} [Fintype σ.Op] [Fintype U] (circuit : Circuit σ n m) (interpretation : Interpretation σ U) {depth : ℕ} (bounded : circuit.depth ≤ depth) : circuit.eval interpretation ∈ Algebraic.Depth.targets interpretation n m depth

Exact and numeric lower-bound criteria

def Algebraic.Depth.countBound (σ : Signature) [Fintype σ.Op] (n : ℕ) : ℕ → ℕ

Interpretation-independent numeric recurrence bounding the number of scalar functions at each depth.

Equations

• Algebraic.Depth.countBound σ n 0 = n
• Algebraic.Depth.countBound σ n depth.succ = n + σ.lineCount (Algebraic.Depth.countBound σ n depth)

theorem Algebraic.Depth.card_functions_le_countBound {U : Type u_1} {σ : Signature} [Fintype σ.Op] [Fintype U] (interpretation : Interpretation σ U) (n depth : ℕ) : (functions interpretation n depth).card ≤ countBound σ n depth

theorem Algebraic.Depth.card_targets_le_countBound {U : Type u_1} {σ : Signature} [Fintype σ.Op] [Fintype U] (interpretation : Interpretation σ U) (n m depth : ℕ) : (targets interpretation n m depth).card ≤ countBound σ n depth ^ m

theorem Cslib.Circuits.Circuit.exists_depth_hard_in_family {U : Type u_1} {σ : Signature} {n m : ℕ} [Fintype σ.Op] [Fintype U] (interpretation : Interpretation σ U) (family : Finset (Algebraic.Target U n m)) {depth : ℕ} (large : (Algebraic.Depth.functions interpretation n depth).card ^ m < family.card) : ∃ target ∈ family, DepthHard interpretation depth target

A family exceeding the semantic closure count contains a depth-hard target.

theorem Cslib.Circuits.Circuit.exists_depth_hard_in_family_of_countBound {U : Type u_1} {σ : Signature} {n m : ℕ} [Fintype σ.Op] [Fintype U] (interpretation : Interpretation σ U) (family : Finset (Algebraic.Target U n m)) {depth : ℕ} (large : Algebraic.Depth.countBound σ n depth ^ m < family.card) : ∃ target ∈ family, DepthHard interpretation depth target

Purely numeric depth criterion, derived from Depth.countBound.

theorem Cslib.Circuits.Circuit.exists_depth_hard {U : Type u_1} {σ : Signature} {n m : ℕ} [Fintype σ.Op] [Fintype U] (interpretation : Interpretation σ U) {depth : ℕ} (large : (Algebraic.Depth.functions interpretation n depth).card ^ m < Algebraic.Target.count U n m) : ∃ (target : Algebraic.Target U n m), DepthHard interpretation depth target

Full-universe depth lower bound from the exact semantic closure count.

theorem Cslib.Circuits.Circuit.exists_depth_hard_of_countBound {U : Type u_1} {σ : Signature} {n m : ℕ} [Fintype σ.Op] [Fintype U] (interpretation : Interpretation σ U) {depth : ℕ} (large : Algebraic.Depth.countBound σ n depth ^ m < Algebraic.Target.count U n m) : ∃ (target : Algebraic.Target U n m), DepthHard interpretation depth target

Full-universe depth lower bound from the numeric recurrence.

Arity-only recurrence

def Algebraic.Depth.coarseCount (σ : Signature) [Fintype σ.Op] (r n : ℕ) : ℕ → ℕ

Arity-only recurrence bounding the interpretation-independent depth closure.

Equations

• Algebraic.Depth.coarseCount σ r n 0 = n
• Algebraic.Depth.coarseCount σ r n depth.succ = n + Fintype.card σ.Op * (Algebraic.Depth.coarseCount σ r n depth + 1) ^ r

theorem Algebraic.Depth.countBound_le_coarseCount (σ : Signature) [Fintype σ.Op] {r : ℕ} (arity : σ.ArityAtMost r) (n depth : ℕ) : countBound σ n depth ≤ coarseCount σ r n depth

theorem Cslib.Circuits.Circuit.exists_depth_hard_in_family_coarse {U : Type u_1} {σ : Signature} {n m : ℕ} [Fintype σ.Op] [Fintype U] (interpretation : Interpretation σ U) (family : Finset (Algebraic.Target U n m)) {r depth : ℕ} (arity : σ.ArityAtMost r) (large : Algebraic.Depth.coarseCount σ r n depth ^ m < family.card) : ∃ target ∈ family, DepthHard interpretation depth target

theorem Cslib.Circuits.Circuit.exists_boolean_depth_hard_coarse {σ : Signature} {n m : ℕ} [Fintype σ.Op] (interpretation : Interpretation σ Bool) {r depth : ℕ} (arity : σ.ArityAtMost r) (large : Algebraic.Depth.coarseCount σ r n depth ^ m < Algebraic.Target.count Bool n m) : ∃ (target : Algebraic.Target Bool n m), DepthHard interpretation depth target

Boolean specialization of the arity-only depth recurrence.