moat_width_unsat
An unsatisfiable CNF formula over n variables forces J-cost at least 1 on every assignment. Complexity researchers examining the Recognition Science reduction of P vs NP to circuit capacity would cite this bound when establishing the defect moat. The proof is a direct one-line application of unsat_cost_lower_bound from RSatEncoding.
claimLet $f$ be an unsatisfiable CNF formula on $n$ variables. Then for every assignment $a$, the J-cost satisfies $satJCost(f,a) ≥ 1$.
background
The CircuitLedger module treats Boolean circuits as feed-forward sub-ledgers whose local gates lack global J-cost coupling across the full lattice. CNFFormula n is a structure holding a list of clauses with var_count = n; Assignment n is the type Fin n → Bool. satJCost f a counts the number of clauses unsatisfied by a, so equals zero exactly on satisfying assignments. The upstream unsat_cost_lower_bound states: 'for UNSAT formulas, the minimum J-cost over all assignments is positive (bounded away from zero)'. Module documentation identifies this positive lower bound as the 'defect moat' that separates satisfiable regions from UNSAT obstructions.
proof idea
One-line wrapper that applies unsat_cost_lower_bound f h from RSatEncoding. The lemma already establishes that unsatisfiability implies every assignment leaves at least one clause unsatisfied, and the cast from natural-number length to ℝ yields the integer bound ≥ 1.
why it matters in Recognition Science
Supplies the moat_width component inside circuitLedgerCert and the moat_exists field inside circuitSeparation. It completes the defect-moat stage of the four-stage Circuit Ledger argument, showing that any poly-size circuit with Z-capacity bounded by 2S cannot read enough bits to certify crossing the J-cost barrier. In the broader framework this supports the claim that feed-forward circuits cannot simulate the O(n) global recognition steps performed by the full ledger. It leaves open the spectral-gap to Turing-machine overhead translation required for the final separation.
scope and limits
- Does not apply to satisfiable formulas.
- Does not give an upper bound on J-cost.
- Does not constrain circuit size or depth.
- Does not resolve the full P vs NP separation.
Lean usage
moat_width := fun _n f h => moat_width_unsat f hformal statement (Lean)
185theorem moat_width_unsat {n : ℕ} (f : CNFFormula n) (h : f.isUNSAT) :
186 ∀ a : Assignment n, satJCost f a ≥ 1 :=
proof body
Term-mode proof.
187 unsat_cost_lower_bound f h
188
189/-- **THEOREM (Moat Width for SAT).**
190 For a SAT formula, there exists a zero-cost assignment. -/