ExampleConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-13

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.

$T_{10, 3} = K_{3, 3, 4}$ has $33$ edges and is the unique $10$ -vertex $K_{4}$ -extremal graph

Example

The balanced three-partite graph on ten vertices is

$T_{10, 3} = K_{3, 3, 4},$

and it has $33$ edges. It is the unique extremal graph for forbidding $K_{4}$ on ten vertices.

Facts & Assumptions

Given: The hypotheses and notation of the statement above.

[F1]

Among complete $r$ -partite graphs on $n$ vertices, $T_{n, r}$ has maximum edge count, with equality exactly for balanced part sizes (The exact edge count of $T_{n, r}$ and the unique balancing maximum among complete $r$ -partite graphs).

[F2]

For $n \in N$ and $r \geq 1$ , Turán's theorem gives $ex (n, K_{r + 1}) = e (T_{n, r})$ , and an $n$ -vertex $K_{r + 1}$ -free graph attains equality exactly when it is isomorphic to $T_{n, r}$ (Turán's theorem with equality: $ex (n, K_{r + 1}) = e (T_{n, r})$ , and $T_{n, r}$ is the unique extremal graph).

Verification

technique · compute by the two edge-count formulas

1.1

Division gives $10 = 3 \cdot 3 + 1$ , so the balanced sizes are $4, 3, 3$ . Counting cross-part edges gives $4 \cdot 3 + 4 \cdot 3 + 3 \cdot 3 = 33$ ; equivalently $(\binom{10}{2}) - (\binom{4}{2}) - 2 (\binom{3}{2}) = 45 - 6 - 6 = 33$ .

givenalgebraF1

2.1

Turán's theorem with $r = 3$ says this is $ex (10, K_{4})$ and that equality occurs only for $T_{10, 3}$ .

step 1.1givenF2∎

Depends on

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: 22 results over 11 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

Yufei Zhao, Graph Theory and Additive Combinatorics (standard reference, not scraped)

T10,3=K3,3,4T10,3​=K3,3,4​ has 3333 edges and is the unique 1010-vertex K4K4​-extremal graph