`reduceRS2VC`

definition

show as: view math explainer →

module: IndisputableMonolith.Complexity.RSVC
domain: Complexity
line: 24 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Complexity.RSVC on GitHub at line 24.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  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
  47, reduce := reduceRS2VC }
  48
  49end RSVC
  50
  51end Complexity
  52
  53namespace IndisputableMonolith
  54

papers checked against this theorem

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