IsPolynomial
plain-language theorem explainer
Definition IsPolynomial declares a function f from naturals to naturals to be polynomial when constants c and k exist making f(n) at most c n to the power k plus c for all n. Analysts of RS to vertex cover reductions in the Recognition Science framework cite this to certify polynomial time bounds on reductions. The definition is introduced directly as an existential statement over c and k.
Claim. A function $f : ℕ → ℕ$ satisfies the polynomial bound if there exist natural numbers $c$ and $k$ such that $f(n) ≤ c · n^k + c$ for every natural number $n$.
background
The RSVC module maps RS constraint instances to vertex cover instances by associating them with edges that require covering. This setting supports reductions that preserve certain properties between the original RS problem and the graph problem. IsPolynomial encodes the standard polynomial growth condition used to bound the running time of such reductions. It appears as the default for the time complexity bound in the RSPreserving structure.
proof idea
The definition is given directly by existential quantification: there exist c and k in naturals such that the inequality holds for all n. No external lemmas or tactics are invoked; it serves as the foundational predicate for polynomial complexity in this module.
why it matters
RSPreserving references IsPolynomial to set its TcBound field, enabling the definition of reductions whose time complexity is polynomial. This fits into the broader Recognition Science effort to derive physical laws from functional equations by ensuring computational reductions remain efficient. It addresses the complexity aspect of mapping RS instances without introducing superpolynomial overhead.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.