sat_recognition_time_bound
For any satisfiable CNF formula over n variables the recognition operator reaches a zero J-cost assignment in at most n steps. Researchers studying recognition-time complexity and non-Turing models would cite this to separate R̂-polytime SAT from Turing time. The proof extracts a zero-cost assignment from the isSAT hypothesis and pairs it with the trivial bound n.
claimLet $f$ be a satisfiable CNF formula over $n$ variables. Then there exist a natural number $k$ with $k ≤ n$ and an assignment $a$ of truth values to the variables such that the J-cost of $f$ under $a$ equals zero.
background
In the R̂ SAT encoding module a CNFFormula n consists of a list of clauses together with a variable count equal to n, while an Assignment n is a function Fin n → Bool. The function satJCost f a returns the number of unsatisfied clauses under a, hence equals zero precisely when a satisfies every clause. The module states that the Recognition Science operator R̂ supplies a non-natural polytime certifier for SAT: satisfiable instances reach zero J-cost in O(n) steps while unsatisfiable instances exhibit a topological obstruction. This theorem rests on the upstream result sat_reaches_zero, which asserts that satisfiability implies existence of an assignment with satJCost equal to zero.
proof idea
The proof is a one-line term-mode wrapper. It applies sat_reaches_zero to the satisfiability hypothesis to obtain an assignment a with satJCost f a = 0, then uses le_refl to witness the bound steps ≤ n.
why it matters in Recognition Science
This supplies the constructive O(n) bound for satisfiable instances that is instantiated inside circuitSeparation and dissolution_holds. It completes the first half of the partial theorem recorded in the module documentation: satisfiable instances reach zero cost in O(n) steps. Within the Recognition framework the result shows that recognition time for SAT is linear in the variable count, thereby separating the R̂ model from standard Turing computation time without resolving P versus NP.
scope and limits
- Does not establish any sublinear recognition bound.
- Does not apply to unsatisfiable formulas.
- Does not supply an explicit search algorithm beyond existence.
- Does not prove P ≠ NP for Turing machines.
Lean usage
let ⟨steps, a, hle, ha⟩ := sat_recognition_time_bound f hformal statement (Lean)
129theorem sat_recognition_time_bound {n : ℕ} (f : CNFFormula n) (h : f.isSAT) :
130 ∃ (steps : ℕ) (a : Assignment n),
131 steps ≤ n ∧ satJCost f a = 0 := by
proof body
Term-mode proof.
132 obtain ⟨a, ha⟩ := sat_reaches_zero f h
133 exact ⟨n, a, le_refl _, ha⟩
134
135/-! ## Part 2: Unsatisfiable → Topological Obstruction -/
136
137/-- For an unsatisfiable formula, every assignment has J-cost > 0.
138 This means the J-cost landscape has no zero-cost point = topological obstruction. -/