defect_moat_zero_iff_sat
plain-language theorem explainer
The defect moat of a CNF formula equals zero exactly when the formula is satisfiable. Researchers formalizing the Recognition Science separation between circuit reach and global J-cost resolution would cite this equivalence to anchor the moat construction. The proof proceeds by unfolding the definition of the moat, invoking classical decidability of satisfiability, and simplifying after a case split on the satisfiability predicate.
Claim. Let $f$ be a CNF formula over $n$ variables. The defect moat value of $f$ equals zero if and only if $f$ is satisfiable.
background
In the Circuit Ledger module, Boolean circuits are modeled as feed-forward sub-ledgers whose gates see only local parents and lack the global J-cost coupling present in the full recognition ledger. The DefectMoat for a formula $f$ is defined to return 0 when $f$ is satisfiable and 1 otherwise, with the UNSAT case resting on the prior result that every assignment then carries J-cost at least 1. CNFFormula is the structure holding a list of clauses together with a variable count that matches $n$. This equivalence sits inside Stage 3 of the module's four-stage argument that poly-size circuits cannot verify satisfiability without reading all input bits.
proof idea
The term proof first unfolds the definition of DefectMoat. It then obtains a classical decidability instance for the satisfiability predicate and performs a by_cases split on whether the formula is satisfiable. Each branch is discharged by a single simp application that substitutes the known truth value into the conditional definition.
why it matters
This theorem supplies the exact numerical meaning of the defect moat that later arguments use to show circuits cannot sense which side of the moat they occupy. It directly supports the module's Stage 3 claim that a proper subset of variables leaves the decoder unable to distinguish satisfiable from unsatisfiable instances, citing the BalancedParityHidden lower bound. The result closes the basic equivalence needed before the open question of Z-capacity bounds forcing exponential depth can be addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.