sat_reaches_zero
plain-language theorem explainer
If a CNF formula over n variables is satisfiable then an assignment exists with zero J-cost. Complexity researchers in the Recognition Science program cite this when separating recognition time from Turing time for SAT. The proof is a term-mode one-liner that extracts the witness from the isSAT hypothesis and applies the zero-cost equivalence.
Claim. Let $f$ be a $k$-CNF formula on $n$ variables. If $f$ is satisfiable, then there exists an assignment $a$ from the $n$ variables to Boolean values such that the J-cost of $f$ under $a$ equals zero, where J-cost equals the number of unsatisfied clauses.
background
In the R̂ SAT encoding, CNFFormula n is a structure holding a list of clauses together with a variable count fixed at n. Assignment n is the type Fin n → Bool. satJCost f a counts the clauses of f that fail to be satisfied by a, so the quantity is zero exactly when a meets every clause. The module documentation states that this encoding lets R̂ act as a non-natural polytime certifier for satisfiable instances while unsatisfiable ones carry a topological obstruction. The upstream lemma satJCost_zero_iff supplies the equivalence between zero J-cost and full satisfaction.
proof idea
The proof is a term-mode one-liner. It obtains the pair (a, ha) directly from the hypothesis h : f.isSAT. It then feeds a into the right-to-left direction of satJCost_zero_iff to replace ha with the equality satJCost f a = 0.
why it matters
This result supplies the constructive witness required by moat_zero_sat and by sat_recognition_time_bound, which together establish that satisfiable formulas reach zero J-cost in at most n recognition steps. It realizes the module's core claim that R̂ separates recognition-time complexity from Turing-machine time for SAT. The theorem therefore sits inside the larger Recognition Science program that derives physical constants and dimensions from the forcing chain while treating complexity distinctions as consequences of the J-cost landscape.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.