CircuitWithEvalDecides
plain-language theorem explainer
CircuitWithEvalDecides encodes the condition that a circuit equipped with a bundled evaluation map matches a CNF formula's satisfiability predicate on every assignment. Researchers analyzing circuit capacity and defect moat arguments in the Recognition Science treatment of P versus NP cite this predicate when contrasting concrete evaluation models against existential decision predicates. The definition is a direct universal quantification over assignments that equates circuit output to the formula satisfaction check.
Claim. A circuit $c$ equipped with an evaluation map decides a CNF formula $f$ precisely when, for every assignment $a$ of the $n$ variables, the value $c(a)$ equals the truth value of whether $f$ is satisfied by $a$.
background
In the Circuit Ledger module, Boolean circuits appear as restricted sub-ledgers lacking global J-cost coupling across the full lattice. BooleanCircuitWithEval extends the base circuit structure by bundling an explicit evaluation map from assignments to Boolean values, avoiding gate-by-gate wiring details. An Assignment is a function from Fin n to Bool, while CNFFormula packages a list of clauses over n variables. The module frames the P versus NP gap as the question whether a feed-forward circuit of polynomial size can simulate the global recognition steps that resolve SAT in linear time.
proof idea
The definition is the direct statement of universal agreement between the bundled evaluation function and the satisfiability predicate on all assignments. It serves as the universal counterpart to the existential CircuitDecides predicate defined later in the module.
why it matters
This definition supports the analysis of circuit capacity bounds and defect moat arguments in the Recognition Science reduction of P versus NP. It distinguishes the concrete evaluation model from the abstract existential decision model used for compatibility with later capacity checks. The module's stage 1 treats circuits as feed-forward sub-ledgers, and this predicate enables the Z-capacity bounds and moat-crossing obstructions developed in subsequent declarations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.