   7namespace RSVC
   8
   9/-- RS constraint instance mapped to edges to be covered. -/
  10structure ConstraintInstance where
  11  vertices    : List Nat
  12  constraints : List (Nat × Nat)
  13  k           : Nat
  14
  15/-- Forgetful map to a Vertex Cover instance. -/
  16@[simp] def toVC (A : ConstraintInstance) : VertexCover.Instance :=
  17{ vertices := A.vertices, edges := A.constraints, k := A.k }
  18
  19/-- RS recognizer: instance is accepted iff its Vertex Cover image has a cover. -/
  20def Recognizes (A : ConstraintInstance) : Prop :=
  21  VertexCover.HasCover (toVC A)
  22
  23/-- The reduction from RS constraints to Vertex Cover (identity on fields). -/
  24@[simp] def reduceRS2VC : ConstraintInstance → VertexCover.Instance := toVC
  25
  26/-- Correctness is immediate from the definition. -/
  27@[simp] theorem reduce_correct (A : ConstraintInstance) :
  28  Recognizes A ↔ VertexCover.HasCover (reduceRS2VC A) := Iff.rfl
  29
  30/-- Polynomial bound predicate: f(n) ≤ c·n^k for some c,k -/
  31def IsPolynomial (f : ℕ → ℕ) : Prop := ∃ c k : ℕ, ∀ n, f n ≤ c * n ^ k + c
  32
  33/-- RS‑preserving reduction scaffold: relates complexities up to monotone envelopes. -/
  34structure RSPreserving (A B : Type) where
  35  sizeA : A → ℕ
  36  sizeB : B → ℕ
  37  reduce : A → B
  38  /-- Time complexity bound - polynomial -/
  39  TcBound : (ℕ → ℕ) → Prop := IsPolynomial
  40  /-- Space complexity bound - polynomial -/

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.