rs_pres_prop
Researchers in complexity reductions for Recognition Science cite this definition to assert existence of an RS-preserving reduction from constraint instances to vertex cover instances under polynomial size bounds. It packages the claim as a Prop for use in later lemmas. The definition applies the Nonempty constructor directly to the RSPreserving structure on the two concrete instance types.
claimThe proposition that the type of RS-preserving reductions from constraint instances (vertices, constraint pairs, and parameter $k$) to vertex cover instances (vertices, edges, and parameter $k$) is non-empty, where the reduction supplies size maps and a polynomial time bound.
background
ConstraintInstance is the structure with fields vertices : List Nat, constraints : List (Nat × Nat), and k : Nat, serving as the source type for RS problems. RSPreserving A B is the structure carrying sizeA : A → ℕ, sizeB : B → ℕ, reduce : A → B, and TcBound : (ℕ → ℕ) → Prop set to IsPolynomial. VertexCover.Instance is the target structure with vertices, edges, and k. The module sets the local context of mapping RS constraints onto graph edges for covering.
proof idea
This is a definition that directly sets the Prop to Nonempty (RSPreserving ConstraintInstance VertexCover.Instance). It functions as a one-line packaging of the existence claim with no further tactics or reductions applied.
why it matters in Recognition Science
The definition supplies the statement proved by the downstream lemma rs_pres_holds via the concrete reduction rs_preserving_RS2VC. It fills the slot asserting that RS constraint problems reduce to vertex cover while preserving size measures up to polynomial envelopes. This supports the broader Recognition Science program of embedding computational problems into known graph problems under the required complexity controls.
scope and limits
- Does not construct or exhibit any explicit reduce function.
- Does not verify that the time bound is polynomial.
- Does not reference Recognition Science constants such as phi or the forcing chain.
- Does not address decidability of the instances or the reduction.
formal statement (Lean)
56def rs_pres_prop : Prop :=
proof body
Definition body.
57 Nonempty (Complexity.RSVC.RSPreserving
58 Complexity.RSVC.ConstraintInstance
59 Complexity.VertexCover.Instance)
60