DefectMoat
plain-language theorem explainer
DefectMoat returns 0 for satisfiable CNF formulas and 1 for unsatisfiable ones. Researchers bounding circuit capacity against the global J-cost gradient in Recognition Science cite this when showing poly-size circuits cannot sense the full moat. The definition performs a direct case split on the isSAT predicate after invoking classical decidability.
Claim. Let $f$ be a CNF formula on $n$ variables. Define the defect moat $D(f) := 0$ if $f$ is satisfiable and $D(f) := 1$ otherwise.
background
The Circuit Ledger module treats Boolean circuits as feed-forward sub-ledgers with only local parent connections and no global J-cost coupling across the Z³ lattice. CNFFormula is the structure holding a list of clauses together with a variable count. The defect moat is the binary indicator of whether a satisfying assignment exists, drawn from the J-cost definition in ObserverForcing where cost of a recognition event equals its J-cost.
proof idea
One-line definition that first obtains decidability of isSAT via Classical.propDecidable, then returns 0 or 1 by direct if-then on the boolean value.
why it matters
Supplies the numerical value consumed by the downstream theorem defect_moat_zero_iff_sat that equates the moat to zero precisely when the formula is satisfiable. It implements Stage 3 of the module's four-stage argument separating satisfiable from unsatisfiable regions. In the Recognition Science framework it links the J-cost gradient (T5) and RCL to circuit capacity bounds, leaving open the spectral-gap-to-TM-overhead translation required for the full P vs NP separation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.