H_SATTMRuntime
This definition asserts that for any SAT instance with n variables and m clauses there exists a Turing-machine runtime T at most n times the cellular-automaton evaluation time such that the machine returns the correct satisfiability answer. Researchers working on the P-versus-NP separation inside the Recognition Science framework would cite the predicate when bounding the serial readout cost of a parallel CA computation. The definition is assembled as a direct existential quantification over the product of n and sat_eval_time together with an尚未
claimFor natural numbers $n$ and $m$, the predicate $H(n,m)$ holds if and only if there exists a natural number $T$ satisfying $T ≤ n · t_{SAT eval}(n,m)$ and the Turing machine produces the correct satisfiability verdict for the instance.
background
The module builds one-dimensional cellular automata with local radius-r rules that evaluate Boolean circuits, relying on Rule 110 universality and reversible updates that preserve the ledger parity σ = 0. The supporting definition sat_eval_time returns the ceiling of $n^{1/3} log(n+m+2)$, obtained by laying variables on a three-dimensional-like grid so that clause propagation takes logarithmic depth while width grows as the cube root. Upstream results include the fundamental period T from Breath1024 and the structural conditions extracted from PrimitiveDistinction that guarantee the CA steps remain compatible with the simplicial ledger.
proof idea
The definition is a one-line wrapper that multiplies the already-computed sat_eval_time by n to encode the Turing-machine simulation overhead and conjoins the resulting bound with the placeholder predicate IsCorrectTMResult. No further lemmas or tactics are invoked; the body simply asserts existence of a T inside the envelope.
why it matters in Recognition Science
The predicate supplies the runtime hypothesis required by the P-versus-NP argument in the CellularAutomata module, converting the CA bound O(n^{1/3} log n) into a Turing-machine bound O(n^{4/3} log n). It occupies the chain step that links local CA gadgets to total serial time and therefore sits inside the Recognition Science forcing sequence from T5 uniqueness through the eight-tick octave. The open question it leaves is the formal definition and proof of IsCorrectTMResult together with the exact constant factor in the simulation overhead.
scope and limits
- Does not prove that IsCorrectTMResult holds for any concrete SAT instance.
- Does not derive the O(n^{4/3} log n) simulation bound; it only states an upper envelope.
- Does not establish that the cellular automaton itself solves SAT inside the stated time.
- Does not connect the runtime predicate to Recognition Science mass or fine-structure formulas.
formal statement (Lean)
218def H_SATTMRuntime (n m : ℕ) : Prop :=
proof body
Definition body.
219 ∃ (T : ℕ), T ≤ n * sat_eval_time n m ∧
220 -- This is the total Turing time for SAT evaluation via CA
221 IsCorrectTMResult n m T -- SCAFFOLD: IsCorrectTMResult is not yet defined.
222
223-- axiom h_sat_tm_runtime : ∀ n m, 0 < n → H_SATTMRuntime n m
224
225/-! ## The Key Separation -/
226
227/-- **Computation time** for SAT via CA (documentation / TODO): O(n^{1/3} log n)
228
229Intended claim: The CA evaluation time for a SAT instance with n variables and m clauses is
230O(n^{1/3} log(n+m)). This follows from arranging variables in a 3D-like grid on the 1D tape
231and using parallel propagation. -/
232/-!