DefectMoat
The defect moat for a CNF formula over n variables returns zero when the formula is satisfiable and one when it is unsatisfiable. Researchers reducing the P versus NP question to circuit capacity in Recognition Science cite this quantity to separate satisfiable regions from J-cost obstructions. The definition performs a classical case split on the decidable satisfiability predicate.
claimFor a CNF formula $f$ over $n$ variables, the defect moat is $0$ if $f$ is satisfiable and $1$ otherwise.
background
The Circuit Ledger module treats Boolean circuits as feed-forward sub-ledgers whose local gates lack the global J-cost coupling present in the full Z³ recognition lattice. A CNF formula consists of a list of clauses over n variables. J-cost is the non-negative recognition cost of an assignment, obtained either as the derived cost of a multiplicative recognizer comparator or directly as the J-cost of a recognition event. The module states that every assignment to an unsatisfiable formula incurs J-cost at least 1, creating the defect moat that separates the satisfiable region from the obstruction.
proof idea
The definition installs a classical decidability instance for the satisfiability predicate and returns zero on the true branch and one on the false branch. It is a direct one-line wrapper around the case distinction on satisfiability.
why it matters in Recognition Science
This definition supplies the moat value consumed by the downstream theorem that equates the moat to zero precisely when the formula is satisfiable. It completes Stage 3 of the circuit-ledger analysis, connecting the Z-capacity bound (at most twice the gate count) to the global J-cost gradient required for SAT resolution. The remaining open piece is the spectral-gap to Turing-machine step-count translation that would force exponential depth for any poly-size circuit attempting to cross the moat.
scope and limits
- Does not compute explicit J-cost values for concrete assignments.
- Does not prove any circuit-size lower bound for detecting the moat.
- Does not address the depth overhead needed to simulate global recognition.
formal statement (Lean)
179noncomputable def DefectMoat {n : ℕ} (f : CNFFormula n) : ℕ :=
proof body
Definition body.
180 haveI := Classical.propDecidable f.isSAT
181 if f.isSAT then 0 else 1
182
183/-- **THEOREM (Moat Width for UNSAT).**
184 For an UNSAT formula, every assignment has J-cost ≥ 1. -/