import HardnessReductions.Graph.VertexCover

/-!
# VERTEX COVER on graphs of maximum degree at most three

A *structural* "hard even if": the restriction constrains the shape of the
graph, where 3SAT's constrains the shape of a formula. Garey,
Johnson and Stockmeyer's Theorem 2.6 — the paper whose title, "Some simplified
NP-complete graph problems", is exactly this genre.

## Why `≤ 3` and not `= 3`

Both statements circulate. The construction proves the bound, not the
regularity: its variable circuits carry a connection edge on one side of each
slot pair only, so half the circuit vertices have degree two, and the graph is
not cubic. Stating `≤ 3` is also the sharpest of the `≤`-bounds — degree `≤ 2`
graphs are disjoint paths and cycles, whose minimum vertex cover is computable
directly — so nothing is lost by not asking for equality. Regularity is a
genuinely different statement, reached by padding the construction, and belongs
to whichever descendant first needs it.

Hardness proof (in `BoundedDegree/`): from 3SAT (`FromSat3.lean`, one circuit
per variable and one triangle per clause; certified in `FromSat3/Code.lean` and
`FromSat3/Adequacy.lean`).
-/

namespace Hardness

/-- VERTEX COVER, restricted to graphs in which no vertex has more than three
neighbours, in the promise-free formulation of `Problem.restrict`: a graph with
a vertex of degree four is simply a no-instance. -/
def VERTEX_COVER_DEG3 : Problem GraphThresholdInstance :=
  VERTEX_COVER.restrict fun x ↦ ∀ v : x.V, x.G.degree v ≤ 3

/-- **Renaming invariance of a degree bound**: it transfers across a bijection
matching the two adjacency relations. The companion of
`exists_vertexCover_iff_of_equiv`, and what the entry's representation pair
consumes — the bijection is an isomorphism of graphs, and mathlib's
`SimpleGraph.Iso.degree_eq` says isomorphisms preserve degrees. -/
theorem forall_degree_le_iff_of_equiv {V W : Type*} [Fintype V] [Fintype W]
    {G : SimpleGraph V} {H : SimpleGraph W} [DecidableRel G.Adj] [DecidableRel H.Adj]
    (e : V ≃ W) (hadj : ∀ a b : V, G.Adj a b ↔ H.Adj (e a) (e b)) (d : ℕ) :
    (∀ v : V, G.degree v ≤ d) ↔ ∀ w : W, H.degree w ≤ d := by
  have f : G ≃g H := ⟨e, fun {a b} ↦ (hadj a b).symm⟩
  constructor
  · intro h w
    have hw : G.degree (f.symm w) = H.degree w := f.symm.degree_eq w
    rw [← hw]
    exact h _
  · intro h v
    have hv : H.degree (f v) = G.degree v := f.degree_eq _
    rw [← hv]
    exact h _

end Hardness