How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
The Petersen graph has ten vertices, is cubic, has girth five and has
Example
For , the Petersen graph on has ten vertices, is cubic, has girth , and satisfies
Facts & Assumptions
Given: The Petersen graph whose vertices are the two-element subsets of , adjacent exactly when disjoint.
This is the Petersen graph of The Petersen graph on the two-element subsets of a five-element set, adjacent when disjoint.
An -element set has two-element subsets (A finite set with elements has exactly two-element subsets, and ).
Girth is the least cycle length, with the acyclic convention (Graph distance within a component, eccentricity, diameter and girth, including the acyclic convention).
and are the minimum sizes of vertex and edge cuts (Vertex cuts, edge cuts, vertex connectivity and edge connectivity , with conventions for complete and one-vertex graphs).
Whitney's inequalities give for a nontrivial connected graph (Whitney's inequalities: for every nontrivial connected graph).
Verification
The vertex set has elements by [L1]. For a vertex , its neighbours are the two-element subsets of the three-element complement , so it has neighbours. Thus is cubic and .
If distinct vertices are disjoint, their union has four elements and there is no two-element subset disjoint from both. If they intersect, their union has three elements and its two-element complement is their unique common neighbour.
Deleting any two vertices leaves a connected graph. Up to relabelling , two deleted two-element subsets are either the disjoint pair or the intersecting pair . In the first case the remaining vertices have the spanning path ; in the second they have the spanning path . Every successive pair displayed is disjoint. Relabelling preserves disjointness, so these cases cover every pair.
There is no triangle: adjacent vertices are disjoint and have no common neighbour by step 1.2. There is no -cycle, because its two opposite vertices would have two distinct common neighbours, also impossible by step 1.2.
Every two distinct vertices are at distance at most : disjoint ones are adjacent, and intersecting ones have the common neighbour from step 1.2. Hence is connected.
The vertices in that order form a -cycle, since consecutive sets, including and , are disjoint. With step 2.1 and [F2], this proves .
No set of at most two edges disconnects . Indeed, if such a deletion produced a component on a smallest vertex set , then . Writing for the number of edges inside , cubicity gives edges leaving . For this number is at least , since a simple triangle-free graph on those sizes has at most edges. For , the absence of triangles and -cycles makes the induced graph acyclic, so it has at most edges and at least edges leave. For , it is either acyclic with at most edges or is a chordless -cycle with edges, so at least edges leave. Every case has at least three boundary edges, a contradiction. Therefore .
Deleting one vertex also leaves a connected graph: choose a second vertex, use step 1.3 on the remaining eight, and then add the second vertex back; it retains at least two of its three neighbours. Step 2.2 covers deletion of no vertices. Thus no vertex cut has size at most , and .
By [L2] and step 1.1, . Together with step 3.2 this gives .
Whitney's inequality [L2] and step 4.1 give , while step 3.3 gives the reverse bound. Hence ; both lower bounds were obtained in steps 3.2 and 3.3, which use the cubic regularity of .
Depends on
- The Petersen graph on the two-element subsets of a five-element set, adjacent when disjoint
- A finite set with $n$ elements has exactly $\binom{n}{2}$ two-element subsets, and $2\binom{n}{2} = n(n-1)$
- Graph distance within a component, eccentricity, diameter and girth, including the acyclic convention
- Vertex cuts, edge cuts, vertex connectivity $\kappa(G)$ and edge connectivity $\lambda(G)$, with conventions for complete and one-vertex graphs
- Whitney's inequalities: $\kappa(G)\le\lambda(G)\le\delta(G)$ for every nontrivial connected graph
Used by
Nothing in the library uses this result yet.
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 64 results over 19 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.
Sources
- R. Diestel, Graph Theory, Chapter 1 preview (standard reference, not scraped)