rs_pres_prop
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.