Vertex Cover from a Hamilton circuit

The reverse direction of the reduction reads a vertex cover off a Hamilton circuit of the gadget graph. Its foundation is a precise characterization of the neighbors of each gadget vertex (DescriptiveComplexity.dgEdge_iff / DescriptiveComplexity.IAdjRaw).

Structure

1. Neighbor sets. For each gadget vertex, the exact set of its DescriptiveComplexity.DGEdge-neighbors (by cases on the other vertex's tag, via dgEdge_iff). The internal vertices ⟨g1,(a,b)⟩ and ⟨g4,(a,b)⟩ have exactly two neighbors, ⟨g0/g2⟩ and ⟨g3/g5⟩ respectively.
2. Forced edges. In a Hamilton circuit each vertex has exactly two tour-neighbors, both adjacent to it. So a degree-two vertex uses both its edges, forcing the paths g0-g1-g2 and g3-g4-g5 in every gadget (DescriptiveComplexity.forced_g1, DescriptiveComplexity.forced_g4).
3. The three traversals. Propagating through g2, g3 (degree three) shows each gadget is traversed through the u-side, the v-side, or both – never neither (which would isolate it as two 6-cycles): every edge has a straight side (DescriptiveComplexity.side_straight).
4. Chain propagation. A straight side (b,a) frees the entrance and exit slots of the opposite side (a,b) from the cross edges (DescriptiveComplexity.g0_other/g5_other); the freed slot is a selector at the ends of a's chain, or a chain-link that straightens the walked side in turn (DescriptiveComplexity.straight_of_chain_down/up). Well-founded induction along a's neighbor list puts a selector at both chain ends: a is active (DescriptiveComplexity.active_of_straight).
5. The cover. C := {a | Active f a} covers every edge (DescriptiveComplexity.cover_property), and |C| ≤ |marked| by the selector-slot injection (DescriptiveComplexity.active_ncard_le).

DescriptiveComplexity.eq_gPt_of_val below reconstructs a vertex from its tag and coordinates (sidestepping a simp/subtype mismatch), the workhorse of step 1.

theorem DescriptiveComplexity.eq_gPt_of_val {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {t : HTag} {ht : t ≠ HTag.sel ∧ t ≠ HTag.hub} {a b : A} (h : HEdge a b) {q : hamInterp.MapRel A} (hqt : (↑q).1 = t) (h0 : (↑q).2 0 = a) (h1 : (↑q).2 1 = b) : q = gPt t ht h

Reconstruction: an interpreted vertex with a gadget tag t and coordinates (a, b) is the gadget vertex gPt t _ h. This is the workhorse of the neighbor characterizations of step 1 (it sidesteps the subtype/MapRel definitional mismatch that blocks simp on raw destructured vertices).

noncomputable def DescriptiveComplexity.tourSucc {H : Type} {N : ℕ} (f : Fin N ≃ H) : Equiv.Perm H

The tour successor of a cyclic enumeration f, as a permutation of the universe: the vertex one step further along the tour.

Equations

• DescriptiveComplexity.tourSucc f = f.symm.trans (Equiv.trans (finRotate N) f)

@[simp]

theorem DescriptiveComplexity.tourSucc_apply {H : Type} {N : ℕ} (f : Fin N ≃ H) (x : H) : (tourSucc f) x = f (nextIdx (f.symm x))

def DescriptiveComplexity.TAdj {H : Type} {N : ℕ} (f : Fin N ≃ H) (x y : H) : Prop

Two vertices are tour-adjacent when one is the tour successor of the other. This is symmetric, and every vertex has exactly two tour-neighbors.

Equations

• DescriptiveComplexity.TAdj f x y = ((DescriptiveComplexity.tourSucc f) x = y ∨ (DescriptiveComplexity.tourSucc f) y = x)

From the tour to the forced gadget paths

theorem DescriptiveComplexity.forced_g1 {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {N : ℕ} (f : Fin N ≃ hamInterp.MapRel A) (hf : ∀ (i : Fin N), DGEdge (f i) (f (nextIdx i))) {a b : A} (h : HEdge a b) : TAdj f (gPt HTag.g1 ⋯ h) (gPt HTag.g0 ⋯ h) ∧ TAdj f (gPt HTag.g1 ⋯ h) (gPt HTag.g2 ⋯ h)

Forced u-path. The degree-two internal vertex ⟨g1,(a,b)⟩ uses both of its edges: ⟨g0⟩ and ⟨g2⟩ are its two tour-neighbors.

theorem DescriptiveComplexity.forced_g4 {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {N : ℕ} (f : Fin N ≃ hamInterp.MapRel A) (hf : ∀ (i : Fin N), DGEdge (f i) (f (nextIdx i))) {a b : A} (h : HEdge a b) : TAdj f (gPt HTag.g4 ⋯ h) (gPt HTag.g3 ⋯ h) ∧ TAdj f (gPt HTag.g4 ⋯ h) (gPt HTag.g5 ⋯ h)

Forced v-path. Symmetrically, ⟨g4,(a,b)⟩ uses both ⟨g3⟩ and ⟨g5⟩.

theorem DescriptiveComplexity.side_straight {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {N : ℕ} (f : Fin N ≃ hamInterp.MapRel A) (hf : ∀ (i : Fin N), DGEdge (f i) (f (nextIdx i))) {a b : A} (h : HEdge a b) : TAdj f (gPt HTag.g2 ⋯ h) (gPt HTag.g3 ⋯ h) ∨ TAdj f (gPt HTag.g2 ⋯ ⋯) (gPt HTag.g3 ⋯ ⋯)

At least one side is straight. Combining the g2 case split (prop_g2) on both sides with not_both_crossed: for every edge, the tour runs straight through the a-side gadget (g2-g3) or through the b-side gadget.

Straightness propagates along the owner's chain

def DescriptiveComplexity.isSel {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] (q : hamInterp.MapRel A) : Prop

Whether a vertex is a selector.

Equations

• DescriptiveComplexity.isSel q = ((↑q).1 = DescriptiveComplexity.HTag.sel)

@[instance_reducible]

instance DescriptiveComplexity.instDecidablePredMapRelHTagHamInterpIsSel {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] : DecidablePred isSel

Equations

• DescriptiveComplexity.instDecidablePredMapRelHTagHamInterpIsSel q = DescriptiveComplexity.instDecidablePredMapRelHTagHamInterpIsSel._aux_1 q

theorem DescriptiveComplexity.g0_other {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {N : ℕ} (f : Fin N ≃ hamInterp.MapRel A) (hf : ∀ (i : Fin N), DGEdge (f i) (f (nextIdx i))) {a b : A} (h : HEdge a b) (hS : TAdj f (gPt HTag.g2 ⋯ ⋯) (gPt HTag.g3 ⋯ ⋯)) : (∀ (d : A), HEdge a d → b ≤ d) ∧ (isSel ((tourSucc f) (gPt HTag.g0 ⋯ h)) ∨ isSel ((Equiv.symm (tourSucc f)) (gPt HTag.g0 ⋯ h))) ∨ ∃ (c : A) (hc : HEdge a c), c < b ∧ TAdj f (gPt HTag.g0 ⋯ h) (gPt HTag.g5 ⋯ hc)

The entrance slot of a straight-opposite side. When the b-side of the edge {a, b} is straight, both tour-slots of ⟨g2,(b,a)⟩ are known, so the cross edge into ⟨g0,(a,b)⟩ is unused: the tour-neighbor of ⟨g0,(a,b)⟩ other than the forced ⟨g1,(a,b)⟩ is a selector (and b is a's least neighbor) or the chain-link from the predecessor side.

theorem DescriptiveComplexity.g5_other {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {N : ℕ} (f : Fin N ≃ hamInterp.MapRel A) (hf : ∀ (i : Fin N), DGEdge (f i) (f (nextIdx i))) {a b : A} (h : HEdge a b) (hS : TAdj f (gPt HTag.g2 ⋯ ⋯) (gPt HTag.g3 ⋯ ⋯)) : (∀ (d : A), HEdge a d → d ≤ b) ∧ (isSel ((tourSucc f) (gPt HTag.g5 ⋯ h)) ∨ isSel ((Equiv.symm (tourSucc f)) (gPt HTag.g5 ⋯ h))) ∨ ∃ (c : A) (hc : HEdge a c), b < c ∧ TAdj f (gPt HTag.g5 ⋯ h) (gPt HTag.g0 ⋯ hc)

The exit slot of a straight-opposite side, symmetrically: the tour-neighbor of ⟨g5,(a,b)⟩ other than the forced ⟨g4,(a,b)⟩ is a selector (and b is a's greatest neighbor) or the chain-link to the successor side.

theorem DescriptiveComplexity.straight_of_chain_down {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {N : ℕ} (f : Fin N ≃ hamInterp.MapRel A) (hf : ∀ (i : Fin N), DGEdge (f i) (f (nextIdx i))) {a b c : A} (h : HEdge a b) (hc : HEdge a c) (hch : TAdj f (gPt HTag.g0 ⋯ h) (gPt HTag.g5 ⋯ hc)) : TAdj f (gPt HTag.g2 ⋯ ⋯) (gPt HTag.g3 ⋯ ⋯)

A used chain-link straightens the earlier side. If the tour uses the chain edge ⟨g0,(a,b)⟩–⟨g5,(a,c)⟩, both tour-slots of ⟨g5,(a,c)⟩ are known, so its cross edge is unused and (by prop_g3) the side (c,a) is straight.

Counting: the active chains inject into the selectors

noncomputable def DescriptiveComplexity.nbrFinset {A : Type} [FirstOrder.Language.markedGraph.Structure A] [Fintype A] (a : A) : Finset A

The neighbors of a as a finset.

Equations

• DescriptiveComplexity.nbrFinset a = Finset.filter (DescriptiveComplexity.HEdge a) Finset.univ

theorem DescriptiveComplexity.mem_nbrFinset {A : Type} [FirstOrder.Language.markedGraph.Structure A] [Fintype A] {a b : A} : b ∈ nbrFinset a ↔ HEdge a b

theorem DescriptiveComplexity.nbrFinset_nonempty {A : Type} [FirstOrder.Language.markedGraph.Structure A] [Fintype A] {a : A} (h : ∃ (b : A), HEdge a b) : (nbrFinset a).Nonempty

noncomputable def DescriptiveComplexity.minNbr {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] [Fintype A] {a : A} (h : ∃ (b : A), HEdge a b) : A

The least neighbor of a (the second coordinate of its chain entrance).

Equations

• DescriptiveComplexity.minNbr h = (DescriptiveComplexity.nbrFinset a).min' ⋯

noncomputable def DescriptiveComplexity.maxNbr {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] [Fintype A] {a : A} (h : ∃ (b : A), HEdge a b) : A

The greatest neighbor of a (the second coordinate of its chain exit).

Equations

• DescriptiveComplexity.maxNbr h = (DescriptiveComplexity.nbrFinset a).max' ⋯

theorem DescriptiveComplexity.hEdge_minNbr {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] [Fintype A] {a : A} (h : ∃ (b : A), HEdge a b) : HEdge a (minNbr h)

theorem DescriptiveComplexity.hEdge_maxNbr {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] [Fintype A] {a : A} (h : ∃ (b : A), HEdge a b) : HEdge a (maxNbr h)

noncomputable def DescriptiveComplexity.entrancePt {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] [Fintype A] {a : A} (h : ∃ (b : A), HEdge a b) : hamInterp.MapRel A

The chain entrance of a: ⟨g0,(a, minNbr a)⟩.

Equations

• DescriptiveComplexity.entrancePt h = DescriptiveComplexity.gPt DescriptiveComplexity.HTag.g0 DescriptiveComplexity.entrancePt._proof_1 ⋯

noncomputable def DescriptiveComplexity.exitPt {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] [Fintype A] {a : A} (h : ∃ (b : A), HEdge a b) : hamInterp.MapRel A

The chain exit of a: ⟨g5,(a, maxNbr a)⟩.

Equations

• DescriptiveComplexity.exitPt h = DescriptiveComplexity.gPt DescriptiveComplexity.HTag.g5 DescriptiveComplexity.exitPt._proof_1 ⋯

noncomputable def DescriptiveComplexity.bit {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {N : ℕ} (f : Fin N ≃ hamInterp.MapRel A) (v : hamInterp.MapRel A) : Bool

Which tour-slot direction of the selector s points back at the vertex.

Equations

• DescriptiveComplexity.bit f v = decide (DescriptiveComplexity.isSel ((DescriptiveComplexity.tourSucc f) v))

def DescriptiveComplexity.Active {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] [Fintype A] {N : ℕ} (f : Fin N ≃ hamInterp.MapRel A) (a : A) : Prop

a is active in tour f: both its chain entrance and its chain exit are tour-adjacent to a selector (so its whole chain is a selector-to-selector arc).

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.active_ncard_le {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] [Fintype A] {N : ℕ} (f : Fin N ≃ hamInterp.MapRel A) [Nonempty (hamInterp.MapRel A)] : {a : A | Active f a}.ncard ≤ {m : A | MGMarked m}.ncard

The active vertices inject into the marked ones: |C| ≤ |marked|. The map (a, entrance/exit) ↦ (selector, slot-direction) is injective – the selector and slot pin down the entrance/exit vertex (recover_selOf), whose owner and role (g0 vs g5) pin down a. Two chain-endpoints per active chain, two slots per selector, so 2|C| ≤ 2|marked|.

theorem DescriptiveComplexity.active_of_straight {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] [Fintype A] {N : ℕ} (f : Fin N ≃ hamInterp.MapRel A) (hf : ∀ (i : Fin N), DGEdge (f i) (f (nextIdx i))) {u v : A} (h : HEdge u v) (hS : TAdj f (gPt HTag.g2 ⋯ h) (gPt HTag.g3 ⋯ h)) : Active f v

A straight side makes the opposite owner active: if the side (u,v) of the edge {u,v} is traversed straight through g2–g3, then v's chain runs selector to selector, so v is active.

theorem DescriptiveComplexity.cover_property {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] [Fintype A] {N : ℕ} (f : Fin N ≃ hamInterp.MapRel A) (hf : ∀ (i : Fin N), DGEdge (f i) (f (nextIdx i))) {a b : A} (h : HEdge a b) : Active f a ∨ Active f b

Cover property: every edge has an active endpoint. The gadget of {a,b} is traversed straight on the a-side or the b-side (side_straight), and a straight side activates the opposite owner (active_of_straight).