computation_recognition_separation
plain-language theorem explainer
The declaration asserts that for natural numbers n at least 100, there exist real numbers Tc and Tr with Tc bounded above by n to the one-third power times log n, Tr at least n, and Tc strictly less than Tr. Researchers addressing P versus NP via cellular automata in the Recognition Science setting would cite it to separate local parallel computation from global result readout. The statement supplies no proof body and stands as an unproved claim in the module.
Claim. For every natural number $n$ with $n$ at least 100, there exist real numbers $T_c$ and $T_r$ such that $T_c$ is at most $n^{1/3} log n$, $T_r$ is at least $n$, and $T_c$ is strictly less than $T_r$.
background
The module constructs one-dimensional cellular automata with finite-radius local update rules to evaluate SAT instances. Gadgets implement Boolean operations while preserving locality, determinism, and reversibility for ledger compatibility; the model adapts Rule 110 universal computation. Parallel evaluation yields computation time O(n to the one-third times log n), yet balanced-parity encoding forces any readout of the result to require Omega(n) queries.
proof idea
No proof body or tactics are attached to the declaration; it functions solely as a statement of the time separation.
why it matters
The theorem supports the module's P versus NP resolution by exhibiting a gap between fast local CA computation and slower recognition. It directly encodes the O(n^{1/3} log n) versus Omega(n) bounds stated in the module documentation. No downstream uses or upstream lemmas are recorded, and the result remains disconnected from the forcing chain or phi-ladder constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.