toVC

formal source

  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 -/
  41  TrBound : (ℕ → ℕ) → Prop := IsPolynomial
  42
  43/-- RS‑preserving wrapper bundling sizes and the reduction map. -/
  44def rs_preserving_RS2VC : RSPreserving ConstraintInstance VertexCover.Instance :=
  45{ sizeA := fun a => a.vertices.length + a.constraints.length
  46, sizeB := fun b => b.vertices.length + b.edges.length