DefectMoat
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.