sat_reaches_zero
plain-language theorem explainer
If a CNF formula over n variables is satisfiable then there exists an assignment a such that the J-cost of the formula under a equals zero. Researchers examining the R̂ recognition operator in complexity would cite this for its constructive witness on satisfiable instances. The proof extracts the witness from the satisfiability hypothesis and applies the zero-cost equivalence.
Claim. Let $f$ be a CNF formula on $n$ variables. If $f$ is satisfiable, then there exists an assignment $a :$ Fin $n$ $→$ Bool such that the J-cost of $f$ under $a$ equals zero.
background
CNFFormula n is a structure containing a list of clauses and a proof that var_count equals n. Assignment n is the type Fin n → Bool. satJCost f a counts the unsatisfied clauses under a. The upstream theorem satJCost_zero_iff states that this count is zero precisely when a satisfies all clauses of f.
proof idea
The proof is term-mode. It obtains the satisfying assignment a together with ha from the hypothesis that f is satisfiable, then applies the right-to-left direction of satJCost_zero_iff to ha.
why it matters
This supplies the constructive zero-cost witness for satisfiable formulas and is invoked by moat_zero_sat to equate the moat value with satisfiability. It is also used by sat_recognition_time_bound to bound recognition steps by n. The result completes the satisfiable half of the partial theorem on R̂ SAT encoding, where recognition time separates from Turing computation time.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.