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

BooleanCircuit

show as:
view Lean formalization →

BooleanCircuit n encodes a feed-forward Boolean circuit over n inputs as a restricted sub-ledger with local DAG wiring and no global lattice coupling. Researchers formalizing the Recognition Science P versus NP gap cite this structure to derive polynomial Z-capacity bounds from gate count. The definition is a direct structural bundle of gate count, topological gate map, input-variable constraint, and output existence, with no separate proof steps.

claimA Boolean circuit over $n$ input variables is a structure with gate count $S$, a map from each index in Fin $S$ to a gate of type Gate $S$, a predicate ensuring every input-type gate references one variable in Fin $n$, and an existence witness for at least one output-type gate.

background

The module treats Boolean circuits as Stage 1 of the P versus NP reduction in Recognition Science: a feed-forward sub-ledger whose reach is bounded by depth rather than the global J-cost gradient of the full R̂ ledger. GateType is the inductive type with constructors Input (leaf reading one variable), And, Or, Not, and Output. Gate S packages a gate type together with a list of at most two parent indices, each strictly smaller than the current index to enforce the DAG property. Upstream LedgerFactorization supplies the J-cost calibration that later stages contrast with the circuit's local bond count.

proof idea

This is a structural definition; the fields gate_count, gates, input_var, and has_output are declared directly with their types and predicates. No tactics or lemmas are applied beyond the sibling Gate structure that already encodes arity_le and ff_bound.

why it matters in Recognition Science

BooleanCircuit supplies the base type for BooleanCircuitWithEval, CircuitBondCount, circuit_bond_count_le, and circuit_capacity_bound, which together prove that any circuit of size S has Z-capacity at most 2S. It therefore anchors the module's claim that polynomial-size circuits remain polynomially bounded in Z-complexity, feeding CircuitLedgerCert and the defect-moat separation argument. The open piece remains the translation from spectral gap to Turing-machine step count that would close the exponential-depth requirement.

scope and limits

Lean usage

theorem capacity_example {n : ℕ} (c : BooleanCircuit n) : CircuitZCapacity c ≤ 2 * c.gate_count := circuit_capacity_bound c

formal statement (Lean)

  96structure BooleanCircuit (n : ℕ) where
  97  /-- Total number of gates (inputs + internal + output) -/
  98  gate_count : ℕ
  99  /-- The gates in topological order -/
 100  gates : Fin gate_count → Gate gate_count
 101  /-- Input gates each reference one variable in {0,..,n-1} -/
 102  input_var : ∀ i : Fin gate_count,
 103    (gates i).gtype = GateType.Input → ∃ _v : Fin n, True
 104  /-- At least one output gate exists -/
 105  has_output : ∃ i : Fin gate_count, (gates i).gtype = GateType.Output
 106
 107/-- The size of a circuit is its gate count. -/
 108def BooleanCircuit.size {n : ℕ} (c : BooleanCircuit n) : ℕ := c.gate_count

proof body

Definition body.

 109
 110/-- A Boolean circuit computes a specific Boolean function determined by its
 111    gate structure and input wiring. We model this as a bundled function field
 112    rather than implementing gate-by-gate evaluation (which would require
 113    enriching BooleanCircuit with explicit input wiring). -/

used by (17)

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

depends on (21)

Lean names referenced from this declaration's body.