BooleanCircuitWithEval
plain-language theorem explainer
BooleanCircuitWithEval extends BooleanCircuit n by adjoining an explicit map from n-variable assignments to Boolean outputs. Researchers bounding circuit capacity against the global J-cost gradient in Recognition Science cite this when treating feed-forward structures as restricted sub-ledgers. The declaration is a pure structure extension carrying no proof obligations.
Claim. A Boolean circuit with evaluation over $n$ variables consists of a Boolean circuit (gate count, topological gate list, input-variable references, and output existence) together with a function $eval : Assignment(n) → Bool$ that returns the circuit output on each assignment.
background
The Circuit Ledger module models Boolean circuits as restricted sub-ledgers: feed-forward, locally deterministic structures lacking global J-cost coupling across the Z³ lattice. BooleanCircuit n records gate_count, the Fin-indexed list of gates, the condition that every input gate references a variable in {0,…,n−1}, and the existence of at least one output gate. Assignment n is the type Fin n → Bool (or Var n → Bool in the SAT.CNF sibling), supplying the domain of the added eval field. Upstream constants A = 1 appear in integration-gap and mass-anchor contexts but are not invoked by this structure. The module frames the construction as Stage 1 of the P-vs-NP reduction: circuits simulate only local recognition steps while the full ledger R̂ resolves SAT via global J-cost.
proof idea
This is a structure definition that directly extends BooleanCircuit n by adjoining the eval field. No lemmas or tactics are applied; the declaration simply bundles the parent fields with the new evaluation map.
why it matters
The structure supplies the model required by CircuitWithEvalDecides, which states that a circuit decides a CNF formula when its eval map matches satisfiability on every assignment. Within Recognition Science it advances Stage 1 of the circuit-ledger argument and feeds the subsequent capacity bound CircuitZCapacity c ≤ 2·c.gate_count together with the defect-moat separation for UNSAT instances. The declaration therefore sits inside the chain that isolates the open gap: whether Z-capacity < n forces exponential depth to simulate full moat-crossing verification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.