three_sat_runtime_prop
plain-language theorem explainer
three_sat_runtime_prop encodes the target runtime bound for 3-SAT of size n as O(n^{11/3} log n), absorbed into O(n^4). Researchers analyzing CA-to-TM simulations in complexity would cite it when closing polynomial-time claims. The declaration is a direct existential definition over the reals with no lemmas or tactics.
Claim. For every natural number $n$, there exists a positive real $c$ such that $n^{11/3} log(n+2) ≤ c n^4$.
background
The module supplies abstract runtime parameters for cellular automaton embeddings. This definition records the concrete target bound for the full 3-SAT algorithm expressed as a Turing-machine time cost. No upstream lemmas appear in the declaration or its immediate context.
proof idea
The definition is a direct existential statement over positive reals; no lemmas are applied and the body contains no tactics.
why it matters
The definition supplies the target bound referenced by the 3-SAT algorithm in the Complexity domain. It supports downstream claims that CA embeddings yield polynomial runtime. It sits inside the abstract runtime parameter layer without reference to Recognition Science landmarks such as the forcing chain or phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.