Testing Graph Invariants

This file contains tests for graph invariants on 5 specific concrete graphs:

1. HouseGraph: A graph on 5 vertices.
2. K4: The complete graph on 4 vertices.
3. PetersenGraph: The Petersen graph on 10 vertices.
4. C6: The cycle graph on 6 vertices.
5. Star5: The star graph with 5 leaves (6 vertices total).

Tests cover: independence_number, dominationNumber, average_distance, diameter, radius, girth, order, size, szeged_index, wiener_index, min_degree, max_degree, average_degree, matching_number, residue, annihilation_number, cvetkovic.

Graph Definitions

def HouseGraph : SimpleGraph (Fin 5)

House Graph: Square 0-1-2-3-0 with roof 4 connected to 2,3.

Equations

• HouseGraph = SimpleGraph.fromEdgeSet {s(0, 1), s(1, 2), s(2, 3), s(3, 0), s(2, 4), s(3, 4)}

instance instDecidableRelFinOfNatNatAdjHouseGraph : DecidableRel HouseGraph.Adj

Equations

• instDecidableRelFinOfNatNatAdjHouseGraph = id inferInstance

@[reducible, inline]

abbrev K4 : SimpleGraph (Fin 4)

K4: Complete graph on 4 vertices.

Equations

• K4 = SimpleGraph.completeGraph (Fin 4)

def PetersenGraph : SimpleGraph (Fin 10)

Petersen Graph on 10 vertices.

Equations

• PetersenGraph = SimpleGraph.fromEdgeSet {s(0, 1), s(1, 2), s(2, 3), s(3, 4), s(4, 0), s(0, 5), s(1, 6), s(2, 7), s(3, 8), s(4, 9), s(5, 7), s(7, 9), s(9, 6), s(6, 8), s(8, 5)}

@[reducible, inline]

abbrev C6 : SimpleGraph (Fin 6)

C6: Cycle graph on 6 vertices.

Equations

• C6 = SimpleGraph.cycleGraph 6

def Star5 : SimpleGraph (Fin 1 ⊕ Fin 5)

Star5: Star graph with center 0 and 5 leaves.

Equations

• Star5 = completeBipartiteGraph (Fin 1) (Fin 5)

House Graph Tests

theorem house_indep : HouseGraph.a = 2

theorem house_dom : HouseGraph.dominationNumber = 2

theorem house_avg_dist : HouseGraph.averageDistance = 7 / 5

theorem house_diameter : HouseGraph.maxEccentricity = 2

theorem house_radius : HouseGraph.minEccentricity = 2

theorem house_girth : HouseGraph.girth = 3

theorem house_order : HouseGraph.n = 5

theorem house_size : HouseGraph.edgeFinset.card = 6

theorem house_szeged : HouseGraph.szegedIndex = 24

theorem house_wiener : HouseGraph.wienerIndex = 14

theorem house_min_deg : HouseGraph.minDegree = 2

theorem house_max_deg : HouseGraph.maxDegree = 3

theorem house_avg_deg : HouseGraph.averageDegree = 12 / 5

theorem house_matching : HouseGraph.m = 2

theorem house_residue : HouseGraph.residue = 2

theorem house_annihilation : HouseGraph.annihilationNumber = 3

theorem house_cvetkovic : HouseGraph.cvetkovic = 3

K4 Tests

theorem K4_indep : K4.a = 1

theorem K4_dom : K4.dominationNumber = 1

theorem K4_avg_dist : K4.averageDistance = 1

theorem K4_diameter : K4.maxEccentricity = 1

theorem K4_radius : K4.minEccentricity = 1

theorem K4_girth : K4.girth = 3

theorem K4_order : K4.n = 4

theorem K4_size : K4.edgeFinset.card = 6

theorem K4_szeged : K4.szegedIndex = 6

theorem K4_wiener : K4.wienerIndex = 6

theorem K4_min_deg : K4.minDegree = 3

theorem K4_max_deg : K4.maxDegree = 3

theorem K4_avg_deg : K4.averageDegree = 3

theorem K4_matching : K4.m = 2

theorem K4_residue : K4.residue = 1

theorem K4_annihilation : K4.annihilationNumber = 2

theorem K4_cvetkovic : K4.cvetkovic = 1

Petersen Graph Tests

theorem petersen_indep : PetersenGraph.a = 4

theorem petersen_dom : PetersenGraph.dominationNumber = 3

theorem petersen_avg_dist : PetersenGraph.averageDistance = 5 / 3

theorem petersen_diameter : PetersenGraph.maxEccentricity = 2

theorem petersen_radius : PetersenGraph.minEccentricity = 2

theorem petersen_girth : PetersenGraph.girth = 5

theorem petersen_order : PetersenGraph.n = 10

theorem petersen_size : PetersenGraph.edgeFinset.card = 15

theorem petersen_szeged : PetersenGraph.szegedIndex = 135

theorem petersen_wiener : PetersenGraph.wienerIndex = 75

theorem petersen_min_deg : PetersenGraph.minDegree = 3

theorem petersen_max_deg : PetersenGraph.maxDegree = 3

theorem petersen_avg_deg : PetersenGraph.averageDegree = 3

theorem petersen_matching : PetersenGraph.m = 5

theorem petersen_residue : PetersenGraph.residue = 3

theorem petersen_annihilation : PetersenGraph.annihilationNumber = 5

theorem petersen_cvetkovic : PetersenGraph.cvetkovic = 4

C6 Tests

theorem C6_indep : C6.a = 3

theorem C6_dom : C6.dominationNumber = 2

theorem C6_avg_dist : C6.averageDistance = 9 / 5

theorem C6_diameter : C6.maxEccentricity = 3

theorem C6_radius : C6.minEccentricity = 3

theorem C6_girth : C6.girth = 6

theorem C6_order : C6.n = 6

theorem C6_size : C6.edgeFinset.card = 6

theorem C6_szeged : C6.szegedIndex = 54

theorem C6_wiener : C6.wienerIndex = 27

theorem C6_min_deg : C6.minDegree = 2

theorem C6_max_deg : C6.maxDegree = 2

theorem C6_avg_deg : C6.averageDegree = 2

theorem C6_matching : C6.m = 3

theorem C6_residue : C6.residue = 2

theorem C6_annihilation : C6.annihilationNumber = 3

theorem C6_cvetkovic : C6.cvetkovic = 3

Star5 Tests

theorem Star5_indep : Star5.a = 5

theorem Star5_dom : Star5.dominationNumber = 1

theorem Star5_avg_dist : Star5.averageDistance = 5 / 3

theorem Star5_diameter : Star5.maxEccentricity = 2

theorem Star5_radius : Star5.minEccentricity = 1

theorem Star5_girth : Star5.egirth = ⊤

theorem Star5_order : Star5.n = 6

theorem Star5_size : Star5.edgeFinset.card = 5

theorem Star5_szeged : Star5.szegedIndex = 25

theorem Star5_wiener : Star5.wienerIndex = 25

theorem Star5_min_deg : Star5.minDegree = 1

theorem Star5_max_deg : Star5.maxDegree = 5

theorem Star5_avg_deg : Star5.averageDegree = 5 / 3

theorem Star5_matching : Star5.m = 1

theorem Star5_residue : Star5.residue = 5

theorem Star5_annihilation : Star5.annihilationNumber = 5

theorem Star5_cvetkovic : Star5.cvetkovic = 5