RSPreserving
plain-language theorem explainer
RSPreserving supplies a structure that bundles size maps for two types, a reduction function between them, and polynomial complexity predicates on those sizes. Researchers constructing explicit reductions between constraint satisfaction and vertex cover instances in the Recognition Science setting would cite this scaffold when establishing polynomial-time mappings. The declaration is a direct structure definition that assigns the time and space bounds to the IsPolynomial predicate.
Claim. A structure on types $A$ and $B$ consisting of size functions $size_A : A → ℕ$ and $size_B : B → ℕ$, a reduction map $reduce : A → B$, and predicates $TcBound, TrBound : (ℕ → ℕ) → Prop$ each set to the predicate $IsPolynomial$, where $IsPolynomial(f)$ asserts that $f(n) ≤ c · n^k + c$ for some constants $c, k ∈ ℕ$.
background
The RSVC module treats RS constraint instances as graphs whose edges must be covered. The sibling definition IsPolynomial states that a function $f : ℕ → ℕ$ is polynomial when there exist $c, k ∈ ℕ$ such that $f(n) ≤ c · n^k + c$ for every $n$. Upstream imports supply the Time abbreviation from RSNativeUnits, the constant $A = 1$ for active edges per tick from both IntegrationGap and Masses.Anchor, and the Actualization operator $A$ that selects the minimal-J configuration. The module context is the mapping of RS constraint instances onto vertex-cover edge sets.
proof idea
This is a structure definition. The four fields are declared directly, with TcBound and TrBound defaulting to the IsPolynomial predicate supplied by the sibling definition at line 31.
why it matters
The structure is instantiated by rs_preserving_RS2VC to produce a concrete reduction from ConstraintInstance to VertexCover.Instance and is asserted nonempty by rs_pres_prop. It supplies the scaffold for RS-preserving reductions in the complexity domain, supporting polynomial bounds on the size functions that appear in the Recognition Science forcing chain. No open questions are closed by this definition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.