defect_moat_zero_iff_sat
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not prove that every circuit fails to decide SAT.
- Does not bound the circuit size needed to cross the moat.
- Does not address the spectral-gap to Turing-machine step translation.
formal statement (Lean)
196theorem defect_moat_zero_iff_sat {n : ℕ} (f : CNFFormula n) :
197 DefectMoat f = 0 ↔ f.isSAT := by
proof body
Term-mode proof.
198 unfold DefectMoat
199 haveI := Classical.propDecidable f.isSAT
200 by_cases h : f.isSAT
201 · simp [h]
202 · simp [h]
203
204/-! ## Part 4: Circuit Cannot Sense the Moat -/
205
206/-- **THEOREM (Circuit Cannot Verify Satisfiability Without Full Input).**
207 For any fixed-view decoder over a proper subset M of variables (|M| < n),
208 there exists a pair (b, R) such that the decoder cannot distinguish the hidden bit.
209
210 This is the BalancedParityHidden adversarial lower bound applied to circuits:
211 any fixed-view decoder over a proper subset of variables can be fooled.
212
213 Consequence: no poly-size circuit (querying < n variables) can correctly
214 decide satisfiability for all n-variable formulas. -/