defect_moat_zero_iff_sat
plain-language theorem explainer
A CNF formula over n variables has defect moat zero exactly when it admits a satisfying assignment. Researchers reducing P versus NP inside Recognition Science cite the equivalence to separate local circuit reach from global ledger J-cost. The argument unfolds the moat definition, invokes decidability of satisfiability, splits cases, and simplifies each branch.
Claim. For any natural number $n$ and CNF formula $f$ on $n$ variables, the defect moat of $f$ equals zero if and only if $f$ is satisfiable.
background
The CircuitLedger module treats Boolean circuits as feed-forward sub-ledgers whose gates see only local parents and therefore lack the global J-cost gradient available to the full Recognition ledger. A CNFFormula is a list of clauses together with a variable count; its isSAT predicate decides existence of an assignment making every clause true. The DefectMoat definition returns 0 precisely on satisfiable formulas and 1 otherwise, encoding the fact (proved upstream in RSatEncoding) that every assignment on an unsatisfiable formula carries J-cost at least 1.
proof idea
The term proof unfolds DefectMoat, installs classical decidability for the isSAT predicate, performs case analysis on whether the formula is satisfiable, and applies simp in each branch. The positive case reduces both sides to true; the negative case reduces both sides to false.
why it matters
The theorem supplies the exact numerical meaning of the defect moat inside the four-stage P-versus-NP argument of the module. It directly enables the later claim that circuits cannot sense the moat (via BalancedParityHidden) and therefore cannot decide SAT in polynomial size. The result sits at Stage 3 of the reduction; the remaining open piece is the translation from Z-capacity deficit to exponential depth overhead.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.