Fixed-Host Colored Deletion Decks

This module starts the Lean infrastructure for the fixed-host singleton analysis in proof_sketch.tex.

The fixed-host problem keeps one graph K fixed and compares subsets U V : Set V by the colored vertex-deletion decks of (K, S, U) and (K, S, V), where S is a passive first color and U/V are the active second colors.

The definitions here are intentionally modest: colored card isomorphisms, deleted colors, fixed-host same-deck, and the one-hole/two-hole cards used in the low/complementary rectangular boundary.

structure SimpleGraph.TwoColorIso {V : Type u_1} {W : Type u_2} (G : SimpleGraph V) (H : SimpleGraph W) (S T : Set V) (S' T' : Set W) : Type (max u_1 u_2)

A graph isomorphism preserving two vertex colors.

• iso : G ≃g H
• map_first (v : V) : v ∈ S ↔ self.iso.toEquiv v ∈ S'
• map_second (v : V) : v ∈ T ↔ self.iso.toEquiv v ∈ T'

def SimpleGraph.TwoColorIso.refl {V : Type u_1} (G : SimpleGraph V) (S T : Set V) : G.TwoColorIso G S T S T

The identity two-colored isomorphism.

Equations

• SimpleGraph.TwoColorIso.refl G S T = { iso := SimpleGraph.Iso.refl, map_first := ⋯, map_second := ⋯ }

def SimpleGraph.TwoColorIso.symm {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} {S T : Set V} {S' T' : Set W} (e : G.TwoColorIso H S T S' T') : H.TwoColorIso G S' T' S T

Reverse a two-colored isomorphism.

Equations

• e.symm = { iso := e.iso.symm, map_first := ⋯, map_second := ⋯ }

def SimpleGraph.TwoColorIso.trans {V : Type u_1} {W : Type u_2} {X : Type u_3} {G : SimpleGraph V} {H : SimpleGraph W} {L : SimpleGraph X} {S T : Set V} {S' T' : Set W} {S'' T'' : Set X} (e₁ : G.TwoColorIso H S T S' T') (e₂ : H.TwoColorIso L S' T' S'' T'') : G.TwoColorIso L S T S'' T''

Compose two two-colored isomorphisms.

Equations

• e₁.trans e₂ = { iso := RelIso.trans e₁.iso e₂.iso, map_first := ⋯, map_second := ⋯ }

def SimpleGraph.deleteColor {V : Type u_1} (A : Set V) (z : V) : Set { w : V // w ≠ z }

Delete a vertex from a vertex color.

Equations

• SimpleGraph.deleteColor A z = {w : { w : V // w ≠ z } | ↑w ∈ A}

@[simp]

theorem SimpleGraph.mem_deleteColor {V : Type u_1} (A : Set V) (z : V) (w : { w : V // w ≠ z }) : w ∈ deleteColor A z ↔ ↑w ∈ A

@[reducible, inline]

abbrev SimpleGraph.fixedHostCardGraph {V : Type u_1} (K : SimpleGraph V) (z : V) : SimpleGraph { w : V // w ≠ z }

The fixed-host colored card obtained from (K, S, U) by deleting z.

Equations

• K.fixedHostCardGraph z = K.deleteVert z

def SimpleGraph.FixedHostCardIso {V : Type u_1} (K : SimpleGraph V) (S U V' : Set V) (z w : V) : Prop

Two fixed-host colored cards are isomorphic.

Equations

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

def SimpleGraph.FixedHostSameDeck {V : Type u_1} (K : SimpleGraph V) (S U V' : Set V) : Prop

Equality of fixed-host two-colored deletion decks, represented by a matching of deleted vertices.

Equations

• K.FixedHostSameDeck S U V' = ∃ (σ : V ≃ V), ∀ (z : V), K.FixedHostCardIso S U V' z (σ z)

theorem SimpleGraph.FixedHostSameDeck.refl {V : Type u_1} (K : SimpleGraph V) (S U : Set V) : K.FixedHostSameDeck S U U

Fixed-host same-deck is reflexive.

def SimpleGraph.singletonLeft {V : Type u_1} (T : Set V) (a : V) : Set V

The left singleton second color T ∪ {a}.

Equations

• SimpleGraph.singletonLeft T a = T ∪ {a}

def SimpleGraph.singletonRight {V : Type u_1} (T : Set V) (b : V) : Set V

The right singleton second color T ∪ {b}.

Equations

• SimpleGraph.singletonRight T b = T ∪ {b}

def SimpleGraph.singletonOutside {V : Type u_1} (T : Set V) (a b : V) : Set V

The outside set O = V(K) \ (T ∪ {a,b}) in the singleton switch.

Equations

• SimpleGraph.singletonOutside T a b = {x : V | x ∉ T ∧ x ≠ a ∧ x ≠ b}

@[simp]

theorem SimpleGraph.mem_singletonOutside {V : Type u_1} (T : Set V) (a b x : V) : x ∈ singletonOutside T a b ↔ x ∉ T ∧ x ≠ a ∧ x ≠ b

def SimpleGraph.FixedHostSingletonState {V : Type u_1} (K : SimpleGraph V) (S T : Set V) (a b : V) : Prop

The fixed-host singleton hypotheses: the active second color changes from T ∪ {a} to T ∪ {b} and the fixed-host colored decks agree.

Equations

• K.FixedHostSingletonState S T a b = (a ∉ T ∧ b ∉ T ∧ a ≠ b ∧ K.FixedHostSameDeck S (SimpleGraph.singletonLeft T a) (SimpleGraph.singletonRight T b))

def SimpleGraph.FixedHostSingletonSolved {V : Type u_1} (K : SimpleGraph V) (S T : Set V) (a b : V) : Prop

The desired singleton conclusion: a color-preserving automorphism of the fixed host carries T ∪ {a} to T ∪ {b}.

Equations

• K.FixedHostSingletonSolved S T a b = Nonempty (K.TwoColorIso K S (SimpleGraph.singletonLeft T a) S (SimpleGraph.singletonRight T b))

def SimpleGraph.FixedHostSingletonConjecture {V : Type u_1} (K : SimpleGraph V) (S T : Set V) (a b : V) : Prop

The fixed-host singleton conjecture as a Lean proposition.

Equations

• K.FixedHostSingletonConjecture S T a b = (K.FixedHostSingletonState S T a b → K.FixedHostSingletonSolved S T a b)

def SimpleGraph.LowDirectCancellation {V : Type u_1} (K : SimpleGraph V) (S T : Set V) (a b : V) : Prop

The low direct-shadow cancellation H_a ≅ H_b.

Equations

• K.LowDirectCancellation S T a b = K.FixedHostCardIso S T T a b

def SimpleGraph.ComplementaryDirectCancellation {V : Type u_1} (K : SimpleGraph V) (S T : Set V) (a b : V) : Prop

The complementary direct cancellation C_b^a ≅ C_a^b.

Equations

• K.ComplementaryDirectCancellation S T a b = K.FixedHostCardIso S (SimpleGraph.singletonLeft T a) (SimpleGraph.singletonRight T b) b a

@[reducible, inline]

abbrev SimpleGraph.lowShadowGraph {V : Type u_1} (K : SimpleGraph V) (z : V) : SimpleGraph { w : V // w ≠ z }

The graph underlying a natural low shadow K-z.

Equations

• K.lowShadowGraph z = K.deleteVert z

def SimpleGraph.lowCardASecondColor {V : Type u_1} (T : Set V) (a t : V) : Set { w : V // w ≠ t }

Low-slice A_t = (K-t, S-t, (T-t) ∪ {a}).

Equations

• SimpleGraph.lowCardASecondColor T a t = SimpleGraph.deleteColor (SimpleGraph.singletonLeft T a) t

def SimpleGraph.lowCardBSecondColor {V : Type u_1} (T : Set V) (b t : V) : Set { w : V // w ≠ t }

Low-slice B_t = (K-t, S-t, (T-t) ∪ {b}).

Equations

• SimpleGraph.lowCardBSecondColor T b t = SimpleGraph.deleteColor (SimpleGraph.singletonRight T b) t

def SimpleGraph.compCardASecondColor {V : Type u_1} (T : Set V) (a o : V) : Set { w : V // w ≠ o }

Complementary-slice C_o^a = (K-o, S-o, T ∪ {a}).

Equations

• SimpleGraph.compCardASecondColor T a o = SimpleGraph.deleteColor (SimpleGraph.singletonLeft T a) o

def SimpleGraph.compCardBSecondColor {V : Type u_1} (T : Set V) (b o : V) : Set { w : V // w ≠ o }

Complementary-slice C_o^b = (K-o, S-o, T ∪ {b}).

Equations

• SimpleGraph.compCardBSecondColor T b o = SimpleGraph.deleteColor (SimpleGraph.singletonRight T b) o

@[reducible, inline]

abbrev SimpleGraph.deleteTwoVertex {V : Type u_1} (t o : V) : Type u_1

The two-hole vertex type obtained by deleting t and o.

Equations

• SimpleGraph.deleteTwoVertex t o = { x : V // x ≠ t ∧ x ≠ o }

def SimpleGraph.deleteTwo {V : Type u_1} (K : SimpleGraph V) (t o : V) : SimpleGraph (deleteTwoVertex t o)

The graph K - {t,o}.

Equations

• K.deleteTwo t o = SimpleGraph.induce {x : V | x ≠ t ∧ x ≠ o} K

def SimpleGraph.deleteTwoColor {V : Type u_1} (A : Set V) (t o : V) : Set (deleteTwoVertex t o)

Delete two vertices from a color.

Equations

• SimpleGraph.deleteTwoColor A t o = {x : SimpleGraph.deleteTwoVertex t o | ↑x ∈ A}

@[simp]

theorem SimpleGraph.mem_deleteTwoColor {V : Type u_1} (A : Set V) (t o : V) (x : deleteTwoVertex t o) : x ∈ deleteTwoColor A t o ↔ ↑x ∈ A

def SimpleGraph.twoHoleASecondColor {V : Type u_1} (T : Set V) (a t o : V) : Set (deleteTwoVertex t o)

The a-side two-hole second color (T \ {t}) ∪ {a} on K - {t,o}.

Equations

• SimpleGraph.twoHoleASecondColor T a t o = SimpleGraph.deleteTwoColor (SimpleGraph.singletonLeft T a) t o

def SimpleGraph.twoHoleBSecondColor {V : Type u_1} (T : Set V) (b t o : V) : Set (deleteTwoVertex t o)

The b-side two-hole second color (T \ {t}) ∪ {b} on K - {t,o}.

Equations

• SimpleGraph.twoHoleBSecondColor T b t o = SimpleGraph.deleteTwoColor (SimpleGraph.singletonRight T b) t o

def SimpleGraph.TwoHoleMatch {V : Type u_1} (K : SimpleGraph V) (S T : Set V) (a b t o t' o' : V) : Type u_1

A two-hole match D^a_{t,o} ≅ D^b_{t',o'}.

Equations

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