Documentation

FormalConjectures.WrittenOnTheWallII.Test

Testing Graph Invariants #

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

HouseGraph: A graph on 5 vertices.
K4: The complete graph on 4 vertices.
PetersenGraph: The Petersen graph on 10 vertices.
C6: The cycle graph on 6 vertices.
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.

@[reducible, inline]

abbrev WrittenOnTheWallII.Test.HouseGraph :

SimpleGraph (Fin 5)

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

Equations

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

Instances For

@[reducible, inline]

abbrev WrittenOnTheWallII.Test.K4 :

SimpleGraph (Fin 4)

K4: Complete graph on 4 vertices.

Equations

WrittenOnTheWallII.Test.K4 = SimpleGraph.completeGraph (Fin 4)

Instances For

@[reducible, inline]

abbrev WrittenOnTheWallII.Test.PetersenGraph :

SimpleGraph (Fin 10)

Petersen Graph on 10 vertices.

Equations

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

Instances For

@[reducible, inline]

abbrev WrittenOnTheWallII.Test.C6 :

SimpleGraph (Fin 6)

C6: Cycle graph on 6 vertices.

Equations

WrittenOnTheWallII.Test.C6 = SimpleGraph.cycleGraph 6

Instances For

@[reducible, inline]

abbrev WrittenOnTheWallII.Test.Star5 :

SimpleGraph (Fin 1 ⊕ Fin 5)

Star5: Star graph with center 0 and 5 leaves.

Equations

WrittenOnTheWallII.Test.Star5 = completeBipartiteGraph (Fin 1) (Fin 5)

Instances For

instance WrittenOnTheWallII.Test.instDecidableRelSumFinOfNatNatAdjStar5 :

DecidableRel Star5.Adj

Equations

WrittenOnTheWallII.Test.instDecidableRelSumFinOfNatNatAdjStar5 = id (id inferInstance)

theorem WrittenOnTheWallII.Test.house_indep :

HouseGraph.indepNum = 2

theorem WrittenOnTheWallII.Test.house_dom :

HouseGraph.dominationNumber = 2

theorem WrittenOnTheWallII.Test.house_avg_dist :

HouseGraph.averageDistance = 7 / 5

theorem WrittenOnTheWallII.Test.house_diameter :

HouseGraph.maxEccentricity = 2

theorem WrittenOnTheWallII.Test.house_radius :

HouseGraph.minEccentricity = 2

theorem WrittenOnTheWallII.Test.house_girth :

HouseGraph.girth = 3

theorem WrittenOnTheWallII.Test.house_order :

HouseGraph.n = 5

theorem WrittenOnTheWallII.Test.house_size :

HouseGraph.edgeFinset.card = 6

theorem WrittenOnTheWallII.Test.house_szeged :

HouseGraph.szegedIndex = 24

theorem WrittenOnTheWallII.Test.house_wiener :

HouseGraph.wienerIndex = 14

theorem WrittenOnTheWallII.Test.house_min_deg :

HouseGraph.minDegree = 2

theorem WrittenOnTheWallII.Test.house_max_deg :

HouseGraph.maxDegree = 3

theorem WrittenOnTheWallII.Test.house_avg_deg :

HouseGraph.averageDegree = 12 / 5

theorem WrittenOnTheWallII.Test.house_matching :

HouseGraph.m = 2

theorem WrittenOnTheWallII.Test.house_residue :

HouseGraph.residue = 0

theorem WrittenOnTheWallII.Test.house_annihilation :

HouseGraph.annihilationNumber = 3

theorem WrittenOnTheWallII.Test.house_cvetkovic :

HouseGraph.cvetkovic = 3

theorem WrittenOnTheWallII.Test.K4_indep :

K4.indepNum = 1

theorem WrittenOnTheWallII.Test.K4_dom :

K4.dominationNumber = 1

theorem WrittenOnTheWallII.Test.K4_avg_dist :

K4.averageDistance = 1

theorem WrittenOnTheWallII.Test.K4_diameter :

K4.maxEccentricity = 1

theorem WrittenOnTheWallII.Test.K4_radius :

K4.minEccentricity = 1

theorem WrittenOnTheWallII.Test.K4_girth :

theorem WrittenOnTheWallII.Test.K4_order :

K4.n = 4

theorem WrittenOnTheWallII.Test.K4_size :

K4.edgeFinset.card = 6

theorem WrittenOnTheWallII.Test.K4_szeged :

K4.szegedIndex = 6

theorem WrittenOnTheWallII.Test.K4_wiener :

K4.wienerIndex = 6

theorem WrittenOnTheWallII.Test.K4_min_deg :

K4.minDegree = 3

theorem WrittenOnTheWallII.Test.K4_max_deg :

K4.maxDegree = 3

theorem WrittenOnTheWallII.Test.K4_avg_deg :

K4.averageDegree = 3

theorem WrittenOnTheWallII.Test.K4_matching :

K4.m = 2

theorem WrittenOnTheWallII.Test.K4_residue :

theorem WrittenOnTheWallII.Test.K4_annihilation :

K4.annihilationNumber = 2

theorem WrittenOnTheWallII.Test.K4_cvetkovic :

K4.cvetkovic = 1

theorem WrittenOnTheWallII.Test.petersen_indep :

PetersenGraph.indepNum = 4

theorem WrittenOnTheWallII.Test.petersen_dom :

PetersenGraph.dominationNumber = 3

theorem WrittenOnTheWallII.Test.petersen_avg_dist :

PetersenGraph.averageDistance = 5 / 3

theorem WrittenOnTheWallII.Test.petersen_diameter :

PetersenGraph.maxEccentricity = 2

theorem WrittenOnTheWallII.Test.petersen_radius :

PetersenGraph.minEccentricity = 2

theorem WrittenOnTheWallII.Test.petersen_girth :

PetersenGraph.girth = 5

theorem WrittenOnTheWallII.Test.petersen_order :

PetersenGraph.n = 10

theorem WrittenOnTheWallII.Test.petersen_size :

PetersenGraph.edgeFinset.card = 15

theorem WrittenOnTheWallII.Test.petersen_szeged :

PetersenGraph.szegedIndex = 135

theorem WrittenOnTheWallII.Test.petersen_wiener :

PetersenGraph.wienerIndex = 75

theorem WrittenOnTheWallII.Test.petersen_min_deg :

PetersenGraph.minDegree = 3

theorem WrittenOnTheWallII.Test.petersen_max_deg :

PetersenGraph.maxDegree = 3

theorem WrittenOnTheWallII.Test.petersen_avg_deg :

PetersenGraph.averageDegree = 3

theorem WrittenOnTheWallII.Test.petersen_matching :

PetersenGraph.m = 5

theorem WrittenOnTheWallII.Test.petersen_residue :

PetersenGraph.residue = 0

theorem WrittenOnTheWallII.Test.petersen_annihilation :

PetersenGraph.annihilationNumber = 5

theorem WrittenOnTheWallII.Test.petersen_cvetkovic :

PetersenGraph.cvetkovic = 4

theorem WrittenOnTheWallII.Test.C6_indep :

C6.indepNum = 3

theorem WrittenOnTheWallII.Test.C6_dom :

C6.dominationNumber = 2

theorem WrittenOnTheWallII.Test.C6_avg_dist :

C6.averageDistance = 9 / 5

theorem WrittenOnTheWallII.Test.C6_diameter :

C6.maxEccentricity = 3

theorem WrittenOnTheWallII.Test.C6_radius :

C6.minEccentricity = 3

theorem WrittenOnTheWallII.Test.C6_girth :

theorem WrittenOnTheWallII.Test.C6_order :

C6.n = 6

theorem WrittenOnTheWallII.Test.C6_size :

C6.edgeFinset.card = 6

theorem WrittenOnTheWallII.Test.C6_szeged :

C6.szegedIndex = 54

theorem WrittenOnTheWallII.Test.C6_wiener :

C6.wienerIndex = 27

theorem WrittenOnTheWallII.Test.C6_min_deg :

C6.minDegree = 2

theorem WrittenOnTheWallII.Test.C6_max_deg :

C6.maxDegree = 2

theorem WrittenOnTheWallII.Test.C6_avg_deg :

C6.averageDegree = 2

theorem WrittenOnTheWallII.Test.C6_matching :

C6.m = 3

theorem WrittenOnTheWallII.Test.C6_residue :

theorem WrittenOnTheWallII.Test.C6_annihilation :

C6.annihilationNumber = 3

theorem WrittenOnTheWallII.Test.C6_cvetkovic :

C6.cvetkovic = 3

theorem WrittenOnTheWallII.Test.Star5_indep :

Star5.indepNum = 5

theorem WrittenOnTheWallII.Test.Star5_dom :

Star5.dominationNumber = 1

theorem WrittenOnTheWallII.Test.Star5_avg_dist :

Star5.averageDistance = 5 / 3

theorem WrittenOnTheWallII.Test.Star5_diameter :

Star5.maxEccentricity = 2

theorem WrittenOnTheWallII.Test.Star5_radius :

Star5.minEccentricity = 1

theorem WrittenOnTheWallII.Test.Star5_girth :

Star5.egirth = ⊤

theorem WrittenOnTheWallII.Test.Star5_order :

theorem WrittenOnTheWallII.Test.Star5_size :

Star5.edgeFinset.card = 5

theorem WrittenOnTheWallII.Test.Star5_szeged :

Star5.szegedIndex = 25

theorem WrittenOnTheWallII.Test.Star5_wiener :

Star5.wienerIndex = 25

theorem WrittenOnTheWallII.Test.Star5_min_deg :

Star5.minDegree = 1

theorem WrittenOnTheWallII.Test.Star5_max_deg :

Star5.maxDegree = 5

theorem WrittenOnTheWallII.Test.Star5_avg_deg :

Star5.averageDegree = 5 / 3

theorem WrittenOnTheWallII.Test.Star5_matching :

theorem WrittenOnTheWallII.Test.Star5_residue :

Star5.residue = 5

theorem WrittenOnTheWallII.Test.Star5_annihilation :

Star5.annihilationNumber = 5

theorem WrittenOnTheWallII.Test.Star5_cvetkovic :

Star5.cvetkovic = 5