`RSPreserving`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Complexity.RSVC on GitHub at line 34.

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

  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
  55/-- RS‑preserving reduction existence as a Prop. -/
  56def rs_pres_prop : Prop :=
  57  Nonempty (Complexity.RSVC.RSPreserving
  58              Complexity.RSVC.ConstraintInstance
  59              Complexity.VertexCover.Instance)
  60
  61lemma rs_pres_holds : rs_pres_prop :=
  62  ⟨Complexity.RSVC.rs_preserving_RS2VC⟩
  63
  64end IndisputableMonolith

papers checked against this theorem

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