CircuitBondCount
CircuitBondCount sums the lengths of parent lists across all gates in a BooleanCircuit to obtain the total wire count. Researchers bounding Z-complexity capacity for feed-forward circuits in Recognition Science cite this definition when establishing that poly-size circuits cannot cross defect moats. The definition is realized directly as a Finset sum of parent lengths with no additional lemmas.
claimLet $c$ be a Boolean circuit with $n$ inputs and $S$ gates in topological order. The bond count of $c$ is the sum over all gates $g_i$ of the number of parents of $g_i$, written $B(c) = |E|$, where $E$ is the set of parent-to-child edges.
background
The Circuit Ledger module treats Boolean circuits as restricted sub-ledgers: feed-forward, locally deterministic structures lacking global J-cost coupling across the full Z³ lattice. The BooleanCircuit structure records gate_count, a Fin-indexed array of gates, input variable references for input gates, and the existence of at least one output gate. Bond count is introduced to quantify the total number of wires (parent-child edges) that determine the topological invariants a circuit can represent.
proof idea
This is a one-line definition that applies Finset.univ.sum to the function extracting the length of the parents list for each gate index.
why it matters in Recognition Science
CircuitBondCount supplies the quantity used to define CircuitZCapacity and to prove the bound CircuitBondCount c ≤ 2 * c.gate_count. It implements Stage 2 of the module's formalization of the P vs NP gap in Recognition Science, showing that a circuit of size S has Z-complexity capacity at most 2S and therefore cannot read the full n-bit information required to cross the defect moat established in RSatEncoding.
scope and limits
- Does not incorporate global J-cost gradients present in the full ledger.
- Does not bound circuit depth or Turing simulation overhead.
- Does not apply to cyclic or non-Boolean graphs.
- Does not compute satisfiability or recognition step counts.
Lean usage
theorem capacity_bound {n : ℕ} (c : BooleanCircuit n) : CircuitBondCount c ≤ 2 * c.gate_count := circuit_bond_count_le cformal statement (Lean)
136def CircuitBondCount {n : ℕ} (c : BooleanCircuit n) : ℕ :=
proof body
Definition body.
137 Finset.univ.sum (fun i => (c.gates i).parents.length)
138
139/-- Bond count is bounded by 2 × gate_count (each gate has ≤ 2 parents). -/