def hasMonoStar {V : Type u_1} (G : SimpleGraph V) (color : Sym2 V → Fin 2) (col : Fin 2) (k : ℕ) : Prop

“Color-col monochromatic star of size k”: there is a center x and a set S of k distinct neighbors of x such that every edge {x,y} with y ∈ S is present in G and colored col. (No restriction on edges inside S.)

Equations

• hasMonoStar G color col k = ∃ (x : V) (S : Finset V), S.card = k ∧ x ∉ S ∧ ∀ ⦃y : V⦄, y ∈ S → G.Adj x y ∧ color s(x, y) = col

def hasMonoTriangle {V : Type u_1} (G : SimpleGraph V) (color : Sym2 V → Fin 2) (col : Fin 2) : Prop

“Color-col monochromatic triangle”: there exist a b c with all three edges present in G and colored col. (Adjacency already forces distinctness.)

Equations

• hasMonoTriangle G color col = ∃ (a : V) (b : V) (c : V), G.Adj a b ∧ G.Adj b c ∧ G.Adj a c ∧ color s(a, b) = col ∧ color s(b, c) = col ∧ color s(a, c) = col

def Pikhurko_n5_statement : Prop

Statement (n = 5 case of Pikhurko’s counterexample). There exists a simple graph on 16 vertices with exactly 44 edges such that for every 2‑coloring of unordered pairs, either color 0 contains a K_{1,5} (a 5‑edge star) or color 1 contains a K₃ (a triangle).

This only states the claim (as a Prop). You can later prove it from the explicit construction, or assume it as an axiom while you develop the rest.

Equations

• Pikhurko_n5_statement = ∃ (V : Type) (G : SimpleGraph V), G.edgeSet.ncard = 44 ∧ ∀ (color : Sym2 V → Fin 2), hasMonoStar G color 0 5 ∨ hasMonoTriangle G color 1

inductive PikhurkoN5.V : Type

Vertex type with 2 + 5 + 3 + 5 + 1 = 16 vertices.

• A1 (i : Fin 2) : V
• B1 (j : Fin 5) : V
• A2 (i : Fin 3) : V
• B2 (j : Fin 5) : V
• apex : V

instance PikhurkoN5.instDecidableEqV : DecidableEq V

Equations

• PikhurkoN5.instDecidableEqV = PikhurkoN5.decEqV✝

instance PikhurkoN5.instReprV : Repr V

Equations

• PikhurkoN5.instReprV = { reprPrec := PikhurkoN5.reprV✝ }

def PikhurkoN5.GAdj : V → V → Prop

Adjacency relation for the Pikhurko n=5 counterexample.

• Inside A1 and inside A2: cliques.
• Between A1–B1 and A2–B2: complete bipartite.
• Inside B1 and B2: no edges.
• No edges between the two blocks {A1,B1} and {A2,B2}.
• apex is connected to every non-apex vertex.

Equations

• PikhurkoN5.GAdj PikhurkoN5.V.apex PikhurkoN5.V.apex = False
• PikhurkoN5.GAdj PikhurkoN5.V.apex x✝ = True
• PikhurkoN5.GAdj x PikhurkoN5.V.apex = True
• PikhurkoN5.GAdj (PikhurkoN5.V.A1 i) (PikhurkoN5.V.A1 j) = (i ≠ j)
• PikhurkoN5.GAdj (PikhurkoN5.V.A2 i) (PikhurkoN5.V.A2 j) = (i ≠ j)
• PikhurkoN5.GAdj (PikhurkoN5.V.A1 i) (PikhurkoN5.V.B1 j) = True
• PikhurkoN5.GAdj (PikhurkoN5.V.B1 j) (PikhurkoN5.V.A1 i) = True
• PikhurkoN5.GAdj (PikhurkoN5.V.A2 i) (PikhurkoN5.V.B2 j) = True
• PikhurkoN5.GAdj (PikhurkoN5.V.B2 j) (PikhurkoN5.V.A2 i) = True
• PikhurkoN5.GAdj x✝¹ x✝ = False

def PikhurkoN5.G : SimpleGraph V

The graph G on 16 vertices used for the n=5 counterexample.

Equations

• PikhurkoN5.G = { Adj := PikhurkoN5.GAdj, symm := PikhurkoN5.G._proof_1, loopless := PikhurkoN5.G._proof_2 }

Convenience simp lemmas. These are optional but help when you start proving properties about colorings later on.

@[simp]

theorem PikhurkoN5.adj_apex_left {v : V} : G.Adj V.apex v ↔ v ≠ V.apex

@[simp]

theorem PikhurkoN5.adj_apex_right {v : V} : G.Adj v V.apex ↔ v ≠ V.apex

@[simp]

theorem PikhurkoN5.adj_A1A1 {i j : Fin 2} : G.Adj (V.A1 i) (V.A1 j) ↔ i ≠ j

@[simp]

theorem PikhurkoN5.adj_A2A2 {i j : Fin 3} : G.Adj (V.A2 i) (V.A2 j) ↔ i ≠ j

@[simp]

theorem PikhurkoN5.adj_A1B1 {i : Fin 2} {j : Fin 5} : G.Adj (V.A1 i) (V.B1 j)

@[simp]

theorem PikhurkoN5.adj_B1A1 {i : Fin 5} {j : Fin 2} : G.Adj (V.B1 i) (V.A1 j)

@[simp]

theorem PikhurkoN5.adj_A2B2 {i : Fin 3} {j : Fin 5} : G.Adj (V.A2 i) (V.B2 j)

@[simp]

theorem PikhurkoN5.adj_B2A2 {i : Fin 3} {j : Fin 5} : G.Adj (V.B2 j) (V.A2 i)

@[simp]

theorem PikhurkoN5.no_adj_B1B1 {j j' : Fin 5} : ¬G.Adj (V.B1 j) (V.B1 j')

@[simp]

theorem PikhurkoN5.no_adj_B2B2 {j j' : Fin 5} : ¬G.Adj (V.B2 j) (V.B2 j')

@[simp]

theorem PikhurkoN5.no_cross_blocks_A1B2 {i : Fin 2} {j : Fin 5} : ¬G.Adj (V.A1 i) (V.B2 j)

@[simp]

theorem PikhurkoN5.no_cross_blocks_A2B1 {i : Fin 3} {j : Fin 5} : ¬G.Adj (V.A2 i) (V.B1 j)

@[simp]

theorem PikhurkoN5.no_cross_blocks_B1A2 {i : Fin 3} {j : Fin 5} : ¬G.Adj (V.B1 j) (V.A2 i)

@[simp]

theorem PikhurkoN5.no_cross_blocks_B1B2 {i j : Fin 5} : ¬G.Adj (V.B1 j) (V.B2 i)

@[simp]

theorem PikhurkoN5.no_cross_blocks_A2A1 {i : Fin 2} {j : Fin 3} : ¬G.Adj (V.A2 j) (V.A1 i)

instance PikhurkoN5.instFintypeV : Fintype V

Equations

• PikhurkoN5.instFintypeV = Fintype.ofEquiv (Fin 2 ⊕ Fin 5 ⊕ Fin 3 ⊕ Fin 5 ⊕ Unit) PikhurkoN5.V.proxyTypeEquiv

def PikhurkoN5.VEquiv : V ≃ (((Fin 2 ⊕ Fin 5) ⊕ Fin 3) ⊕ Fin 5) ⊕ Unit

An explicit equivalence showing V has 2+5+3+5+1 = 16 elements.

Equations

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

theorem PikhurkoN5.card_V : Fintype.card V = 16

|V| = 16. Useful for quick cardinality arithmetic.

Degree computations

We compute the degree of each vertex kind. We’ll use your [simp] adjacency lemmas from Approach A:

• adj_apex_left, adj_A1A1, adj_A2A2, adj_A1B1, adj_A2B2, and the corresponding “no edge” lemmas across blocks.

theorem PikhurkoN5.degree_apex : G.degree V.apex = 15

deg(apex) = 15.

theorem PikhurkoN5.degree_A1 (i : Fin 2) : G.degree (V.A1 i) = 7

deg(A1 i) = 7 for each i.

theorem PikhurkoN5.degree_B1 (j : Fin 5) : G.degree (V.B1 j) = 3

deg(B1 j) = 3 for each j. (Two A1s + apex.)

theorem PikhurkoN5.degree_A2 (i : Fin 3) : G.degree (V.A2 i) = 8

deg(A2 i) = 8 for each i. (Two inside A2 + five in B2 + apex.)

theorem PikhurkoN5.degree_B2 (j : Fin 5) : G.degree (V.B2 j) = 4

deg(B2 j) = 4 for each j. (Three A2s + apex.)

Edge count via the handshaking lemma

We now sum the degrees and divide by 2.

theorem PikhurkoN5.edge_count_44 : G.edgeSet.ncard = 44

Small utilities

theorem PikhurkoN5.Finset.exists_subset_card_eq {α : Type u_1} (s : Finset α) {k : ℕ} (hk : k ≤ s.card) : ∃ t ⊆ s, t.card = k

theorem PikhurkoN5.fin2_eq_one_iff_ne_zero (a : Fin 2) : a = 1 ↔ a ≠ 0

In Fin 2, saying “equals 1” is the same as “not equal to 0”.

Red neighbors of the apex are ≥ 11 if there is no blue star K_{1,5}

noncomputable def PikhurkoN5.blueNeighbors (color : Sym2 V → Fin 2) : Finset V

The set of blue neighbors of apex in color class 0.

Equations

• PikhurkoN5.blueNeighbors color = {v ∈ PikhurkoN5.G.neighborFinset PikhurkoN5.V.apex | color s(PikhurkoN5.V.apex, v) = 0}

noncomputable def PikhurkoN5.redNeighbors (color : Sym2 V → Fin 2) : Finset V

The set of red neighbors of apex in color class 1.

Equations

• PikhurkoN5.redNeighbors color = {v ∈ PikhurkoN5.G.neighborFinset PikhurkoN5.V.apex | color s(PikhurkoN5.V.apex, v) = 1}

theorem PikhurkoN5.blueNeighbors_card_le_4 (color : Sym2 V → Fin 2) (hNoBlueStar : ¬hasMonoStar G color 0 5) : (blueNeighbors color).card ≤ 4

If there is no blue K_{1,5}, then the apex has at most 4 blue neighbors.

theorem PikhurkoN5.red_from_apex_at_least_11 (color : Sym2 V → Fin 2) (hNoBlueStar : ¬hasMonoStar G color 0 5) : (redNeighbors color).card ≥ 11

If there is no blue K_{1,5}, then at least 11 neighbors of apex are red.

def PikhurkoN5.inBlock1 : V → Prop

Membership in the first block {A1, B1}.

Equations

• PikhurkoN5.inBlock1 (PikhurkoN5.V.A1 i) = True
• PikhurkoN5.inBlock1 (PikhurkoN5.V.B1 j) = True
• PikhurkoN5.inBlock1 x✝ = False

noncomputable instance PikhurkoN5.instDecidablePredVInBlock1 : DecidablePred inBlock1

Equations

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

noncomputable def PikhurkoN5.redBlock1 (color : Sym2 V → Fin 2) : Finset V

Red neighbors of apex that lie in the first block {A1,B1}.

Equations

• PikhurkoN5.redBlock1 color = {v ∈ PikhurkoN5.redNeighbors color | PikhurkoN5.inBlock1 v}

noncomputable def PikhurkoN5.redBlock2 (color : Sym2 V → Fin 2) : Finset V

Red neighbors of apex that lie in the second block {A2,B2}.

We implement this as the complement of inBlock1 inside redNeighbors. Since apex ∉ redNeighbors color, this is exactly the {A2,B2} part.

Equations

• PikhurkoN5.redBlock2 color = {v ∈ PikhurkoN5.redNeighbors color | ¬PikhurkoN5.inBlock1 v}

theorem PikhurkoN5.redBlocks_partition_card (color : Sym2 V → Fin 2) : (redBlock1 color).card + (redBlock2 color).card = (redNeighbors color).card

Partition of the red neighbors of apex into the two blocks.

theorem PikhurkoN5.exists_block_receives_at_least_6_red (color : Sym2 V → Fin 2) (hNoBlueStar : ¬hasMonoStar G color 0 5) : (redBlock1 color).card ≥ 6 ∨ (redBlock2 color).card ≥ 6

Pigeonhole step. If there is no blue K_{1,5}, then one of the two blocks receives at least six red edges from apex.

Part / block predicates

def PikhurkoN5.isA1 : V → Prop

Recognizes the clique side A1.

Equations

• PikhurkoN5.isA1 (PikhurkoN5.V.A1 i) = True
• PikhurkoN5.isA1 x✝ = False

def PikhurkoN5.isB1 : V → Prop

Recognizes the independent side B1.

Equations

• PikhurkoN5.isB1 (PikhurkoN5.V.B1 j) = True
• PikhurkoN5.isB1 x✝ = False

def PikhurkoN5.isA2 : V → Prop

Recognizes the clique side A2.

Equations

• PikhurkoN5.isA2 (PikhurkoN5.V.A2 i) = True
• PikhurkoN5.isA2 x✝ = False

def PikhurkoN5.isB2 : V → Prop

Recognizes the independent side B2.

Equations

• PikhurkoN5.isB2 (PikhurkoN5.V.B2 j) = True
• PikhurkoN5.isB2 x✝ = False

def PikhurkoN5.inBlock2 : V → Prop

Second block {A2,B2}.

Equations

• PikhurkoN5.inBlock2 (PikhurkoN5.V.A2 i) = True
• PikhurkoN5.inBlock2 (PikhurkoN5.V.B2 j) = True
• PikhurkoN5.inBlock2 x✝ = False

noncomputable instance PikhurkoN5.instDecidablePredVIsA1 : DecidablePred isA1

Equations

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

noncomputable instance PikhurkoN5.instDecidablePredVIsB1 : DecidablePred isB1

Equations

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

noncomputable instance PikhurkoN5.instDecidablePredVIsA2 : DecidablePred isA2

Equations

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

noncomputable instance PikhurkoN5.instDecidablePredVIsB2 : DecidablePred isB2

Equations

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

noncomputable instance PikhurkoN5.instDecidablePredVInBlock1_1 : DecidablePred inBlock1

Equations

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

noncomputable instance PikhurkoN5.instDecidablePredVInBlock2 : DecidablePred inBlock2

Equations

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

@[simp]

theorem PikhurkoN5.inBlock1_iff (v : V) : inBlock1 v ↔ isA1 v ∨ isB1 v

@[simp]

theorem PikhurkoN5.inBlock2_iff (v : V) : inBlock2 v ↔ isA2 v ∨ isB2 v

@[simp]

theorem PikhurkoN5.not_isA1_and_isB1 (v : V) : ¬(isA1 v ∧ isB1 v)

@[simp]

theorem PikhurkoN5.not_isA2_and_isB2 (v : V) : ¬(isA2 v ∧ isB2 v)

Splitting the apex red neighbors by parts

noncomputable def PikhurkoN5.redBlock1A1 (color : Sym2 V → Fin 2) : Finset V

Further refine redBlock1 into its A1 and B1 parts.

Equations

• PikhurkoN5.redBlock1A1 color = {v ∈ PikhurkoN5.redNeighbors color | PikhurkoN5.isA1 v}

noncomputable def PikhurkoN5.redBlock1B1 (color : Sym2 V → Fin 2) : Finset V

Equations

• PikhurkoN5.redBlock1B1 color = {v ∈ PikhurkoN5.redNeighbors color | PikhurkoN5.isB1 v}

noncomputable def PikhurkoN5.redBlock2A2 (color : Sym2 V → Fin 2) : Finset V

Further refine redBlock2 into its A2 and B2 parts.

Equations

• PikhurkoN5.redBlock2A2 color = {v ∈ PikhurkoN5.redNeighbors color | PikhurkoN5.isA2 v}

noncomputable def PikhurkoN5.redBlock2B2 (color : Sym2 V → Fin 2) : Finset V

Equations

• PikhurkoN5.redBlock2B2 color = {v ∈ PikhurkoN5.redNeighbors color | PikhurkoN5.isB2 v}

theorem PikhurkoN5.redBlock1_eq_union (color : Sym2 V → Fin 2) : redBlock1 color = redBlock1A1 color ∪ redBlock1B1 color

redBlock1 is exactly the disjoint union of its A1 and B1 parts.

theorem PikhurkoN5.redBlock2_eq_union (color : Sym2 V → Fin 2) : redBlock2 color = redBlock2A2 color ∪ redBlock2B2 color

redBlock2 is exactly the disjoint union of its A2 and B2 parts.

theorem PikhurkoN5.redA1_redB1_disjoint (color : Sym2 V → Fin 2) : Disjoint (redBlock1A1 color) (redBlock1B1 color)

The two parts of redBlock1 are disjoint.

theorem PikhurkoN5.redA2_redB2_disjoint (color : Sym2 V → Fin 2) : Disjoint (redBlock2A2 color) (redBlock2B2 color)

The two parts of redBlock2 are disjoint.

theorem PikhurkoN5.redBlock1_card_eq_sum (color : Sym2 V → Fin 2) : (redBlock1 color).card = (redBlock1A1 color).card + (redBlock1B1 color).card

Cardinal decompositions of the blocks.

theorem PikhurkoN5.redBlock2_card_eq_sum (color : Sym2 V → Fin 2) : (redBlock2 color).card = (redBlock2A2 color).card + (redBlock2B2 color).card

Bounding the B-parts by 5

def PikhurkoN5.B1Set : Finset V

All B1-vertices as a finset (image of Fin 5).

Equations

• PikhurkoN5.B1Set = Finset.image (fun (j : Fin 5) => PikhurkoN5.V.B1 j) Finset.univ

def PikhurkoN5.B2Set : Finset V

All B2-vertices as a finset (image of Fin 5).

Equations

• PikhurkoN5.B2Set = Finset.image (fun (j : Fin 5) => PikhurkoN5.V.B2 j) Finset.univ

theorem PikhurkoN5.redBlock1B1_subset_B1Set (color : Sym2 V → Fin 2) : redBlock1B1 color ⊆ B1Set

theorem PikhurkoN5.redBlock2B2_subset_B2Set (color : Sym2 V → Fin 2) : redBlock2B2 color ⊆ B2Set

theorem PikhurkoN5.card_B1Set_le_5 : B1Set.card ≤ 5

theorem PikhurkoN5.card_B2Set_le_5 : B2Set.card ≤ 5

theorem PikhurkoN5.redBlock1B1_card_le_5 (color : Sym2 V → Fin 2) : (redBlock1B1 color).card ≤ 5

theorem PikhurkoN5.redBlock2B2_card_le_5 (color : Sym2 V → Fin 2) : (redBlock2B2 color).card ≤ 5

Existence of a red neighbor in the clique parts A1 / A2

theorem PikhurkoN5.exists_red_A1_of_block1_ge6 (color : Sym2 V → Fin 2) (h6 : 6 ≤ (redBlock1 color).card) : ∃ (i : Fin 2), G.Adj V.apex (V.A1 i) ∧ color s(V.apex, V.A1 i) = 1

If block 1 receives at least 6 red neighbors from apex, then one of them lies in A1.

theorem PikhurkoN5.exists_red_A2_of_block2_ge6 (color : Sym2 V → Fin 2) (h6 : 6 ≤ (redBlock2 color).card) : ∃ (i : Fin 3), G.Adj V.apex (V.A2 i) ∧ color s(V.apex, V.A2 i) = 1

If block 2 receives at least 6 red neighbors from apex, then one of them lies in A2.

theorem PikhurkoN5.exists_red_clique_neighbor (color : Sym2 V → Fin 2) (hNoBlueStar : ¬hasMonoStar G color 0 5) : (∃ (i : Fin 2), G.Adj V.apex (V.A1 i) ∧ color s(V.apex, V.A1 i) = 1) ∨ ∃ (i : Fin 3), G.Adj V.apex (V.A2 i) ∧ color s(V.apex, V.A2 i) = 1

Corollary: under the “no blue star” hypothesis, there is a red neighbor of apex in the appropriate clique A1 or A2.

Helpers: the chosen clique vertex lies in the corresponding red block

theorem PikhurkoN5.A1_mem_redBlock1_of_red (color : Sym2 V → Fin 2) (i : Fin 2) (_hAdj : G.Adj V.apex (V.A1 i)) (hRed : color s(V.apex, V.A1 i) = 1) : V.A1 i ∈ redBlock1 color

theorem PikhurkoN5.A2_mem_redBlock2_of_red (color : Sym2 V → Fin 2) (i : Fin 3) (_hAdj : G.Adj V.apex (V.A2 i)) (hRed : color s(V.apex, V.A2 i) = 1) : V.A2 i ∈ redBlock2 color

Triangle-or-star from Block 1

theorem PikhurkoN5.triangle_or_blueStar_from_block1 (color : Sym2 V → Fin 2) (h6 : 6 ≤ (redBlock1 color).card) (i : Fin 2) (hAdj : G.Adj V.apex (V.A1 i)) (hRedApexA1 : color s(V.apex, V.A1 i) = 1) : hasMonoTriangle G color 1 ∨ hasMonoStar G color 0 5

If Block 1 has at least 6 red apex-neighbors, and one of them is A1 i with a red edge from apex, then either we have a red triangle, or a blue K_{1,5} centered at A1 i.

Triangle-or-star from Block 2 (same proof pattern)

theorem PikhurkoN5.triangle_or_blueStar_from_block2 (color : Sym2 V → Fin 2) (h6 : 6 ≤ (redBlock2 color).card) (i : Fin 3) (hAdj : G.Adj V.apex (V.A2 i)) (hRedApexA2 : color s(V.apex, V.A2 i) = 1) : hasMonoTriangle G color 1 ∨ hasMonoStar G color 0 5

Final step: no blue K_{1,5} ⇒ a red triangle

theorem PikhurkoN5.red_triangle_of_no_blue_star (color : Sym2 V → Fin 2) (hNoBlueStar : ¬hasMonoStar G color 0 5) : hasMonoTriangle G color 1

Main step (n=5): If there is no blue K_{1,5}, then the red color class contains a triangle.

theorem PikhurkoN5.main : Pikhurko_n5_statement