sat_reaches_zero
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove P = NP for Turing machines.
- Applies only when the input formula is satisfiable.
- Recognition steps are counted in the R̂ model, not classical algorithms.
- Does not address fixed-k hardness or approximation ratios.
Lean usage
theorem moat_zero_sat {n : ℕ} (f : CNFFormula n) (h : f.isSAT) : ∃ a : Assignment n, satJCost f a = 0 := sat_reaches_zero f hformal statement (Lean)
123theorem sat_reaches_zero {n : ℕ} (f : CNFFormula n) (h : f.isSAT) :
124 ∃ a : Assignment n, satJCost f a = 0 := by
proof body
Term-mode proof.
125 obtain ⟨a, ha⟩ := h
126 exact ⟨a, (satJCost_zero_iff f a).mpr ha⟩
127
128/-- The recognition time for a satisfiable formula is ≤ n (variable count). -/