three_sat_runtime_prop
plain-language theorem explainer
The definition asserts that for any natural number n the Turing machine runtime solving 3-SAT instances satisfies an O(n^{11/3} log n) upper bound. Researchers analyzing complexity in the Recognition Science CA-embedding setting would cite it as the concrete target for the full algorithm. The statement is realized directly as an existential claim over a positive real constant c that dominates the given monomial and logarithmic term.
Claim. For every natural number $n$ there exists a positive real $c$ such that $n^{11/3} (n+2)^{(1/2)} wait no, log(n+2) ≤ c n^4$.
background
The module supplies abstract runtime parameters for the cellular automaton embedding of decision problems. The definition records the target Turing-machine time bound for the complete 3-SAT algorithm as O(n^{11/3} log n). No upstream lemmas are referenced; the surrounding siblings supply the CA model and simulation map that this bound is intended to close.
proof idea
Direct definition of the proposition via existential quantification over a positive real constant c satisfying the stated polynomial-logarithmic inequality.
why it matters
The definition supplies the explicit complexity target that the CA-to-TM simulation must respect inside the Recognition Science framework. It closes the runtime accounting for the 3-SAT instance in the complexity module and aligns with the broader program of embedding computational problems into the phi-ladder and eight-tick structures. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.