sat_recognition_time
plain-language theorem explainer
For each n > 0 there exists c > 0 such that any decoder from n-bit tapes to a SAT result cannot be fixed by inspecting fewer than n bits. Changing the unread bits can always flip the decoded outcome for any target result. Researchers working on P versus NP inside Recognition Science would cite the claim to separate sublinear computation time from linear recognition time. The entry is a documentation stub with no Lean proof body.
Claim. For every natural number $n > 0$ there exists a positive real $c$ such that for any relation $D$ from $n$-bit assignments to booleans, there is a set $M$ of fewer than $n$ indices where, for every boolean $r$, two assignments agreeing on $M$ exist with $D$ holding for one and failing for the other.
background
The module builds cellular automata gadgets for SAT using local update rules modeled on Rule 110. Tapes are full boolean assignments, Neighborhoods restrict dependence to a fixed radius, and the step function applies a deterministic localRule while preserving reversibility. Computation exploits parallelism for O(n^{1/3} log n) scaling, yet balanced-parity encoding forces recognition to require Ω(n) queries.
proof idea
No proof body is supplied. The declaration acts as a placeholder documenting the intended Tc << Tr separation without constructing the decoder family or deriving the explicit time bounds.
why it matters
The statement underpins the P versus NP resolution by showing recognition time remains linear even when cellular-automaton computation is sublinear. It fits the Recognition Science setting where local rules enable fast parallel evaluation but global readout stays costly. No downstream theorems are recorded and the formalization of the bounds remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.