pith. machine review for the scientific record. sign in
def definition def or abbrev high

CircuitZCapacity

show as:
view Lean formalization →

CircuitZCapacity maps each Boolean circuit over n variables to the total number of bonds in its gate graph, serving as the measure of Z-complexity capacity in the Recognition Science ledger model. Researchers bounding circuit information content for the P versus NP gap cite this definition when showing polynomial-size circuits remain polynomially bounded. The definition is realized as a direct one-line alias to the CircuitBondCount summation over parent references.

claimFor a Boolean circuit $c$ with $n$ input variables, the Z-complexity capacity equals the total number of parent-child wires (bonds) in the circuit graph.

background

In the Circuit Ledger module Boolean circuits are treated as restricted sub-ledgers: feed-forward, locally deterministic structures with no global J-cost coupling across the Z³ lattice. The structure BooleanCircuit n records gate_count, a topologically ordered list of gates, input variable references for each input gate, and the existence of at least one output gate. Z-complexity capacity is introduced as the topological charge carried by the bond graph of these gates. Upstream CircuitBondCount defines the bond total as the sum, over all gates, of the length of each gate's parent list, with the immediate bound that this sum is at most twice the gate count.

proof idea

This is a one-line wrapper that directly returns CircuitBondCount c, inheriting the summation over gate parents from that definition.

why it matters in Recognition Science

The definition supplies the capacity measure used by the Circuit Capacity Bound theorem, which states that any circuit of size S has Z-capacity at most 2S and therefore that polynomial-size circuits have polynomial Z-capacity. It is referenced inside CircuitLedgerCert and the CircuitSeparation structure that contrast the O(n) recognition steps of the full ledger against the local reach of circuits. In the RS framework it operationalizes the restriction of sub-ledgers to local reach, contrasting with the global J-cost gradient resolved by T5 J-uniqueness and the Recognition Composition Law. The remaining open gap is the translation from Z-capacity deficit to required exponential depth overhead.

scope and limits

formal statement (Lean)

 154def CircuitZCapacity {n : ℕ} (c : BooleanCircuit n) : ℕ :=

proof body

Definition body.

 155  CircuitBondCount c
 156
 157/-- **THEOREM (Circuit Capacity Bound).**
 158    A Boolean circuit of size S has Z-complexity capacity at most 2S.
 159
 160    The significance: a polynomial-size circuit (S = poly(n)) has
 161    Z-capacity at most 2·poly(n) = poly(n). -/

used by (4)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (15)

Lean names referenced from this declaration's body.