moat_zero_sat
plain-language theorem explainer
The theorem establishes that any satisfiable CNF formula admits an assignment with zero J-cost. Researchers working on the P vs NP gap in Recognition Science would cite this result when bounding circuit capacity against the defect moat. The proof is a one-line wrapper that invokes the upstream sat_reaches_zero theorem from RSatEncoding.
Claim. For a CNF formula $f$ over $n$ variables that is satisfiable, there exists an assignment $a$ such that the J-cost of $f$ under $a$ equals zero.
background
In the CircuitLedger module, Boolean circuits are modeled as restricted sub-ledgers without global J-cost coupling across the full lattice. A CNFFormula is a structure holding a list of clauses over $n$ variables, while Assignment is the type Fin $n$ → Bool. The function satJCost counts the number of unsatisfied clauses under a given assignment, so that satJCost $f$ $a$ = 0 precisely when $a$ satisfies every clause.
proof idea
The proof is a one-line wrapper that applies the upstream theorem sat_reaches_zero, which extracts the satisfying assignment from the isSAT witness and confirms that its J-cost is zero.
why it matters
This result supports the defect moat width analysis in the module, where unsatisfiable formulas create a positive J-cost barrier that limited-capacity circuits cannot cross. It fills stage 3 of the module motivation by supplying the complementary zero-cost existence for satisfiable cases, tying directly to the open question of whether poly-size circuits can simulate the global J-cost gradient of the recognition operator R̂. The parent separation structure remains incomplete until the spectral-gap to Turing-step translation is formalized.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.