Alphabeta Math
ExampleConstruction: AI-adaptedVerification: AI-generatedprecheck passverified 2026-08-04 (gpt-5.6-sol-codex-subscription)
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 κ=λ=3

Example

For Ω={1,2,3,4,5}, the Petersen graph on [Ω]2 has ten vertices, is cubic, has girth 5, and satisfies

κ(G)=λ(G)=3.

12341523453525241413the5-cycle12;34;15;23;45;12

Facts & Assumptions

Given: The Petersen graph G whose vertices are the two-element subsets of Ω={1,2,3,4,5}, adjacent exactly when disjoint.

[F2]
[L2]

Whitney's inequalities give κ(G)≤λ(G)≤δ(G) for a nontrivial connected graph (Whitney's inequalities: κ(G)≤λ(G)≤δ(G) for every nontrivial connected graph).

Verification

technique · direct
1.1

The vertex set has (52)=10 elements by [L1]. For a vertex A, its neighbours are the two-element subsets of the three-element complement Ω∖A, so it has (32)=3 neighbours. Thus G is cubic and δ(G)=3.

F1L1algebra
1.2

If distinct vertices A,B 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.

F1
1.3

Deleting any two vertices leaves a connected graph. Up to relabelling Ω, two deleted two-element subsets are either the disjoint pair 12,34 or the intersecting pair 12,13. In the first case the remaining vertices have the spanning path 13,25,14,35,24,15,23,45; in the second they have the spanning path 24,35,14,25,34,15,23,45. Every successive pair displayed is disjoint. Relabelling preserves disjointness, so these cases cover every pair.

F1
2.1

There is no triangle: adjacent vertices are disjoint and have no common neighbour by step 1.2. There is no 4-cycle, because its two opposite vertices would have two distinct common neighbours, also impossible by step 1.2.

step 1.2
2.2

Every two distinct vertices are at distance at most 2: disjoint ones are adjacent, and intersecting ones have the common neighbour from step 1.2. Hence G is connected.

step 1.2F1
3.1

The vertices 12,34,15,23,45 in that order form a 5-cycle, since consecutive sets, including 45 and 12, are disjoint. With step 2.1 and [F2], this proves g(G)=5.

step 2.1F1F2
3.2

No set of at most two edges disconnects G. Indeed, if such a deletion produced a component on a smallest vertex set S, then 1≤∣S∣≤5. Writing e(S) for the number of edges inside S, cubicity gives 3∣S∣−2e(S) edges leaving S. For ∣S∣=1,2,3 this number is at least 3,4,5, since a simple triangle-free graph on those sizes has at most 0,1,2 edges. For ∣S∣=4, the absence of triangles and 4-cycles makes the induced graph acyclic, so it has at most 3 edges and at least 6 edges leave. For ∣S∣=5, it is either acyclic with at most 4 edges or is a chordless 5-cycle with 5 edges, so at least 5 edges leave. Every case has at least three boundary edges, a contradiction. Therefore λ(G)≥3.

step 1.1step 2.1F3algebra
3.3

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 2, and κ(G)≥3.

step 1.1step 2.2step 1.3F3
4.1

By [L2] and step 1.1, λ(G)≤δ(G)=3. Together with step 3.2 this gives λ(G)=3.

step 1.1step 3.2L2
5.1

Whitney's inequality [L2] and step 4.1 give κ(G)≤3, while step 3.3 gives the reverse bound. Hence κ(G)=λ(G)=3; both lower bounds were obtained in steps 3.2 and 3.3, which use the cubic regularity of G.

step 4.1step 3.3L2∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

25 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources