IndisputableMonolith.Complexity.RSVC

   1import Mathlib
   2import IndisputableMonolith.Complexity.VertexCover
   3
   4namespace IndisputableMonolith
   5namespace Complexity
   6
   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 -/
  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
  65
  66end IndisputableMonolith
  67