sat_recognition_time_bound
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.