CircuitBondCount
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.