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 neighbours of each gadget vertex (DescriptiveComplexity.dgEdge_iff / DescriptiveComplexity.IAdjRaw).

Structure

1. Neighbour sets. For each gadget vertex, the exact set of its DescriptiveComplexity.DGEdge-neighbours (by cases on the other vertex's tag, via dgEdge_iff). The internal vertices ⟨g1,(a,b)⟩ and ⟨g4,(a,b)⟩ have exactly two neighbours, ⟨g0/g2⟩ and ⟨g3/g5⟩ respectively.
2. Forced edges. In a Hamilton circuit each vertex has exactly two tour-neighbours, 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 neighbour 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.gPt_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) : ↑(gPt t ht h) = (t, ![a, b])

A gadget vertex ⟨t,(a,b)⟩ (raw form). Reconstructing a neighbour from its tag and coordinates uses this together with Subtype.ext.

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 neighbour characterizations of step 1 (it sidesteps the subtype/MapRel definitional mismatch that blocks simp on raw destructured vertices).

theorem DescriptiveComplexity.nextIdx_eq_finRotate {N : ℕ} (i : Fin N) : nextIdx i = (finRotate N) i

nextIdx on Fin N is Mathlib's cyclic rotation finRotate N (so it is a bijection).

theorem DescriptiveComplexity.nextIdx_nextIdx_ne {N : ℕ} (hN : 3 ≤ N) (i : Fin N) : nextIdx (nextIdx i) ≠ i

In a cyclic enumeration nextIdx applied twice returns a different index, as soon as the cycle has length at least three.

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-neighbours.

Equations

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

theorem DescriptiveComplexity.tourSucc_ne_symm {H : Type} {N : ℕ} (f : Fin N ≃ H) (hN : 3 ≤ N) (x : H) : (tourSucc f) x ≠ (Equiv.symm (tourSucc f)) x

The two tour-neighbours of x are distinct once the cycle has length ≥ 3: the successor is not the predecessor.

theorem DescriptiveComplexity.TAdj_symm {H : Type} {N : ℕ} {f : Fin N ≃ H} {x y : H} (h : TAdj f x y) : TAdj f y x

Tour-adjacency is symmetric.

theorem DescriptiveComplexity.tadj_succ {H : Type} {N : ℕ} (f : Fin N ≃ H) (x : H) : TAdj f x ((tourSucc f) x)

x is tour-adjacent to its successor and to its predecessor.

theorem DescriptiveComplexity.tadj_pred {H : Type} {N : ℕ} (f : Fin N ≃ H) (x : H) : TAdj f x ((Equiv.symm (tourSucc f)) x)

theorem DescriptiveComplexity.tadj_eq {H : Type} {N : ℕ} {f : Fin N ≃ H} {x y : H} (h : TAdj f x y) : y = (tourSucc f) x ∨ y = (Equiv.symm (tourSucc f)) x

Every tour-neighbour of x is its successor or its predecessor.

theorem DescriptiveComplexity.tadj_dgEdge {H : Type} {N : ℕ} {f : Fin N ≃ H} {R : H → H → Prop} (hf : ∀ (i : Fin N), R (f i) (f (nextIdx i))) (hsymm : ∀ (a b : H), R a b → R b a) {x y : H} (h : TAdj f x y) : R x y

A tour edge is a graph edge.

theorem DescriptiveComplexity.tourSucc_mem_of_tadj {H : Type} {N : ℕ} {f : Fin N ≃ H} {x p q : H} (hp : TAdj f x p) (hq : TAdj f x q) (hpq : p ≠ q) : (tourSucc f) x = p ∨ (tourSucc f) x = q

The tour successor of x is one of its two known tour-neighbours.

theorem DescriptiveComplexity.tadj_two {H : Type} {N : ℕ} {f : Fin N ≃ H} {x p q y : H} (hp : TAdj f x p) (hq : TAdj f x q) (hpq : p ≠ q) (hy : TAdj f x y) : y = p ∨ y = q

A vertex has only two tour-neighbours: once two distinct ones are known, every tour-neighbour is one of them.

theorem DescriptiveComplexity.all_of_succ_closed {N : ℕ} [NeZero N] (P : Fin N → Prop) (i₀ : Fin N) (h₀ : P i₀) (hs : ∀ (i : Fin N), P i → P (i + 1)) (j : Fin N) : P j

A successor-closed subset of Fin N is everything. Starting from any element, repeatedly adding one cycles through all of Fin N.

theorem DescriptiveComplexity.tourSucc_closed_univ {H : Type} {N : ℕ} (f : Fin N ≃ H) {P : H → Prop} {x : H} (hx : P x) (hclosed : ∀ (y : H), P y → P ((tourSucc f) y)) (z : H) : P z

The tour is a single cycle. Any nonempty subset of the universe closed under the tour successor is the whole universe. (tourSucc is conjugate to the N-cycle finRotate N, so it has no proper invariant subset.)

theorem DescriptiveComplexity.tour_forced {H : Type} {N : ℕ} (f : Fin N ≃ H) {R : H → H → Prop} (hf : ∀ (i : Fin N), R (f i) (f (nextIdx i))) (hsymm : ∀ (a b : H), R a b → R b a) (hN : 3 ≤ N) {x p q : H} (hnb : ∀ (y : H), R x y → y = p ∨ y = q) : TAdj f x p ∧ TAdj f x q

Forced edges. If a vertex x in a tour has at most two graph-neighbours (every neighbour is p or q), then p and q are exactly its two tour-neighbours: every one of x's edges is used by the tour. (Distinctness of the two tour-neighbours, from 3 ≤ N, forces p ≠ q and that both occur.)

theorem DescriptiveComplexity.nbrs_gPt_g1 {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {a b : A} (h : HEdge a b) (q : hamInterp.MapRel A) : DGEdge (gPt HTag.g1 ⋯ h) q ↔ q = gPt HTag.g0 ⋯ h ∨ q = gPt HTag.g2 ⋯ h

The neighbours of the internal vertex ⟨g1,(a,b)⟩ are exactly ⟨g0,(a,b)⟩ and ⟨g2,(a,b)⟩. So in a Hamilton circuit both its edges are forced.

theorem DescriptiveComplexity.nbrs_gPt_g4 {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {a b : A} (h : HEdge a b) (q : hamInterp.MapRel A) : DGEdge (gPt HTag.g4 ⋯ h) q ↔ q = gPt HTag.g3 ⋯ h ∨ q = gPt HTag.g5 ⋯ h

The neighbours of the internal vertex ⟨g4,(a,b)⟩ are exactly ⟨g3,(a,b)⟩ and ⟨g5,(a,b)⟩.

theorem DescriptiveComplexity.nbrs_gPt_g2 {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {a b : A} (h : HEdge a b) (q : hamInterp.MapRel A) : DGEdge (gPt HTag.g2 ⋯ h) q ↔ q = gPt HTag.g1 ⋯ h ∨ q = gPt HTag.g3 ⋯ h ∨ q = gPt HTag.g0 ⋯ ⋯

The neighbours of ⟨g2,(a,b)⟩ are ⟨g1,(a,b)⟩, ⟨g3,(a,b)⟩ and the cross neighbour ⟨g0,(b,a)⟩.

theorem DescriptiveComplexity.nbrs_gPt_g3 {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {a b : A} (h : HEdge a b) (q : hamInterp.MapRel A) : DGEdge (gPt HTag.g3 ⋯ h) q ↔ q = gPt HTag.g2 ⋯ h ∨ q = gPt HTag.g4 ⋯ h ∨ q = gPt HTag.g5 ⋯ ⋯

The neighbours of ⟨g3,(a,b)⟩ are ⟨g2,(a,b)⟩, ⟨g4,(a,b)⟩ and the cross neighbour ⟨g5,(b,a)⟩.

From the tour to the forced gadget paths

theorem DescriptiveComplexity.dgEdge_symm {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {x y : hamInterp.MapRel A} (h : DGEdge x y) : DGEdge y x

The gadget edge relation is symmetric (it is the undirected edge).

theorem DescriptiveComplexity.gPt_ne_tag {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {i j : HTag} (hij : i ≠ j) {hi : i ≠ HTag.sel ∧ i ≠ HTag.hub} {hj : j ≠ HTag.sel ∧ j ≠ HTag.hub} {a b a' b' : A} (h : HEdge a b) (h' : HEdge a' b') : gPt i hi h ≠ gPt j hj h'

Gadget vertices with distinct tags are distinct (local copy, so Reverse stays independent of Forward).

theorem DescriptiveComplexity.gPt_edge_irrel {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {t : HTag} {ht : t ≠ HTag.sel ∧ t ≠ HTag.hub} {a b : A} (h₁ h₂ : HEdge a b) : gPt t ht h₁ = gPt t ht h₂

A gadget vertex depends on the edge only through its endpoints, not the proof (handy to normalize a doubly-symmetrized edge back to the original).

theorem DescriptiveComplexity.eq_selPt_of_tag {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {q : hamInterp.MapRel A} (hqt : (↑q).1 = HTag.sel) : ∃ (m : A) (hm : MGMarked m), q = selPt hm

A vertex tagged sel is a selector selPt hm for a marked vertex.

theorem DescriptiveComplexity.three_le_of_edge {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {N : ℕ} (f : Fin N ≃ hamInterp.MapRel A) {a b : A} (h : HEdge a b) : 3 ≤ N

At least three vertices. If the target universe carries an edge, its gadget contributes twelve distinct vertices, so any cyclic enumeration has length ≥ 3 – enough to run tour_forced.

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-neighbours.

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.prop_g2 {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 ⋯ h) (gPt HTag.g0 ⋯ ⋯)

Propagation at g2. With the forced u-path, ⟨g1⟩ is one of ⟨g2⟩'s two tour-neighbours; the other, being a graph-neighbour distinct from ⟨g1⟩, is either ⟨g3⟩ (traverse this side straight through) or the cross vertex ⟨g0,(b,a)⟩ (hand the tour over to the other side).

theorem DescriptiveComplexity.prop_g3 {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.g3 ⋯ h) (gPt HTag.g2 ⋯ h) ∨ TAdj f (gPt HTag.g3 ⋯ h) (gPt HTag.g5 ⋯ ⋯)

Propagation at g3. Symmetrically, the tour leaves ⟨g3⟩ either straight to ⟨g2⟩ or across to the cross vertex ⟨g5,(b,a)⟩.

theorem DescriptiveComplexity.not_both_crossed {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) (hAcross : TAdj f (gPt HTag.g2 ⋯ h) (gPt HTag.g0 ⋯ ⋯)) (hBcross : TAdj f (gPt HTag.g2 ⋯ ⋯) (gPt HTag.g0 ⋯ h)) : False

Never neither. A gadget cannot be traversed with both sides crossed: that would close the six vertices g0 g1 g2 of each side into a single tour-invariant 6-cycle, which (the tour being one cycle over ≥ 12 vertices) must be the whole universe – impossible, as ⟨g3,(a,b)⟩ lies outside it.

theorem DescriptiveComplexity.nbrs_gPt_g0 {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {a b : A} (h : HEdge a b) (q : hamInterp.MapRel A) : DGEdge (gPt HTag.g0 ⋯ h) q ↔ q = gPt HTag.g1 ⋯ h ∨ q = gPt HTag.g2 ⋯ ⋯ ∨ (∃ (c : A) (hc : HEdge a c), c < b ∧ (∀ (d : A), HEdge a d → d ≤ c ∨ b ≤ d) ∧ q = gPt HTag.g5 ⋯ hc) ∨ (∀ (d : A), HEdge a d → b ≤ d) ∧ ∃ (m : A) (hm : MGMarked m), q = selPt hm

The neighbours of a general ⟨g0,(a,b)⟩: ⟨g1,(a,b)⟩, the cross vertex ⟨g2,(b,a)⟩, the chain link ⟨g5,(a,c)⟩ back to the predecessor neighbour c < b of b, and — when b is the least neighbour — every selector.

theorem DescriptiveComplexity.nbrs_gPt_g5 {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {a b : A} (h : HEdge a b) (q : hamInterp.MapRel A) : DGEdge (gPt HTag.g5 ⋯ h) q ↔ q = gPt HTag.g4 ⋯ h ∨ q = gPt HTag.g3 ⋯ ⋯ ∨ (∃ (c : A) (hc : HEdge a c), b < c ∧ (∀ (d : A), HEdge a d → d ≤ b ∨ c ≤ d) ∧ q = gPt HTag.g0 ⋯ hc) ∨ (∀ (d : A), HEdge a d → d ≤ b) ∧ ∃ (m : A) (hm : MGMarked m), q = selPt hm

The neighbours of a general ⟨g5,(a,b)⟩: ⟨g4,(a,b)⟩, the cross vertex ⟨g3,(b,a)⟩, the chain link ⟨g0,(a,c)⟩ on to the successor neighbour b < c, and — when b is the greatest neighbour — every selector.

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-neighbour of ⟨g0,(a,b)⟩ other than the forced ⟨g1,(a,b)⟩ is a selector (and b is a's least neighbour) 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-neighbour of ⟨g5,(a,b)⟩ other than the forced ⟨g4,(a,b)⟩ is a selector (and b is a's greatest neighbour) 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.

theorem DescriptiveComplexity.straight_of_chain_up {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.g5 ⋯ h) (gPt HTag.g0 ⋯ hc)) : TAdj f (gPt HTag.g2 ⋯ ⋯) (gPt HTag.g3 ⋯ ⋯)

A used chain-link straightens the later side, symmetrically: a tour edge ⟨g5,(a,b)⟩–⟨g0,(a,c)⟩ fills both slots of ⟨g0,(a,c)⟩, so its cross edge is unused and (by prop_g2) 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 neighbours 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 neighbour 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 neighbour 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)

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

theorem DescriptiveComplexity.le_maxNbr {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] [Fintype A] {a : A} (h : ∃ (b : A), HEdge a b) {d : A} (hd : HEdge a d) : d ≤ 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 ⋯

theorem DescriptiveComplexity.entrancePt_inj {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] [Fintype A] {a a' : A} (h : ∃ (b : A), HEdge a b) (h' : ∃ (b : A), HEdge a' b) (he : entrancePt h = entrancePt h') : a = a'

Distinct owners give distinct entrances (so a ↦ entrancePt a is injective).

theorem DescriptiveComplexity.exitPt_inj {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] [Fintype A] {a a' : A} (h : ∃ (b : A), HEdge a b) (h' : ∃ (b : A), HEdge a' b) (he : exitPt h = exitPt h') : a = a'

theorem DescriptiveComplexity.entrancePt_ne_exitPt {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] [Fintype A] {a a' : A} (h : ∃ (b : A), HEdge a b) (h' : ∃ (b : A), HEdge a' b) : entrancePt h ≠ exitPt h'

Entrance and exit never coincide (different tags), even across owners.

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

The selector tour-neighbour of v (well-defined when v has one): the tour successor if that is the selector, else the predecessor.

Equations

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

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))

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

Recover a vertex from its selector-neighbour and the slot direction.

Equations

• DescriptiveComplexity.recover f s β = if β = true then (Equiv.symm (DescriptiveComplexity.tourSucc f)) s else (DescriptiveComplexity.tourSucc f) s

theorem DescriptiveComplexity.recover_selOf {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {N : ℕ} (f : Fin N ≃ hamInterp.MapRel A) (v : hamInterp.MapRel A) : recover f (selOf f v) (bit f v) = v

The recovery is exact: v is read back from selOf v and bit v.

theorem DescriptiveComplexity.isSel_selOf {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {N : ℕ} (f : Fin N ≃ hamInterp.MapRel A) {v : hamInterp.MapRel A} (h : isSel ((tourSucc f) v) ∨ isSel ((Equiv.symm (tourSucc f)) v)) : isSel (selOf f v)

When v has a selector tour-neighbour, selOf v is that selector.

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.

noncomputable def DescriptiveComplexity.ptOf {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] [Fintype A] [Nonempty (hamInterp.MapRel A)] (a : A) (d : Bool) : hamInterp.MapRel A

The entrance (d = false) or exit (d = true) of a; junk if a is isolated.

Equations

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

theorem DescriptiveComplexity.isSel_selOf_ptOf {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] [Fintype A] {N : ℕ} (f : Fin N ≃ hamInterp.MapRel A) [Nonempty (hamInterp.MapRel A)] {a : A} (ha : Active f a) (d : Bool) : isSel (selOf f (ptOf a d))

For an active vertex, ptOf really is the entrance/exit, which has a selector tour-neighbour; hence selOf (ptOf …) is a selector.

theorem DescriptiveComplexity.marked_of_active {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] [Fintype A] {N : ℕ} (f : Fin N ≃ hamInterp.MapRel A) [Nonempty (hamInterp.MapRel A)] {a : A} (ha : Active f a) (d : Bool) : MGMarked ((↑(selOf f (ptOf a d))).2 0)

The mark carried by selOf (ptOf …) of an active vertex is marked.

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.entrance_sel_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))) {a : A} (b : A) (h : HEdge a b) : TAdj f (gPt HTag.g2 ⋯ ⋯) (gPt HTag.g3 ⋯ ⋯) → isSel ((tourSucc f) (entrancePt ⋯)) ∨ isSel ((Equiv.symm (tourSucc f)) (entrancePt ⋯))

Straightness reaches the entrance. If some side (b,a) of a's chain is straight, the entrance slot of ⟨g0,(a,b)⟩ is a selector or a chain-link (g0_other); a chain-link keeps the walked side straight (straight_of_chain_down), so by well-founded descent along a's neighbour list the chain entrance has a selector tour-neighbour.

theorem DescriptiveComplexity.exit_sel_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))) {a : A} (b : A) (h : HEdge a b) : TAdj f (gPt HTag.g2 ⋯ ⋯) (gPt HTag.g3 ⋯ ⋯) → isSel ((tourSucc f) (exitPt ⋯)) ∨ isSel ((Equiv.symm (tourSucc f)) (exitPt ⋯))

Straightness reaches the exit, symmetrically: well-founded ascent along a's neighbour list through g5_other and straight_of_chain_up.

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).