CircuitDecides
plain-language theorem explainer
The definition asserts that a Boolean circuit decides a CNF formula precisely when an evaluation function exists that reproduces the formula's satisfiability on every assignment. Researchers formalizing circuit complexity bounds within Recognition Science cite this to distinguish restricted sub-ledgers from the full ledger. The definition proceeds by direct existential quantification over the space of assignment-to-Boolean maps.
Claim. A Boolean circuit on $n$ variables decides a CNF formula on the same variables if there exists a map from assignments to Booleans such that the map agrees with the satisfiability predicate of the formula for every assignment.
background
The structure for a Boolean circuit models a feed-forward circuit as a restricted sub-ledger consisting of a total gate count, gates listed in topological order, input variable mappings, and an output gate requirement. This enforces local determinism and bounds the reach by circuit depth, without global coupling across the three-dimensional lattice. The CNF formula structure packages clauses over a fixed number of variables, and an assignment is a function assigning truth values to each variable.
proof idea
The declaration is a direct definition. It sets the property to hold exactly when an evaluation function from assignments to Booleans exists that matches the formula's satisfiability check on all inputs.
why it matters
This definition provides the interface for the conditional circuit lower bounds. It is invoked in the algebraic lower bound theorem, which concludes linear size at least $n$ for circuits deciding unsatisfiable formulas under the algebraic restriction hypothesis. It also supports the topological lower bound and the conditional separation of P from NP under uniform topological obstruction. In the Recognition Science framework, it contributes to stage one of the circuit ledger analysis, highlighting the gap between local feed-forward computation and the global recognition needed to cross the defect moat for unsatisfiable instances. The open question remains the formal link from spectral gap to Turing machine step count that would force exponential depth.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.