IsPolynomial
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not specify particular values for the degree k or constant c.
- Does not guarantee minimality of the bound.
- Does not connect directly to RS-specific constants such as phi or the J-function.
formal statement (Lean)
31def IsPolynomial (f : ℕ → ℕ) : Prop := ∃ c k : ℕ, ∀ n, f n ≤ c * n ^ k + c
proof body
Definition body.
32
33/-- RS‑preserving reduction scaffold: relates complexities up to monotone envelopes. -/