Circuit dependency graphs

This module exposes the circuit DAG as a finite directed graph. Vertices are primary inputs, internal gates, and output gates. Edges point from each referenced wire to the gate that reads it.

Main results

• Circuit.dependencyGraph_adj_val_lt -- every edge follows the circuit's canonical index order.
• Circuit.dependencyGraph_isAcyclic -- the dependency graph is acyclic.
• Circuit.dependencyGraph_edge_card_le_totalFanIn -- distinct edges are bounded by total fan-in.

@[simp]

theorem Complexity.Circuit.dependencyGraph_adj_iff {B : Basis} {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit B N M G) {source target : Fin (N + G + M)} : c.dependencyGraph.Adj source target ↔ (source, target) ∈ c.dependencyEdges

Dependency-graph adjacency is membership in the finite edge set.

theorem Complexity.Circuit.dependencyGraph_adj_val_lt {B : Basis} {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit B N M G) {source target : Fin (N + G + M)} (edge : c.dependencyGraph.Adj source target) : ↑source < ↑target

Every dependency edge points from a smaller to a larger vertex index.

theorem Complexity.Circuit.dependencyGraph_isAcyclic {B : Basis} {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit B N M G) : c.dependencyGraph.IsAcyclic

The dependency graph of every well-formed circuit is acyclic.

@[simp]

theorem Complexity.Circuit.dependencyGraph_edgeFinset {B : Basis} {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit B N M G) : c.dependencyGraph.edgeFinset = c.dependencyEdges

The generic graph edge enumeration recovers the circuit edge set.

theorem Complexity.Circuit.dependencyGraph_edge_card_le_totalFanIn {B : Basis} {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit B N M G) : c.dependencyGraph.edgeFinset.card ≤ c.totalFanIn

The number of distinct dependency edges is at most total fan-in.

The inequality can be strict because multiple inputs of one gate may read the same wire, while a digraph stores only one copy of an edge.