computation_recognition_separation
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not construct explicit Tc or Tr values.
- Does not derive the stated bounds from cellular-automaton rules.
- Does not address simulation to Turing machines.
- Does not connect to Recognition Science axioms or constants.
formal statement (Lean)
260theorem computation_recognition_separation (n : ℕ) (hn : 100 ≤ n) :
261 ∃ (Tc Tr : ℝ),
262 Tc ≤ n^(1/3 : ℝ) * Real.log n ∧
263 Tr ≥ n ∧
264 Tc < Tr
265-/
266
267end CellularAutomata
268end Complexity
269end IndisputableMonolith